智能合约安全工具实用指南第3部分：Mythril

警告

本文不是对自动分析器的评级。我使用它们来分析我自己的合约：故意添加伪错误并研究响应。它不是一种“更好或更差”的研究类型，这类任务需要对大量合约进行盲审，实际结果不会很精确，因为这类软件的性质。特定合约的小错误可能会使一大部分分析器逻辑失效，而简单的启发式特征，比如找到竞争对手根本未添加的典型错误，可以提升分析器的性能。此外，合约编译错误可能会影响结果。所有被审查的软件都是相当新的，并且持续开发，因此以太坊智能合约错误的严肃开源安全分析工具不应被认为是无可解决的。在这篇文章中，我们的目标不是帮助读者判断哪个分析器更好，而是展示不同的代码分析方法在实践中的应用以及如何选择合适的方法。我们建议同时使用多个工具，为被审计合约选择最合适的。本文与当前软件版本相关，在你阅读本文时，可能有许多事情会被改变。

分析工具：Mythril

描述：以太坊智能合约的开源安全分析工具

Github: https://github.com/ConsenSys/mythril-classic

配置及预启动

Mythril执行几种类型的分析。这里有一些很棒的相关文章：请访问 这里，看看 这篇 和 这篇 加以改动。在继续之前，我强烈建议你先阅读这些。首先，让我们构建一个Mythril Docker镜像（谁知道我们可能想更改什么呢？）：

git clone
https://github.com/ConsenSys/mythril-classic.git
cd mythril-classic
docker build -t myth .

现在我们将运行 contracts/flattened.sol（我使用的是之前在 引言 中提到的 相同合约），该合约包含两个主要合约：一个OpenZeppelin的“Ownable”和我们的“ Booking”合约。我们仍然面临编译器版本问题（我们的合约是0.4.20），我将按照上次在关于Slither的 文章 中所做的相同方式解决它：在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 合约，并且正确加载所有依赖关系，我们将使用以下命令：

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 编译的内容，并检查整个项目的漏洞。在合约文件名后添加合约名，如 -x contracts/flattened.sol:Booking 使用冒号也是一个重要特征，否则Mythril将分析所有可用合约。我们认为OpenZeppelin的 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。Mythril指南提到：“ 它使用了符号执行、污点分析和控制流检查，以检测多种安全漏洞。”如果你对这些术语不熟悉，我建议你查看关于 符号测试 的维基百科文章以及关于 污点检查 的精彩演示，针对x86。简而言之，Mythril模拟合约执行，存储所有执行分支，并努力尝试不同的参数组合及可能的选项以达到“危险”的合约状态。大体过程如下（请参见上面的文章）：

1. 定义输入变量集。这些将作为符号变量，所有其他变量将视为具体值。
2. 这些变量和每个可能影响符号变量值的操作应记录到跟踪文件中，以及路径条件或任何发生的错误。
3. 选择一组输入变量开始。
4. 执行本地合约代码并保存跟踪文件。
5. 在跟踪上进行符号重新执行，生成一组符号约束（包括路径条件）供未来分析。
6. 将最后的路径条件从“已经分析”的条件中排除，下一次分析新的执行路径。如果没有这样的路径条件，算法结束。
7. 分析路径条件：生成新的输入以修正所有路径条件。如果没有这样的输入，返回第6步并尝试下一个执行路径。
8. 返回第4步。

通俗来说，Mythril遍历分支并检测使每个分支可到达的输入值组合。由于知道哪些分支可以追溯到 assert，transfer，selfdestruct 和其他危险操作码，Mythril检测影响执行安全的输入值和交易组合。Mythril的独特之处在于其断开不将遵循的分支并分析控制流的方法。要更深入了解Mythril的工作原理，请点击 这里。由于智能合约的确定性特性，相同的指令序列总是会产生相同的状态变化集，无论平台、架构和环境。而Mythril以及类似的结合了符号执行和本地执行的分析工具，对于函数非常小且资源有限的智能合约可能非常有效。Mythril运行“状态”的概念，指合约代码、其环境、当前命令指示器、存储和栈内容。文档中写道：

机器状态μ定义为元组 (g, pc, m, i, s)，其中g为可用气体，pc ∈ P256，存储内容为内存内容，内存中活动字数（从位置0连续计数），以及栈内容。内存内容μm是一系列大小为256的零。

状态变化图是我们主要的研究项目。如果分析执行成功，图形详细信息将包含在输出日志中。此外，Mythril还有 --graph 选项，允许以友好的可读格式构建此图。现在，已有一个或多或少清晰的Mythril工作原理的认识，让我们回到合约，找出为什么分析失败并返回“ [WARNING]: 在合约创建执行期间未创建合约”。首先，我调整了 --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;
}

