混合模糊测试：强化Echidna的漏洞挖掘能力

智能合约模糊测试是Trail of Bits在审计中广泛使用的高效漏洞发现技术。在实习期间，我通过开发Hybrid Echidna扩展了我们的模糊测试能力——这是一个将智能合约模糊测试器Echidna与符号执行框架Maat结合的“混合模糊测试器”，能显著提升漏洞发现效率。尽管Echidna已是优秀工具，但仍难以发现某些特定漏洞，而Hybrid Echidna能帮助我们发现更多！

Echidna是Trail of Bits开发的基于属性的模糊测试器，广泛应用于智能合约漏洞挖掘。它属于“智能模糊测试器”类别，利用合约ABI并对源代码进行静态分析，以优化输入数据的生成策略。

问题案例

以下合约包含两个漏洞（表现为断言失败）。触发漏洞需要找到特定的256位整数输入（如0xee250cacdb8de774585208b1e85445fca3bd09da95683133ed06742b71ec2434），这些输入未硬编码在合约中。随机找到正确输入的概率为1/115792089237316195423570985008687907853269984665640564039457584007913129639936——这意味着仅依赖随机模糊测试几乎不可能发现这些漏洞。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14


pragma solidity ^0.7.1;

contract VulnerableContract {
   function func_one(int128 x) public pure {
       if (x / 4 == -20) {
           assert(false); // BUG
       }
   }
   function func_two(int128 x) public pure {
       if ((x >> 30) / 7 == 2) {
           assert(false); // BUG
       }
   }
}

使用Echidna测试该合约（执行命令：echidna VulnerableContract.sol --test-mode assertion）后，虽然工具识别了三个“有趣”输入并添加到测试语料库，但均未触发断言失败。从覆盖率文件可清晰看到未覆盖的代码路径：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16


| pragma solidity ^0.7.1;
*r  |
| contract VulnerableContract {
|
*   |    function func_one(int128 x) public pure {
*   |        if (x / 4 == -20) {
|            assert(false); // BUG
|        }
|    }
|
*   |    function func_two(int128 x) public pure {
*   |        if ((x >> 30) / 7 == 2) {
|            assert(false); // BUG
|        }
|    }
| }

Hybrid Echidna的解决方案

Hybrid Echidna是Optik工具套件的组成部分，该套件专用于以太坊智能合约分析。Optik包含独立工具和增强现有工具（通常是模糊测试器）的动态分析工具。目前其核心工具Hybrid Echidna通过整合Trail of Bits自主研发的符号执行框架Maat来增强Echidna。

工作原理

执行初始Echidna运行以收集测试语料库
对每个独特输入进行符号执行并记录覆盖率
分析覆盖率数据识别未覆盖路径
使用Maat求解未覆盖路径的输入
循环该过程直至无法发现新输入

Hybrid Echidna如同让Echidna在《谁想成为百万富翁》中拥有无限次“求助好友”Maat的能力。

实战演示

使用以下命令运行Hybrid Echidna：

1

hybrid-echidna VulnerableContract.sol --test-mode assertion --corpus-dir hybrid_echidna_output --contract VulnerableContract

结果显著提升：

发现7个独特输入（5个通过模糊测试，2个通过符号执行）
其中2个输入触发断言失败
漏洞分别出现在func_one和func_two函数

例如对func_one的输入15032385536验证：

1
2


$ python -c 'print((15032385536 >> 30) // 7)'
2

未来规划

尽管当前存在局限性（如不支持符号化keccak操作、未考虑gas消耗），Hybrid Echidna已展现出巨大潜力。我们将持续改进符号执行器，并通过真实代码库测试提升工具的可扩展性，最终目标是让Trail of Bits的所有工程师在审计智能合约时都能使用Hybrid Echidna。

欢迎尝试安装Optik并测试Hybrid Echidna：

1

pip install optik-tools