混合模糊测试：提升Echidna的检测能力

智能合约模糊测试是一种有效的漏洞发现技术，在Trail of Bits的审计工作中被广泛使用。在我的实习期间，我参与了Hybrid Echidna的开发工作，这是一个"混合模糊测试器"，将我们的智能合约模糊测试器Echidna与符号执行框架Maat相结合，以改进漏洞发现过程。

Echidna的局限性

Echidna是Trail of Bits开发的基于属性的模糊测试器，广泛用于智能合约漏洞挖掘。它属于"智能模糊测试器"类别，使用合约的ABI并对其源代码进行静态分析，以决定如何最佳生成输入数据。

然而，Echidna在发现某些特定漏洞时仍存在困难。例如，考虑以下包含两个漏洞的合约：

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

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
       }
   }
}

触发这些漏洞需要找到特定的256位整数输入，随机找到正确输入的概率极低（1/2²⁵⁶），这意味着仅依靠随机模糊测试几乎不可能发现这些漏洞。

Hybrid Echidna的解决方案

Hybrid Echidna是Optik工具套件的一部分，Optik是一套用于分析以太坊智能合约的新工具集。它通过将Echidna与Maat符号执行框架相结合来提升检测能力。

工作原理

Hybrid Echidna的工作流程如下：

1. 执行Echidna的初始运行以收集模糊测试语料库
2. 对发现的每个独特输入，使用该输入符号执行合约并记录其覆盖率
3. 检查覆盖率信息以发现遗漏的路径
4. 使用Maat为这些路径求解输入，并记录可能导致执行遗漏路径的新输入
5. 重复此过程，直到找不到更多输入

实际效果

在测试前述漏洞合约时，Hybrid Echidna表现出色：

• 发现了7个独特输入（5个通过模糊测试，2个通过符号执行）
• 其中2个输入导致了断言失败（即漏洞）
• 断言失败发生在func_one和func_two函数中

通过验证，Hybrid Echidna确实找到了满足特定条件的输入，显著提升了检测能力。

未来展望

尽管Hybrid Echidna目前还存在一些限制（如不支持符号keccak操作、无法考虑gas使用等），但我们已经看到了令人鼓舞的结果。这些结果增强了我们对模糊测试方法的信心。

Optik仍在积极开发中。未来，我们计划改进项目的符号执行器，更重要的是通过在真实代码库上进行测试来提高Hybrid Echidna的可扩展性。我们的最终目标是让Trail of Bits的每位工程师在审计智能合约时都能使用Hybrid Echidna。