回到Mythril的动作模式，为了启动跟踪，它必须调用合约构造函数，因为整个后续执行过程都由构造函数中的参数决定。例如，如果使用 _price == 0 来调用构造函数， require(_price > 0) 异常将返回。同时，构造函数将继续失败，尽管Mythril尝试不同的 _price 值，只要 _price <= _cancellationFee。该合约具有严格限制的多个参数；Mythril无法猜测所有有效组合。因此，它将尝试移动到下一个执行路径，通过参数排序构造函数参数，但鉴于参数组合的巨大数量，它几乎没有成功的机会。因此，由于每个执行路径都遇到某些 require(…)，合约上传失败，我们面临上述问题。

现在我们有两个选项。第一个是关闭所有“ require”，通过注释掉它们。然后Mythril将能够使用任何参数组合来调用构造函数并成功运行。但是，使用随机参数意味着检测到由于向构造函数发送无效值而导致的随机错误。简单地说，Mythril可以检测到合约创建者定义 _cancellationFee 超过 _mprice 百万倍时发生的错误，但这样的错误和合约对审计员没有用，Mythril只是在浪费资源寻找这个错误。如果我们想要相对全面的部署参数，设定更现实的构造参数进行后续分析显得合理，以防止Mythril搜索那些只要合约被正确部署就永远不会发生的错误。最好的方法是使用将来合约部署时将使用的真实参数值。

我花了很多小时将各种构造函数段打开和关闭，试图找出部署失败的地方。尽管这些麻烦已经足够，构造函数使用了 getCurrentTime()，它返回当前时间，而我完全不清楚Mythril是如何处理此调用的。我将省略我冒险的进一步细节，因为审计员很可能在常规使用中了解细节。因此，我选择了第二个选项：我从构造函数中移除了所有参数，甚至 getCurrentTime()，然后直接在构造函数中硬编码了所需的内容：

