在这个教程中，我们将学习Mythril的安装与使用方法，了解 Mythril的工作原理，掌握如何利用Ether Thief和Suicide模块 分析合约的安全漏洞，以及如何配置Mythril安全分析的交易数量 参数和执行超时参数。
1、安装Mythril安全分析工具
执行如下命令安装Mythril：
1 | $ pip install mythril |
使用如下命令检查安装是否成功，确保版本不低于0.21.7：
1 | $ myth version |
Mythril最基本的安全分析命令是myth analyze，例如：
1 | $ myth analyze <Solidity file> |
没有其他参数的话，myth analyze命令将执行适合大多数情况的通用分析。
2、Mythril工作原理
Mythril通过在一个特制的以太坊虚拟机里运行智能合约字节码来检查 合约的安全问题，它使用符号执行 技术来检查程序可能的状态，分析过程包含以下步骤：
1、获取合约字节码 2、初始化合约账户的状态 3、利用n个交易来探索合约的状态空间，n默认为2，但可以设置为任意值 4、当发现不希望的状态时，证明或否定其在特定假设下的可到达性
当发现一个漏洞状态时，我们可以计算到达该状态所需的交易。这不仅有助于 确定问题的根源，而且也可以用于漏洞利用。
3、Mythril的基本使用方法
现在让我们用Mythril分析一个智能合约。TOkenSale 是一个简单的用于买卖token的智能合约，下面是其源代码：
分析solidity源码要比分析链上的合约实例简单一些：在提供源码的情况下， Mythril可以展示其发现的bug所对应的代码位置。下载TokenSale 并将其另存为tokensale.sol，然后运行如下命令分析该合约的安全问题：
1 | $ myth analyze -m ether_thief tokensale.sol |
-m参数用来声明一组要执行的Mythril分析模块,
彼此之间用逗号隔开。下面让我们先了解一下Ether Thief模块。
4、使用Ether Thief模块检测合约的以太币泄露问题
正如其名称所示，Ether Thief模块检查从合约中提取以太币的交易序列， 它搜索满足以下条件的状态：
- 可以从合约提取的非零数量的以太币
- 从合约提取以太币的账号不是合约的创建账号
- 从合约提取的以太币数量超过了该账号之前存入合约的数量
这是一个发现合约存在以太币泄露问题的好办法。现在让我们用 Ether Thief模块分析一下TokenSale合约：
1 | $ myth analyze -m ether_thief tokensale.sol==== Unprotected Ether Withdrawal ==== |
Mythtril报告说在withdrawal函数中发现了一个问题，但是根源还不清楚。 如果你还没找出bug在哪里，可以再仔细检查下TokenSale的代码并尝试找出 攻击。
可能你已经推断出来，上面的代码中存在整数溢出问题。要利用这个漏洞，我们 需要向buy()函数传入一个特定的值 —— 好消息是，Mythril已经自动帮我们 计算了这个值！看一下上面的执行结果中transaction Sequence部分的输出：
1 | Transaction Sequence:Caller: [CREATOR], data: [CONTRACT CREATION], value: 0xde0b6b3a7640000 |
这一部分列出了3个交易：1个合约创建交易（由合约的creator发送）和2个攻击者发送的交易。 交易的value字段的值标明没有以太币从攻击者转入合约。让我们仔细看一下data字段：
第一个交易包含4字节的函数签名以及看起来没什么危害的一个额外的字节 —— 0x20 —— 表示uint256类型的num_tokens参数的最左端字节，因此最终 传入num_tokens的值是：
1 | buy(0x2000000000000000000000000000000000000000000000000000000000000000) |
现在让我们看一下这个输入值对第16行require语句的影响：
1 | require(msg.value == numTokens * PRICE_PER_TOKEN); |
PRICE_PER_TOKEN 被设置为1 Ether，对应1e18 wei，将这个数量与 上面Mythril给出的值相乘就会产生整数溢出。更确切地说， uint256(1e18) * uint256(numTokens) 的结果为0 。
因此require语句就会通过，然后海量的token就记在交易发送方的 名下了，即时他们没有发送任何以太币。
在第2个交易中，不合法的token被出售以换回以太币，即调用sell(uint256)。 由于Mythril符号化表示合约账户余额，它为numTokens输出一个非常大的随机值。 在现实中，攻击者将会利用与账户实际以太币余额匹配的值。
5、配置Mythril安全分析的交易数量
在使用Mythril时需要了解的一个重要概念，就是交易数量。这个 变量用来指定进行符号化执行的交易的数量。默认值2对于检测 许多常见bug都足够了，例如整数溢出、未初始化的存储变量以及 错误命令的构造函数等。然而，只有2个交易深度还无法发现那些 在更多交易下才会显现的bug。
因为每个交易都可以有多个有效的最终状态，那么当交易数量增加 后，潜在的状态空间数量（理论上）将指数级增长。幸运的是， Mythril还是很聪明的，它通过分析程序执行路径之间的关系可以 缩小后续交易的搜索空间，这意味着你可以在合理的时间框架内执行多个交易。
下面让我们看另一个例子，看看你是否能找出其中的安全问题，注意 合约名字：
这个合约有一个后门，它允许任何知道密码的人成为合约的owner —— 我们知道，私有状态变量并不是真的秘密，和公开状态变量的区别 在于，solc不会为私有变量生成访问函数。
另一个流行的Mythril模块是Suicide，这个模块检查那些由合约创建 者之外的账号发送的可能杀掉合约的交易。运行Mythril分析上面的 killme合约，就可以”意外地“杀掉合约：
1 | $ myth analyze killme.sol |
Mythril看起来忽略了合约存在的漏洞，原因是至少需要3个交易才能杀掉 合约：发送方必须向activePassword(bytes11 password)方法传入正确的密码， 然后调用pwnContract()成为owner，最后调用kill()触发合约自毁。
现在让我们看看如果用-t参数增加交易数量后会得到什么结果：
1 | $ myth analyze killme.sol -t3 |
这次检测出了合约中的问题，我们得到了包含3个交易的序列。查看交易的data 可以了解被调用的函数名以及参数：
注意：交易1中的字节序列0x747474(…) 是用于补齐uint256参数的随机数据，这部分 数据可以是任意值。
6、设置Mythril安全分析的执行超时
默认情况下，Mythril会尝试执行-t参数指定数量的交易。然而，有时我们希望 能指定执行时间的上限。如果增加–execution-timeout参数，Mythril就会在 超过指定事件后终止，并返回在此期间发现的所有问题。
注意你可以在任何时候使用CTRL+C来中断分析任务的执行，这时Mythril也 会返回此前已经发现的漏洞。例如，可以用Mythril分析Parity的WalletLibrary 并设定最多分析10分钟：
1 | $ myth analyze --execution-timeout 600 -t2 -mether_thief,suicide -c [WALLETLIBRARY-BYTECOE] |
原文链接：Practical Smart Contract Security Analysis and Exploitation
汇智网翻译整理，转载请标明出处