警告
本文未对自动分析仪的有效性进行评级。 我将它们应用于我自己的合同，有意地综合错误并研究反应。 此类研究不能成为确定“优劣”的基础；因此，对大量合同样本进行盲目研究是有意义的，考虑到此类软件的反复无常，这非常困难。 合同中的小错误很可能会禁用大量的分析器逻辑，而简单的启发式符号可能会通过发现竞争对手根本无法添加的普遍错误而为分析器增加大量点。 合同编制和编制中的错误也可能起作用。 所涉及的所有软件都还很年轻，并且正在不断开发中，因此不要将批评意见视为不可弥补的问题。
本文的目的是使读者了解不同分析器中的代码分析方法如何工作以及正确使用它们的能力，而不是“做出选择”。 合理的选择是一次使用多个工具，重点放在最适合所分析合同的工具上。
设置和启动准备
Mythril一次使用几种类型的分析，以下是有关它的几篇好文章： 最重要的是this或this 。 在继续之前，有必要先阅读它们。
首先，让我们构建自己的Mythril Docker镜像（我们想要更改其中的内容是否重要？）：
git clone https://github.com/ConsenSys/mythril-classic.git cd mythril-classic docker build -t myth .
现在，尝试在我们的contracts/flattened.sol （我使用引言中讨论的同一合同）上运行它，其中有两个主要合同， Ownable是Zeppelin拥有的和Booking 。 我们仍然对编译器版本有问题，我以与上一篇文章相同的方式修复了它，在Dockerfile中添加了将替换编译器版本的行：
COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin
重建图像后，您可以尝试运行合同分析。 立即让我们使用-v4和--verbose-report标志查看所有警告。 出发：
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ -v4 \ --verbose-report \ -x contracts/flattened.sol
在这里，我们使用没有依赖性的扁平合约。 要分析单独的Booking.sol合同并让Mythril提取所有依赖项，可以使用以下方法：
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ --solc-args="--allow-paths /tmp/node_modules/zeppelin-solidity/ zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \ -v4 \ --verbose-report \ -x contracts/Booking.sol
我更喜欢使用展平选项，因为 我们将在代码中进行很多修改。 但是Mythril也有一个非常方便的模式--truffle ，该模式仅--truffle truffle所有内容，并检查整个项目是否存在漏洞。 另一个重要功能是能够通过冒号指定要分析的合同名称的功能，否则Mythril将分析它遇到的所有合同。 我们认为Ownable的Ownable是一个安全的合同，我们只打算分析Booking ，所以运行的最后一行是：
docker run -v $(pwd):/tmp -w /tmp myth:latest -x contracts/flattened.sol:Booking -v4 --verbose-report
启动和部署合同
我们从上一行开始分析器，查看输出，除其他外，我们得到以下行：
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) The analysis was completed successfully. No issues were detected.
事实证明，我们的合同并未在仿真器中创建和“修复”。 因此，我建议对所有类型的分析使用-v4标志，以查看所有消息，并且不要遗漏任何重要的消息。 让我们找出问题所在。 解决这一实际问题对于理解如何正确使用秘银很重要。
因此，我们正在阅读有关Mythril的文章： It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities 。 如果您不太熟悉这些术语，我建议您在此处提供有关condical测试的Wiki，但这是有关x86污染检查的很好的介绍。 简而言之：Mythril模拟合同的执行情况，修复可以执行的分支，并尝试实现合同的“中断”状态，对各种参数组合进行排序，并设法避开所有可能的路径。 这是上面文章的示例操作图：
1. . symbolic-, . 2. , , trace . , , . 3. . 4. trace-. 5. symbolic execution trace, symbolic , , , . 6. , . , . 7. : , , input-, , . input- , .6 . 8. .4
如果您对其进行了极大地简化，那么Mythril在代码中遇到了一个分支，便可以了解可以进入哪个变量集和另一个分支。 在每个分支中，Mythril都知道它是否导致assert ， transfer ，selfdestruct和其他与安全相关的操作码。 因此，Mythril分析哪些参数和事务集可能导致安全漏洞。 Mythril切断从未获得控制权的分支并分析控制流的方法是其主要技巧。 有关Mythril肠和分支行走的更多详细信息在此处编写。
由于智能合约执行的确定性，无论平台，体系结构或环境如何，相同的指令序列始终严格导致一组状态变化。 此外，智能合约中的功能相当短，并且资源非常有限，因此像Mythril这样的分析器将符号执行和本机执行相结合，可以非常有效地用于智能合约。
在此过程中，Mythril使用“状态”的概念-这是合同的代码，其环境，指向当前命令的指针，合同的存储以及堆栈的状态。 这里是文档：
The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc ∈ P256, the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents μm are a series of zeroes of size 256.
状态之间的过渡图是研究的主要对象。 如果成功启动分析，则有关该图的信息将显示在分析日志中。 另外，Mythril可以使用--graph选项以--graph形式构建此图形。
现在或多或少地了解了Mythril会做什么，我们将继续了解为什么未解析合同以及合同的来源[WARNING]: No contract was created during the execution of contract creation 。 首先，我扭曲了--create-timeout和--max-depth （按照建议），但没有得到结果，我以为是构造函数的责任–它中的某些功能不起作用。 这是他的代码：
function Booking( string _description, string _fileUrl, bytes32 _fileHash, uint256 _price, uint256 _cancellationFee, uint256 _rentDateStart, uint256 _rentDateEnd, uint256 _noCancelPeriod, uint256 _acceptObjectPeriod ) public payable { require(_price > 0); require(_price > _cancellationFee); require(_rentDateStart > getCurrentTime()); require(_rentDateEnd > _rentDateStart); require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd); require(_rentDateStart > _noCancelPeriod); m_description = _description; m_fileUrl = _fileUrl; m_fileHash = _fileHash; m_price = _price; m_cancellationFee = _cancellationFee; m_rentDateStart = _rentDateStart; m_rentDateEnd = _rentDateEnd; m_noCancelPeriod = _noCancelPeriod; m_acceptObjectPeriod = _acceptObjectPeriod; }
回想一下秘银的动作算法。 要运行跟踪，您需要调用合同构造函数，因为所有后续执行将取决于调用构造函数的参数。 例如，如果您使用_price == 0调用构造函数，则构造函数将在require(_price > 0)上引发异常。 即使Mythril迭代许多_price值，例如_price <= _cancellationFee ，构造函数仍会中断。 在此合同中，有十二个与严格限制相关联的参数，而Mythril当然无法猜测参数的有效组合。 他尝试转到执行的下一个分支，对构造函数的参数进行排序，但是他几乎没有机会猜测-参数太多。 因此，合同的计算无法解决-所有方式都基于某种require(...) ，我们得到了上述问题。
现在我们有两种方法：第一种是通过将它们注释掉来禁用构造函数中的所有require 。 然后Mythril将能够使用任何参数集调用构造函数，并且一切正常。 但这意味着，通过检查带有此类参数的合同，Mythril将发现错误，而错误的值可能会传递给构造函数。 简而言之，如果Mythril发现如果合同创建者将_cancellationFee指定为_cancellationFee的十亿倍的价格时出现的_mprice ，那么在这种bug中就没有用-这样的合同将永远不会被阻塞，并且将花费大量资源来查找错误。 我们暗示该合同仍然停留在或多或少一致的参数上，因此为了进行进一步分析，有必要指定更切合实际的构造函数参数，以便Mythril不会查找如果正确关闭该合同永远不会发生的错误。
我花了很多时间试图确切了解部署的中断位置，包括并禁用构造函数的各个部分。 除了麻烦之外，构造函数还使用getCurrentTime()返回当前时间，目前尚不清楚此调用如何处理Mythril。 在这里我不会描述这些冒险，因为 这些细微之处很可能是经常使用的，因此审计人员知道了。 因此，我选择了第二种方法：限制输入数据，并简单地从构造函数中删除所有参数，甚至是getCurrentTime() ，也直接在构造函数中直接硬编码必要的参数（理想情况下，这些参数应从客户那里获得）：
function Booking( ) public payable { m_description = "My very long booking text about hotel and beautiful sea view!"; m_fileUrl = "https://ether-airbnb.bam/some-url/"; m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7; m_price = 1000000000000000000; // 1 ETH m_cancellationFee = 100000000000000000; // 0.1 ETH m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days m_acceptObjectPeriod = 3600 * 8; // 8 hours m_noCancelPeriod = 3600 * 24; // 1 day require(m_price > 0); require(m_price > m_cancellationFee); require(m_rentDateStart > 1550664800); require(m_rentDateEnd > m_rentDateStart); require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd); require(m_rentDateStart > m_noCancelPeriod); }
另外，要开始一切，还必须设置max-depth参数。 它在AWS t2.medium实例上使用--max-depth=34此构造函数为我工作。 同时，在功能更强大的笔记本电脑上，一切开始时都没有max-depth 。 通过使用此参数判断，有必要构造用于分析的分支，并且其默认值为infinity（ 代码 ）。 因此，请旋转旋转此参数，但要确保分析了所需的合同。 您可以通过以下消息了解此信息：
mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............
第一行仅描述了将要分析的图形，请自己阅读其余几行。 需要大量的计算资源来分析可以执行的各种分支，因此在分析大型合同时，即使在快速的计算机上也必须等待。
搜索错误
现在，我们将查找错误并添加我们自己的错误。 秘银寻找分支，在分支中进行广播，自毁，声明和其他从安全角度来看很重要的动作。 如果以上说明之一出现在合同代码中某处，Mythril将检查可能进入此分支的方式，此外，还会显示通往该分支的交易顺序！
首先，让我们看看Mythril为长期受苦的Booking合同发行了什么。 第一个警告：
==== Dependence on predictable environment variable ==== SWC ID: 116 Severity: Low Contract: Booking Function name: fallback PC address: 566 Estimated Gas Usage: 17908 - 61696 Sending of Ether depends on a predictable variable. The contract sends Ether depending on the values of the following variables: - block.timestamp Note that the values of variables like coinbase, gaslimit, block number and timestamp are predictable and/or can be manipulated by a malicious miner. Don't use them for random number generation or to make critical decisions. -------------------- In file: contracts/flattened.sol:142 msg.sender.transfer(msg.value-m_price)
它的出现是因为
require(m_rentDateStart > getCurrentTime());
在后备功能中。
请注意，Mythril意识到getCurrentTime()隐藏在getCurrentTime() 。 尽管合同的含义不是一个错误，但Mythril将block.timestamp与广播相关联的事实非常出色！ 在这种情况下，程序员必须理解，决策是基于矿工可以控制的值做出的。 而且，如果将来在合同的该地点进行拍卖或其他服务拍卖，则必须考虑到前期攻击的可能性。
让我们看看如果我们在这样的嵌套调用中隐藏变量， block.timestamp是否看到对block.timestamp的依赖：
function getCurrentTime() public view returns (uint256) { - return now; + return getCurrentTimeInner(); } + function getCurrentTimeInner() internal returns (uint256) { + return now; + }
是的！ Mythril继续看到block.timestamp和广播传输之间的联系，这对于审核员而言非常重要。 攻击者控制的变量与合同状态几次更改后做出的决定之间的联系可以被逻辑掩盖，而Mythril允许您跟踪它。 尽管不值得依赖为所有可能的变量之间的所有可能的连接进行getCurrentTime()的事实：如果继续模拟getCurrentTime()函数并进行三层嵌套，则警告会消失。 对Mythril的每个函数调用都需要创建新的状态分支，因此分析非常深层的嵌套将需要大量资源。
当然，我很可能错误地使用了分析参数，或者在分析仪深度的某处发生了截断。 就像我说的那样，在撰写本文时，该产品正在积极开发中，我看到在仓库中提到了max-depth的提交，因此不要认真对待当前的问题，我们已经找到了足够的证据证明Mythril可以非常有效地寻找变量。
首先，在合同中添加一个功能，该功能可将广播提供给任何人，但仅在客户端将广播发送给合同之后。 我们允许任何人提取1/5的以太State.PAID ，但State.PAID是合同处于State.PAID状态（即仅在客户用以太State.PAID支付了租用的号码之后）。 这是函数：
function collectTaxes() external onlyState(State.PAID) { msg.sender.transfer(address(this).balance / 5); }
秘银发现了问题：
==== Unprotected Ether Withdrawal ==== SWC ID: 105 Severity: High Contract: Booking Function name: collectTaxes() PC address: 2492 Estimated Gas Usage: 2135 - 2746 Anyone can withdraw ETH from the contract account. Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent a equivalent amount of ETH to it. This is likely to be a vulnerability. -------------------- In file: contracts/flattened.sol:149 msg.sender.transfer(address(this).balance / 5) -------------------- -------------------- Transaction Sequence: { "2": { "calldata": "0x", "call_value": "0xde0b6b3a7640000", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" }, "3": { "calldata": "0x01b613a5", "call_value": "0x0", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" } }
太好了 秘银甚至带来了两笔交易，导致您可以从合约中提取以太币。 现在将State.PAID需求更改为State.RENT ，如下所示：
- function collectTaxes() external onlyState(State.PAID){ + function collectTaxes() external onlyState(State.RENT) {
现在仅在合同处于State.RENT状态时才可以调用collectTaxes() ，并且此时此刻没有任何余额，因为 合同已经将整个广播发送给了所有者。 重要的是，Mythril这次不会输出错误==== Unprotected Ether Withdrawal ====币取回==== Unprotected Ether Withdrawal ==== ！ 在onlyState(State.RENT)的条件下，分析器没有到达代码分支，该代码分支从具有非零余额的合同发送以太onlyState(State.RENT) 。 Mythril为参数使用了不同的选项，但是只有将所有广播发送给出租人后，您才能进入State.RENT 。 因此，不可能以非零的余额到达代码的这一分支，并且Mythril绝对不会打扰审计人员！
同样，Mythril会发现selfdestruct并assert ，向审计师展示了哪些行为可能导致合同毁灭或破坏重要职能。 我将不给出这些示例，仅尝试使函数类似于上面的函数，仅调用selfdestruct并扭曲其逻辑。
另外，请不要忘记Mythril的一部分是符号执行，而这种方法本身可以在不模拟执行的情况下确定许多漏洞。 例如，如果攻击者以某种方式控制操作数之一，则对“ +”，“-”和其他算术运算符的任何使用都可以视为“整数溢出”的漏洞。 但是我再说一遍，Mythril最强大的功能是将符号和本机执行以及确定导致逻辑分支的参数值组合在一起。
结论
当然，要显示Mythril能够检测到的所有潜在问题，将不仅需要撰写一篇文章，还需要多篇文章。 对于其他所有事物，他都知道如何在真实的区块链中完成所有工作，通过签名找到必要的合同和漏洞，构建漂亮的调用图，格式化报告。 Mythril还允许您编写自己的测试脚本，为合同提供基于python的界面，并允许您测试单个功能，修复参数值，甚至实施自己的策略以任意程度的灵活性处理反汇编代码。
Mythril仍然是一个相当年轻的软件，它不是IDA Pro，除少数文章外，很少有文档。 许多参数的值只能从cli.py开头的Mythril代码中读取。 我希望在文档中对每个参数的操作进行完整而深入的描述。
另外，当合同或多或少很大时，一堆错误的输出会占用很多空间，但是我希望能够接收有关发现的错误的压缩信息，因为 使用Mythril时，您必须绝对查看分析路径，查看已尽力而为地测试了哪些合同，并能够强行禁用审计师认为错误肯定的特定错误。
但是总的来说，Mythril是一种用于分析智能合约的出色且功能非常强大的工具，目前应由任何审核员掌握。 它使您至少可以关注代码的关键部分，并检测变量之间的隐藏关系。
总结一下，使用Mythril的建议是：
- 尽可能缩小研究合同的起始条件。 如果在分析期间Mythril将大量资源花在分支上，而这些资源在实践中永远不会实现，那么它将失去发现真正重要的bug的能力，因此您应始终尝试缩小潜在分支的范围。
- 确保合同分析已经开始，不要错过
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout)类的mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) ，否则您可能会误认为没有错误。 - 您可以在合同代码中任意禁用分支，从而使Mythril在选择分支和节省资源方面的变化更少。 尝试对
max-depth进行无限制的操作，以免“砍掉”分析，但请注意不要掩盖错误。 - 注意每个警告，即使是简短的注释有时也值得至少在合同代码中添加注释，这对于其他开发人员来说更容易。
在下一篇文章中，我们将处理Manticore分析器，但这是准备或计划编写的文章的目录：
第1部分。 简介。 编译，展平，Solidity版本
第2部分。
3. Mythril ( )
4. Manticore ( )
5. Echidna ( )