function Booking( ) public payable {
    m_description = "关于酒店和美丽海景的我的很长的预订文本！";
    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; // 当前时间 + 1 天
    m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // 当前时间 + 4 天
    m_acceptObjectPeriod = 3600 * 8; // 8 小时
    m_noCancelPeriod = 3600 * 24; // 1 天 
    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参数。在我的例子中， -- max-depth=34 在AWS t2.medium实例上有效。请注意，当我使用更强大的笔记本电脑时，不需要 max-depth。根据参数在 这里 的用法，它是分析分支设置策略的一部分，默认值为无穷大（ 请查看代码）。你可以根据需要调整该参数，但确保合约分析成功。在成功启动分析后，你将看到如下消息：

mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states
mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............

第一行描述了分析图参数。分析备选执行分支需要巨大的计算能力，因此审计较大合约即使在强大的PC上也需要时间。

错误查找

现在我们将搜索错误并添加我们自己的错误。Mythril查找所有包含 transfer，selfdestruct，assert 的分支，并检测其他具有安全性的特定问题。因此，如果代码包含上述任何指令，Mythril将识别出可能的执行分支，甚至显示导致它们的所有交易！我们先看看Mythril为不幸的Booking合约发掘了什么。第一个警告如下：

==== 依赖于可预测的环境变量 ====
SWC ID: 116
严重级别: 低
合约: Booking
函数名: fallback
PC地址: 566
估计气体使用量: 17908 - 61696
Ether的发送依赖于可预测变量。
该合约根据以下变量的值发送Ether：
- block.timestamp
请注意，coinbase、gaslimit、区块号和时间戳等变量的值是可预测的和/或可以被恶意矿工操控。
请勿将它们用于随机数生成或做出关键决策。
--------------------
在文件中：contracts/flattened.sol:142msg.sender.transfer(msg.value-m_price)

这发生是因为：

require(m_rentDateStart > getCurrentTime());

在回调函数中。

请注意，Mythril发现了 block.timestamp 的问题在 getCurrentTime() 中。广义上讲，这不是合约错误，但Mythril将 block.timestamp 关系到以太币转移是非常棒的！程序员应该意识到，该决定是 依赖于矿工控制的值。例如，在未来拍卖或其他竞标的发展情况下，存在抢跑交易攻击的风险。

现在我们看看如果隐藏函数调用中的变量，Mythril是否能识别到 block.timestamp 的依赖：

function getCurrentTime() public view returns (uint256) {
-     return now;
+     return getCurrentTimeInner();
}+ function getCurrentTimeInner() internal returns (uint256) {
+     return now;
+ }

太棒了！Mythril仍然能看到 block.timestamp — 以太币转移的依赖，这对审计员来说真的很重要。Mythril允许在进行多个合约状态变化后跟踪变量与决策之间的依赖关系，即使它隐藏在逻辑中。然而，Mythril并不是无所不能，它无法追踪所有可能的变量间依赖。如果我们继续使用 getCurrentTime() 函数并进行 3 层嵌套，警告将消失。每个函数调用都需要新的状态分支，以及巨大的资源来分析深层代码嵌套的层数。此外，我可能误用了分析参数，分析器仍然可能在某个地方识别出错误。正如我之前提到的，该产品正在积极开发中，而在我写这篇文章时，我看到代码库中包含了带有 max-depth 标签的提交。请不要太在意当前的问题，我们已经找到了足够的证据，证明Mythril有效地跟踪变量依赖关系。

现在，我们将为“Booking”合约添加一个随机以太币发送的功能，即任何人可以在合约处于 State.PAID 状态且客户已经用以太币支付预订时撤回1/5的以太币。以下是该功能：

function collectTaxes() external onlyState(State.PAID) {
    msg.sender.transfer(address(this).balance / 5);
}

Mythril检测到以下问题：

==== 无保护的以太币撤回 ====
SWC ID: 105
严重级别: 高
合约: Booking
函数名: collectTaxes()
PC地址: 2492
估计气体使用量: 2135 - 2746
任何人都可以从合约账户中撤回ETH。
除合约创建者以外的任意发送方可以在不提前发送相等数量的ETH到合约的情况下，从合约账户中撤回ETH。
这很可能是一个漏洞。
--------------------
在文件中：contracts/flattened.sol:149msg.sender.transfer(address(this).balance / 5)
--------------------
--------------------
交易序列:{
    "2": {
        "calldata": "0x",
        "call_value": "0xde0b6b3a7640000",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    },
    "3": {
        "calldata": "0x01b613a5",
        "call_value": "0x0",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    }
}

太棒了，Mythril甚至展示了导致可能以太币撤回的两笔交易！现在我们将把 State.PAID 改为 State.RENT，改成这样：

- function collectTaxes() external onlyState(State.PAID){
+ function collectTaxes() external onlyState(State.RENT) {

现在 collectTaxes() 函数只能在合约处于 State.RENT 状态时调用，而账户中没有剩余，因为合约已将以太币发送给所有者。这次Mythril不会显示“==== _无保护的以太币撤回 ====”_错误！ onlyState(State.RENT) 修饰符阻止分析器到达向非零账户余额发送以太币的分支。因此，Mythril遍历了不同的参数选项，但 State.RENT 仅在所有以太币发送给所有者后才可用。因此，以非零余额访问此代码分支是不可能的，Mythril不会打扰审计员——出色的结果！

类似地，Mythril将追踪 selfdestruct 和 assert，显示可能导致合约毁灭或在关键函数中发生异常的操作。这里我将省略这些示例，并建议测试类似导致 selfdestruct 的函数。

不要忘了，Mythril执行符号执行分析，即使没有模拟，也能检测到漏洞。例如，任何使用 “+”、 “-” 和其他算术操作的地方可以被视为“整数溢出”漏洞，如果操作数在某种程度上被攻击者控制。但正如我所说，Mythril最强大的特性是符号和本地执行的结合，能检测分支条件的值。

结论

毫无疑问，一篇文章不足以描述Mythril能够检测到的全部问题。此外，它在真实的区块链环境中工作，通过签名找到必要的合约和漏洞，构建漂亮的调用图并编辑报告。Mythril允许使用基于Python的接口编写个别测试脚本，轻松测试特定函数，修正参数值，甚至实现与反汇编代码工作的自定义策略。

与 IDA Pro 不同，Mythril仍然是一个年轻软件，几乎没有文档，仅有一些文章。许多Mythril参数仅在代码中有描述（从 cli.py 开始）。我希望尽快能够看到全面详细的文档，描述参数及其内部逻辑。

当合约规模相对较大时，显示错误消息需要大量空间。我希望收到有关检测到的错误的“压缩”数据（每个错误一行），因为在使用Mythril时，必须彻底追踪分析过程。此外，去除审计员已知为假阳性错误的输出的可能性，也将是一个有用的功能。

总体而言，Mythril是一个出色且非常强大的智能合约分析工具。每个智能合约审计员都应该使用它，因为它引起了对代码关键部分的关注，并检测了变量之间隐藏的连接。为了总结，使用Mythril的建议如下：

1. 最小化初始合约条件。如果Mythril在永远不会执行的分支上浪费资源，它将错过真正重要的漏洞。始终尝试缩小可能的分支数量（如果适用）。
2. 确保分析已启动，不要忽略诸如 “ mythril.laser.ethereum.svm [WARNING]: 在合约创建执行期间未创建任何合约…” 的消息，否则你可能认为没有漏洞。
3. 你可以轻松否定代码分支，限制Mythril的选择并节省资源。尽量不要使用 max-depth 约束，以免切断分析，谨慎不要隐藏错误。
4. 注意每个警告，即使是对合约代码的微小注释 — 都能使其他开发人员更简单。

我们的下一篇文章将致力于Manticore。敬请期待！其他待发布或正在制作的文章如下：

第1部分：引言。编译、扁平化、Solidity版本

第2部分：Slither

第3部分：Mythril（本文）

如果你对Mythril或其他自动化工具在你的项目中的使用有特定问题，请随时通过我们的 网站 或 Telegram 联系我们。

原发于 mixbytes.io 。

• 原文链接： medium.com/mixbytes/a-pr...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～