跳转至主要内容

如何使用 Echidna 测试智能合约

solidity智能合同安全性测试模糊测试
中级
Trailofbits
构建安全的合约(opens in a new tab)
2020年4月10日
18 分钟阅读 minute read

安装

Echidna 可以通过 docker 或使用预编译的二进制程序安装。

通过 docker 安装 Echidna

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

最后一个命令在有权访问当前目录的 docker 中运行 eth-security-toolbox。 您可以从主机更改文件，并在 docker 中对文件运行工具

在 docker 中，运行：

solc-select 0.5.11
cd /home/training

通过二进制程序安装

https://github.com/crytic/echidna/releases/tag/v1.4.0.0(opens in a new tab)

基于属性的模糊测试简介

Echidna 是一个模糊测试工具，我们在之前的博客中描述过（1(opens in a new tab)、2(opens in a new tab)、3(opens in a new tab)）。

模糊测试

模糊测试(opens in a new tab)是一项在安全技术领域广为人知的技术。 它依靠生成或多或少数量的随机输入值来测试程序中的错误。 传统软件中的模糊测试工具（例如 AFL(opens in a new tab) 或 LibFuzzer(opens in a new tab)）是发现错误的有效工具。

除了完全随机生成输入值外，还有很多其他的技巧和策略来生成足够好的输入，包括：

  • 从每次执行中获取反馈，并使用反馈来指导输入的生成。 例如，如果新生成的输入导致发现一条新的路径，那么，生成接近该路径的新输入是有意义的。
  • 根据结构限制生成输入。 例如，如果您的输入包含一个带有校验和的报文头，则让模糊测试工具生成能够验证校验和的输入将会是很有意义的。
  • 使用已知输入生成新输入：如果您有权访问一个有效输入的大型数据集， 则模糊测试工具可以从中生成新的输入，而不是从头开始生成。 这些通常称为 种子。

基于属性的模糊测试

Echidna 属于一种特定的模糊测试工具系列：基于属性的模糊测试，很大程度上受到了 QuickCheck(opens in a new tab) 的启发。 与尝试查找崩溃的经典模糊测试工具不同，Echedna 会试图去改变用户定义的不变量。

在智能合约中，不变量是 Solidity 函数，可以表示合约可能达到的任何错误或无效状态，包括：

  • 不正确的访问控制：攻击者变成了合约的所有者。
  • 不正确的状态机：合约暂停时代币仍然可以传输。
  • 不正确的算法：用户可以余额不足的情况下获得无限的免费代币。

使用 Echidna 测试属性

我们来看看如何使用 Echidna 测试智能合约。 目标是以下智能合约 token.sol(opens in a new tab)：

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
显示全部
 复制

我们假定此代币必须具有以下属性：

  • 任何人最多可以持有 1000 代币
  • 代币不能转移（它不是 ERC20 代币）

写入属性

Echidna 的属性是 Solidity 函数。 一个属性必须：

  • 没有任何参数
  • 如果成功就返回 true
  • 其名字以 echidna 开头

Echidna 将：

  • 自动生成任意交易来测试属性。
  • 报告导致属性返回 false 或引发错误的任何交易。
  • 调用属性时丢弃负面影响（即，如果属性改变了一个状态变量，则在测试后会被丢弃）

以下属性会检查调用者持有的代币是否不超过 1000 个：

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}
 复制

使用继承将合约与属性分开：

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }
 复制

token.sol(opens in a new tab) 实现了这个属性并继承了代币。

初始化合约

Echidna 需要一个无参 构造函数。 如果您的合约需要特定的初始化，则需要相应地改变构造函数。

Echidna 中有一些特定的地址：

  • 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 用于调用构造函数。
  • 0x10000、0x20000 和 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 用于随机调用其他函数。

在当前的示例中，我们不需要进行任何特定的初始化，因为我们的构造函数是空的。

运行 Echidna

用此命令启动 Echidna：

echidna-test contract.sol

如果 contract.sol 包含多个合约，您可以指定目标合约：

echidna-test contract.sol --contract MyContract

总结：测试属性

下面总结了我们示例中 Echidna 的运行情况：

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }
 复制
echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
显示全部

如果 backdoor 被调用，Echidna 会发现与该属性发生冲突。

过滤在模糊测试期间要调用的函数

我们来了解如何过滤要进行模糊测试的函数。 目标是以下智能合约：

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
显示全部
 复制

这个小例子迫使 Echidna 找到特定的交易序列来改变一个状态变量。 这对一个模糊测试工具来说很困难（建议使用符号执行工具，比如 Manticore(opens in a new tab)）。 我们可以运行 Echidna 对此进行验证：

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

过滤函数

Echidna 很难找到测试此合约的正确序列，因为两个重置函数（reset1 和 reset2）会将所有状态变量设置为 false。 但是，我们可以使用特殊的 Echidna 功能将重置函数列入黑名单，或者仅将 f、g、h 和 i 列入白名单。

要将函数列入黑名单，我们可以使用下面这个配置文件：

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

过滤函数的另一个方法是列出白名单里的函数。 为此，我们可以使用下面这个配置文件：

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]
  • 默认情况下，filterBlacklist 为 true。
  • 只能通过名字进行过滤（不带参数）。 如果您有 f() 和 f(uint256) 两个函数，则过滤器 "f" 会匹配出这两个函数。

运行 Echidna

使用配置文件 blacklist.yaml 运行 Echidna：

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

Echidna 几乎立刻就可以找到伪造属性的交易序列。

总结：过滤函数

