智能合约安全工具实用指南

mixbytes
发布于 2023-02-25 12:57
阅读 36

本文深入探讨了Mythril工具在智能合约安全分析中的应用，介绍了其配置、执行流程及分析方法，通过实例详细说明了如何识别合约中的安全漏洞，尤其是参数限制对合约部署的影响。作者利用Mythril的特色功能强调了其在智能合约审核中的重要性，并提出了一些使用建议。整体内容适合对智能合约安全有一定基础的读者，值得深入学习。

作者：MixBytes团队

![](https://img.learnblockchain.cn/2025/03/09/01.jpg)

## 警告

本文并不是对自动分析器的评级。我使用它们来分析我的合约：故意添加伪错误并研究响应。这并不是一种 "更好或更差" 的类型研究，这类任务需要对大量合约进行盲审，而由于此类软件的性质，实际结果不会非常精确。在特定合约中的一个小错误可能会使分析器逻辑的大部分失效，而一个简单的启发式特征，如找到竞争对手简单忘记添加的典型错误，则可以提升分析器的水平。此外，合约编译错误可能会影响结果。所有审查过的软件都相当新，并且持续在开发中，因此严重错误不应被视为不可解决的。

在这篇文章中，我们的目的是展示不同的代码分析方法在实践中的应用以及如何选择合适的方法，而不是帮助读者决定哪个分析器更好。我们建议同时使用多种工具，并选择最适合审计合约的工具。

## 配置和预启动

Mythril执行几种类型的分析。以下是一些很棒的相关文章：导航 [这里](https://arxiv.org/pdf/1902.03868.pdf)，看看 [这个](https://hackernoon.com/introducing-mythril-a-framework-for-bug-hunting-on-the-ethereum-blockchain-9dc5588f82f6) 和 [这个](https://hackernoon.com/practical-smart-contract-security-analysis-and-exploitation-part-1-6c2f2320b0c) 的变化。我强烈建议在继续之前阅读它们。

首先，让我们构建一个Mythril Docker镜像（谁知道我们可能想要更改什么呢？）：

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

现在我们将运行 contracts/flattened.sol（我使用的是我在 [引言](https://learnblockchain.cn/article/12510) 中提到的相同合约），它包含两个主要合约，一个是OpenZeppelin的Ownable，一个是我们的Booking合约。我们仍然面临编译器版本问题（我们的合约为0.4.20），我将按照上次的方式解决它：在Dockerfile中添加一个编译器更改命令：

```cpp
COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin
```

重新编译镜像后，我们继续进行合约分析。不要忘记激活 -v4 和 --verbose-report 标志，以查看所有警告。让我们开始吧：

```ruby
docker run -v $(pwd):/tmp \
           -w /tmp myth:latest \
           -v4 \
           --verbose-report \
           -x contracts/flattened.sol
```

现在我们处理一个没有依赖项的扁平合约。为了单独分析 Booking.sol 合约并正确加载所有依赖项，我们将使用以下命令：

```ruby
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。启动前的最后一个命令如下：

```ruby
docker run -v $(pwd):/tmp -w /tmp myth:latest -x
contracts/flattened.sol:Booking -v4 --verbose-report
```

## 合约启动和部署

在运行合约后，我们收到以下消息：

```css
mythril.laser.ethereum.svm [WARNING]:
在合约创建执行过程中没有创建合约
增加创建执行的资源（--max-depth或--create-timeout）
分析成功完成。未检测到问题。
```

结果我们合约没有在模拟器中被 “部署”。因此我建议在所有分析中使用 -v4 标志，以免错过重要信息。让我们弄清楚出了什么问题。这个实际问题的解决将帮助我们了解如何正确运行Mythril。Mythril指南说：“它使用共符号分析、污点分析和控制流检查来检测各种安全漏洞。”如果你对这些术语不熟悉，我建议阅读关于 [共符号测试](https://en.wikipedia.org/wiki/Concolic_testing) 的维基文章，以及关于 [污点检查](http://web.cs.iastate.edu/~weile/cs513x/2018spring/taintanalysis.pdf) 针对x86的精彩演示。简而言之，Mythril模拟合约执行，存储所有执行分支，并努力通过尝试不同的参数组合和可能的选项来达到“危险”的合约状态。粗略的过程如下（详见上述文章）：

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

简单来说，Mythril遍历分支并检测输入值的组合，以便能够到达它们。通过了解哪些分支可追踪以断言、转账、自毁和其它危险操作码，Mythril检测影响执行安全的输入值和交易组合。Mythril独特之处在于其切断从未控制的分支并分析控制流的方法。要深入了解Mythril的底层运作，请点击 [这里](https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf)。

由于智能合约的确定性特征，相同的指令序列无论在平台、架构和环境如何，总是涉及相同的状态变化集。Mythril和类似的分析工具结合符号和原生执行，对功能简练且资源有限的智能合约非常有效。Mythril操作“状态”的概念，其中包含合约代码、其环境、当前命令指针、存储和堆栈内容。以下是文档的描述：

```coffeescript
机器状态μ被定义为元组（g， pc， m， i， s），分别代表可用的gas、程序计数器pc ∈ P256、内存内容、活跃内存单词数量（从位置0起按连续计数）以及堆栈内容。
内存内容μm为一系列256大小的零。
```

状态变化图是我们主要的研究项目。如果分析执行成功，图表细节将包含在输出日志中。此外，Mythril还有 --graph 选项，可以以友好的可读格式构建此图。现在，了解了Mythril将如何工作后，我们来看看我们的合约，并找出为什么分析失败并返回 **[WARNING]:** 在合约创建执行过程中没有创建合约。首先，我调整了 --create-timeout 和 --max-depth 参数，按照建议。没有任何反应。我猜是要归咎于构造函数；我想其中出了问题。以下是代码：

```javascript
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) 异常会被返回。此外，只要 \_price <= \_cancellationFee，构造函数将持续失败，尽管Mythril尝试不同的 \_price 值。这个合约有十多个参数并拥有严格限制；因此，Mythril不可能猜出所有的有效组合。因此，它会试图转向下一个执行路径，筛选构造函数参数，但在给定的巨大参数组合中几乎没有机会做出正确的猜测。因此，合约上传失败，因为每个操作路径都会与某些 require(...) 相撞，我们面临上述问题。

现在我们有两个选择。第一个是将所有 require 关闭，通过注释将它们去掉。然后Mythril就能够使用任何参数组合来调用构造函数并成功运行。然而，使用随机参数意味着检测随机错误，这些错误是由于将无效值发送到构造函数造成的。简单来说，Mythril可以检测出一个错误，即合约创作者将 \_cancellationFee 定义为 \_mprice 的百万倍，但这个错误和合约对创作者是没有用的，并且Mythril只是浪费资源来发现这个错误。如果我们想要更全面的部署参数，显然在进行进一步分析时指定更真实的构造函数参数是有意义的，以防止Mythril搜索永远不会发生的错误，只要合约被正确部署。

我花了很多时间关闭和开启各种构造函数段，试图找出部署失败的地点。仿佛这些麻烦还不够，构造函数使用了 getCurrentTime() ，它返回当前时间，而在Mythril处理这个调用时完全不清楚。我将省略进一步的冒险细节，因为审计员很可能在常规使用过程中会亲自了解此事。因此，我选择了第二个选择：我从构造函数中去掉所有参数，甚至去掉 getCurrentTime()，直接在构造函数中硬编码所需的内容：

```cpp
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。根据参数使用的方式 [这里](https://github.com/ConsenSys/mythril-classic/blob/5e0bcd3f9fd98241475c6abaa1d4c2c0115954fa/mythril/laser/ethereum/strategy/__init__.py#L24) 可以看出，它是分析分支设置策略的一部分，默认值为无穷大（[代码见](https://github.com/ConsenSys/mythril-classic/blob/3093ed54b4f7c98187449adc3075b1f08bb723f0/mythril/laser/ethereum/svm.py#L51)）。你可以改变这个参数，但务必让你的合约被分析。在分析启动后，你将看到如下消息：

```css
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、自毁、assert 的分支，并检测其他特定的安全问题。因此，如果代码包含上述任何指令，Mythril会识别可能的执行分支，甚至显示所有导致它们的交易！首先，让我们看看Mythril为可怜的Booking合约准备了什么。第一个警告如下：

```coffeescript
==== 依赖可预测环境变量 ====
SWC ID: 116
严重性：低
合约：Booking
函数名称：fallback
PC地址：566
估计Gas用量：17908 - 61696
以太币的发送依赖于一个可预测的变量。
该合约发送以太币依赖于以下变量的值：
- block.timestamp
请注意，像coinbase、gaslimit、区块号和时间戳这样的变量的值是可预测的，或者可以被恶意矿工操控。
请勿将它们用于随机数生成或做出关键决策。
--------------------
在文件： contracts/flattened.sol:142

msg.sender.transfer(msg.value-m_price)
```

它发生在

```coffeescript
require(m_rentDateStart > getCurrentTime());
```

的fallback函数中。

请注意，Mythril发现 getCurrentTime() 中块时间戳的问题。广义上来说，这不是合约错误，但Mythril将块时间戳与以太传输相关联的确是非常好的一点！程序员应该清楚决策依赖于矿工控制的值。在未来的拍卖或其他竞争中，这会带来前置攻击的风险。

现在让我们看看如果我们在函数调用中隐藏一个变量，Mythril是否会识别出块时间戳的依赖关系：

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

+ function getCurrentTimeInner() internal returns (uint256) {
+     return now;
+ }
```

轰隆！Mythril仍然看到了块时间戳 - 以太传输之间的依赖关系，这对审计员来说至关重要。即使变化逻辑进行了几次状态更改，Mythril也能够追踪变量与决策之间的关系。尽管如此，Mythril并非无所不能，它并不能追踪所有可能的变量间相互依赖。如果我们继续使用 getCurrentTime() 函数并进行3级嵌套，警告将会消失。每一次函数调用都需要新的状态分支和对深度代码嵌套的巨大资源进行分析。我可能误用了分析参数，分析器也可能在某个深处识别出错误。正如我之前提到的，该产品正在积极开发中，同时在撰写本文时，在代码库中看到带有max-depth标签的提交。请不要对当前问题太过焦虑，我们已经找到了足够的证据，表明Mythril能够有效地跟踪变量依赖关系。

我们将添加一个随机以太发送的函数，即在合约处于State.PAID状态且客户已经支付了以太时，任何人都可以提取1/5的以太。函数如下：

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

Mythril检测到了这个问题：

```cpp
==== 未保护的以太取款 ====
SWC ID: 105
严重性：高
合约：Booking
函数名称：collectTaxes()
PC地址：2492
估计Gas用量：2135 - 2746
任何人都可以从合约账户中提取ETH。
除合约创作者以外的任意发送者都可以在未先向其发送等量ETH的情况下，从合约账户中提取ETH。
这可能是一个漏洞。
--------------------
在文件：contracts/flattened.sol:149

msg.sender.transfer(address(this).balance / 5)

--------------------
--------------------
交易序列：

{
    "2": {
        "calldata": "0x",
        "call_value": "0xde0b6b3a7640000",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    },
    "3": {
        "calldata": "0x01b613a5",
        "call_value": "0x0",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    }
}
```

这真不错，Mythril甚至显示了导致可能以太提取的2个交易！现在我们将State.PAID更改为State.RENT，如下所示：

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

现在只有当合约处于State.RENT状态且账户上没有余额时，collectTaxes()函数才可以被调用，因为合约已经将以太发送给所有者。这次Mythril并不会显示未保护的以太提取错误！onlyState(State.RENT)修饰符阻止分析器到达向非零账户余额发送以太的分支。Mythril尝试了不同的参数选项，但State.RENT仅在所有以太发送给所有者之后可用。因此，进入这个状态分支时余额不为零是不可行的，Mythril没有打扰审计员！

同样，Mythril将跟踪自毁和断言，向审计员展示可能导致合约破坏或重要功能故障的操作。我将略去这些示例，并建议测试一个类似的导致自毁的函数。

不要忘记，Mythril执行符号执行分析，这意味着在不模拟的情况下检查漏洞。例如，任何使用 "+", "-" 和其他算术操作的代码都可以被认为是 “整数溢出” 漏洞，如果操作数在任何程度上受到攻击者的控制。但正如我所说，Mythril最强大的功能是其符号和原生执行的结合以及对于逻辑分支值的检测。

## 结论

毫无疑问，单篇文章无法足够全面地描述Mythril能够检测的一系列问题。更何况它在真实的区块链环境中工作，通过签名发现必要的合约和漏洞，构建漂亮的调用图并编辑报告。Mythril允许以基于Python的接口编写个性化测试脚本，轻松测试特定功能，修复参数值，甚至引入自定义策略来处理反汇编代码。

与IDA Pro相比，Mythril仍然是一个年轻的软件，几乎没有文档，除了少数几篇文章。许多Mythril参数只在代码中有所描述（从 [cli.py](https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/interfaces/cli.py) 开始）。我希望很快会出现完整、详尽的文档，并描述参数。

当合约相对较大时，显示的错误堆积占据了大量空间。希望关于检测到的错误的压缩数据可以提供。在使用Mythril时，需要跟踪进度、测试过的合约，并在必要时故意删除审计员已知的假阳性错误。

总的来说，Mythril是一个出色且非常强大的智能合约分析工具。每位审计员都应该使用它，因为它关注代码中的关键部分，并检测变量之间的隐藏联系。

总结一下，关于使用Mythril的建议如下：

这个错误是通过Echidna模糊测试工具发现的。

我们在abs函数中对类型(int256).min值进行了回退，因为int256的范围为 \$-2^{255}\$… \$2^{255} - 1\$。

- 谁是MixBytes？

[MixBytes](https://mixbytes.io/) 是一支专业的区块链审计师和安全研究人员团队，专注于为EVM兼容和Substrate基础的项目提供全面的智能合约审计及技术咨询服务。加入我们在 [X](https://twitter.com/MixBytes) 的社交媒体，一起关注行业最新趋势和见解。

>- 原文链接： [mixbytes.io/blog/guide-s...](https://mixbytes.io/blog/guide-smart-contract-security-tools-mythril)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

作者：MixBytes团队

警告

配置和预启动

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），我将按照上次的方式解决它：在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

docker run -v $(pwd):/tmp -w /tmp myth:latest -x
contracts/flattened.sol:Booking -v4 --verbose-report

合约启动和部署

在运行合约后，我们收到以下消息：

mythril.laser.ethereum.svm [WARNING]:
在合约创建执行过程中没有创建合约
增加创建执行的资源（--max-depth或--create-timeout）
分析成功完成。未检测到问题。

结果我们合约没有在模拟器中被 “部署”。因此我建议在所有分析中使用 -v4 标志，以免错过重要信息。让我们弄清楚出了什么问题。这个实际问题的解决将帮助我们了解如何正确运行Mythril。Mythril指南说：“它使用共符号分析、污点分析和控制流检查来检测各种安全漏洞。”如果你对这些术语不熟悉，我建议阅读关于共符号测试的维基文章，以及关于污点检查针对x86的精彩演示。简而言之，Mythril模拟合约执行，存储所有执行分支，并努力通过尝试不同的参数组合和可能的选项来达到“危险”的合约状态。粗略的过程如下（详见上述文章）：

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

简单来说，Mythril遍历分支并检测输入值的组合，以便能够到达它们。通过了解哪些分支可追踪以断言、转账、自毁和其它危险操作码，Mythril检测影响执行安全的输入值和交易组合。Mythril独特之处在于其切断从未控制的分支并分析控制流的方法。要深入了解Mythril的底层运作，请点击这里。

机器状态μ被定义为元组（g， pc， m， i， s），分别代表可用的gas、程序计数器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 &lt; _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) 异常会被返回。此外，只要 _price <= _cancellationFee，构造函数将持续失败，尽管Mythril尝试不同的 _price 值。这个合约有十多个参数并拥有严格限制；因此，Mythril不可能猜出所有的有效组合。因此，它会试图转向下一个执行路径，筛选构造函数参数，但在给定的巨大参数组合中几乎没有机会做出正确的猜测。因此，合约上传失败，因为每个操作路径都会与某些 require(...) 相撞，我们面临上述问题。

现在我们有两个选择。第一个是将所有 require 关闭，通过注释将它们去掉。然后Mythril就能够使用任何参数组合来调用构造函数并成功运行。然而，使用随机参数意味着检测随机错误，这些错误是由于将无效值发送到构造函数造成的。简单来说，Mythril可以检测出一个错误，即合约创作者将 _cancellationFee 定义为 _mprice 的百万倍，但这个错误和合约对创作者是没有用的，并且Mythril只是浪费资源来发现这个错误。如果我们想要更全面的部署参数，显然在进行进一步分析时指定更真实的构造函数参数是有意义的，以防止Mythril搜索永远不会发生的错误，只要合约被正确部署。

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) &lt; 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上，审计更大的合约也需要时间。

错误搜索

==== 依赖可预测环境变量 ====
SWC ID: 116
严重性：低
合约：Booking
函数名称：fallback
PC地址：566
估计Gas用量：17908 - 61696
以太币的发送依赖于一个可预测的变量。
该合约发送以太币依赖于以下变量的值：
- block.timestamp
请注意，像coinbase、gaslimit、区块号和时间戳这样的变量的值是可预测的，或者可以被恶意矿工操控。
请勿将它们用于随机数生成或做出关键决策。
--------------------
在文件： contracts/flattened.sol:142

msg.sender.transfer(msg.value-m_price)

它发生在

require(m_rentDateStart > getCurrentTime());

的fallback函数中。

现在让我们看看如果我们在函数调用中隐藏一个变量，Mythril是否会识别出块时间戳的依赖关系：

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

+ function getCurrentTimeInner() internal returns (uint256) {
+     return now;
+ }

我们将添加一个随机以太发送的函数，即在合约处于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
估计Gas用量：2135 - 2746
任何人都可以从合约账户中提取ETH。
除合约创作者以外的任意发送者都可以在未先向其发送等量ETH的情况下，从合约账户中提取ETH。
这可能是一个漏洞。
--------------------
在文件：contracts/flattened.sol:149

msg.sender.transfer(address(this).balance / 5)

--------------------
--------------------
交易序列：

{
    "2": {
        "calldata": "0x",
        "call_value": "0xde0b6b3a7640000",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    },
    "3": {
        "calldata": "0x01b613a5",
        "call_value": "0x0",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    }
}

这真不错，Mythril甚至显示了导致可能以太提取的2个交易！现在我们将State.PAID更改为State.RENT，如下所示：

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

同样，Mythril将跟踪自毁和断言，向审计员展示可能导致合约破坏或重要功能故障的操作。我将略去这些示例，并建议测试一个类似的导致自毁的函数。

结论

与IDA Pro相比，Mythril仍然是一个年轻的软件，几乎没有文档，除了少数几篇文章。许多Mythril参数只在代码中有所描述（从 cli.py 开始）。我希望很快会出现完整、详尽的文档，并描述参数。

总的来说，Mythril是一个出色且非常强大的智能合约分析工具。每位审计员都应该使用它，因为它关注代码中的关键部分，并检测变量之间的隐藏联系。

总结一下，关于使用Mythril的建议如下：

这个错误是通过Echidna模糊测试工具发现的。

我们在abs函数中对类型(int256).min值进行了回退，因为int256的范围为 $-2^{255}$… $2^{255} - 1$。

谁是MixBytes？

MixBytes 是一支专业的区块链审计师和安全研究人员团队，专注于为EVM兼容和Substrate基础的项目提供全面的智能合约审计及技术咨询服务。加入我们在 X 的社交媒体，一起关注行业最新趋势和见解。

原文链接： mixbytes.io/blog/guide-s...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

智能合约安全工具实用指南

警告

配置和预启动

合约启动和部署

错误搜索

结论

0 条评论

文章目录