在模糊测试期间，Echidna 可以将要调用的黑名单或白名单函数列入黑名单或白名单，方法是：

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]
echidna-test contract.sol --config config.yaml
...

根据 filterBlacklist 布尔值的不同，Echidna 开始进行模糊测试时，要么将 f1、f2 和 f3 列入黑名单，要么只调用它们。

如何使用 Echidna 测试 Solidity 的断言

在这个简短的教程中，我们将演示如何使用 Echidna 测试合约中的断言检查。 假设我们有这样一个合约：

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
显示全部
 复制

写一个断言：

我们要确保 tmp 返回其差值之后，小于或等于 counter。 我们可以写一个 Echidna 属性，但我们需要将 tmp 值保存某处。 相反，我们可以使用如下断言：

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
显示全部
 复制

运行 Echidna

要启用断言失败测试，请创建 Echidna 配置文件(opens in a new tab) config.yaml：

1checkAsserts: true

当我们在 Echidna 上运行这个合约时，我们会获得预期的结果：

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
显示全部

正如您所见，Echidna 在 inc 函数中报告了一些断言失败。 每个函数可以添加多个断言，但 Echidna 无法判断哪个断言失败了。

使用断言的时机和方式

断言可以用作显示属性的替代项，特别是如果要检查的条件与某些操作 f 的正确使用直接相关。 在某些代码之后添加断言将强制在代码执行后立即进行检查：

1function f(..) public {
2    // some complex code
3    ...
4    assert (condition);
5    ...
6}
7
 复制

相反， 使用显式的 Echidna 属性将随机执行交易，无法轻松地强制要求何时对其进行检查。 但还是可以做以下变通的：

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}
 复制

但是，也存在一些问题：

  • 如果 f 被声明为 internal 或 external 则失败.
  • 不清楚应该使用哪些参数来调用 f。
  • 如果 f 回滚，属性将会失败。

一般来说，我们建议遵循 John Regehr 关于如何使用断言的建议(opens in a new tab)：

  • 在进行断言检查时不要强制任何负面影响。 例如： assert(ChangeStateAndReturn() == 1)
  • 不要断言明显的语句。 例如， 在 assert(var >= 0) 中，var 被声明为 uint。

最后，请不要使用 require 代替 assert，因为 Echidna 将无法检测到它（但合约仍将回滚）。

总结：断言检查

下面总结了我们示例中 Echidna 的运行情况：

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
显示全部
 复制
echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
显示全部

Echidna 发现，如果使用大参数多次调用此函数，inc 中的断言可能会失败。

收集和修改 Echidna 预料库

我们来了解如何用 Echidna 收集和使用交易语料库。 目标是以下智能合约 magic.sol(opens in a new tab)：

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
显示全部
 复制

这个小例子迫使 Echidna 找到一系列交易来改变一个状态变量。 这对一个模糊测试工具来说很困难（建议使用符号执行工具，比如 Manticore(opens in a new tab)）。 我们可以运行 Echidna 对此进行验证：

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
Seed: 2221503356319272685

然而，当我们运行该模糊测试活动时，我们仍然可以使用 Echidna 来收集语料库。

收集语料库

为了启用语料库的收集，请创建一个语料目录：

mkdir corpus-magic

和一个 Echidna 配置文件(opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

现在，我们可以运行工具并检查收集到的语料库：

echidna-test magic.sol --config config.yaml

Echidna 仍然找不到正确的 magic 值，但我们可以看一看它收集到的语料库。 例如，其中一个文件是：

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
显示全部
 复制

显然，此输入不会触发我们属性中的故障。 但是，在下一步，我们将看到如何对此进行修改。

为语料库生成种子

Echidna 需要一些帮助才能处理 magic 函数。 我们将复制和修改输入以使用其合适的参数：

cp corpus/2712688662897926208.txt corpus/new.txt

我们将修改 new.txt 来调用 magic(42,129,333,0)。 现在，我们可以重新运行 Echidna：

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
显示全部

这一次，它立即发现与该属性发生了冲突。

查找消耗大量 gas 的交易

我们来看看如何使用 Echidna 查找燃料消耗大的交易。 目标是以下智能合约：

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
显示全部
 复制

这里的 expensive 可能会消耗大量 gas。

目前，Echidna 总是需要一个属性来测试：这里 echidna_test 始终返回 true。 我们可以运行 Echidna 对此进行验证：

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

测量 gas 消耗

要使用 Echidna 测量燃料消耗，请创建配置文件 config.yaml：

1estimateGas: true

在这个例子中，我们还将减少交易序列的大小，以使结果更易于理解：

1seqLen: 2
2estimateGas: true

Run Echidna

创建好配置文件之后，我们就可以这样运行 Echidna：

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
显示全部

过滤掉 gas 消耗减少的调用

以上关于在模糊测试活动期间过滤要调用的函数的教程展示了如何从测试中删除一些函数。
这对于获得准确的 gas 消耗至关重要。 请考虑下面的示例：

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
显示全部
 复制

如果 Echidna 可以调用所有函数，它将无法轻松找到消耗大量 gas 的交易：

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
显示全部

这是因为成本取决于 addrs 的大小，而随机调用往往会使数组几乎为空。 将 pop 和 clear 加入黑名单却给我们带来了更好的结果:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]
1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

总结：查找消耗大量 gas 的交易

Echidna 可以使用 estimateGas 配置选项找到消耗大量 gas 的交易：

1estimateGas: true
echidna-test contract.sol --config config.yaml
...

模糊测试结束后，Echidna 将报告每个函数中消耗 gas 最多的交易。

上次修改时间: @Chenguang(opens in a new tab), 2023年8月15日

本教程对你有帮助吗？