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

智能合约模糊测试是一种有效的漏洞发现技术，在Trail of Bits的审计工作中被广泛使用。在我实习期间，我参与了Hybrid Echidna的开发工作，这是一个"混合模糊测试器"，将我们的智能合约模糊测试器Echidna与符号执行框架Maat相结合，以改进漏洞发现过程。虽然Echidna是一个优秀的工具，但在发现某些漏洞方面仍存在困难。通过Hybrid Echidna，我们能够发现更多漏洞！

Echidna简介

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

问题描述

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

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

当我们对合约运行Echidna时（通过执行命令echidna VulnerableContract.sol --test-mode assertion），它会在本地保存一些发现的信息。友好的ncurses风格界面会显示摘要，如下图所示：

虽然Echidna识别了三个"有趣"的输入并将其添加到模糊测试语料库中，但没有一个导致断言失败（即漏洞）。换句话说，Echidna未能触发合约中的漏洞。

发生这种情况的原因是Echidna无法找到满足触发漏洞执行路径所需条件的输入。这是可以理解的，因为漏洞条件是算术方程，而Echidna在解决这类方程方面的智能程度有限。查看Echidna生成的覆盖率文件，我们可以清楚地看到未覆盖的代码路径：

 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是一套用于分析以太坊智能合约的新工具套件。Optik旨在包含独立工具和改进现有工具（通常是模糊测试器）的工具，用于动态分析智能合约。到目前为止，它的唯一工具是Hybrid Echidna，它通过将Echidna与Maat（Trail of Bits内部开发的符号执行框架）相结合来改进Echidna。

工作原理

从高层次来看，Hybrid Echidna只是多次运行Echidna，将这些运行与符号分析交织在一起以生成新的模糊测试输入。现在，模糊测试合约的更深入过程如下：

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

因此，Hybrid Echidna获取Echidna发现的数据，使用Maat找出如何更改其输入以到达困难路径，然后再次模糊测试程序（使用新发现的输入），直到无法改进发现结果。

实际演示

让我们重新审视之前查看的合约——那个Echidna忽略了两个漏洞的合约——看看Hybrid Echidna的表现如何。

我们使用以下命令运行Hybrid Echidna：

1

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

运行Hybrid Echidna时，我们会看到另一个友好的UI，提供对其性能的洞察。这包括时间信息和以下关键要点：

Hybrid Echidna找到了七个独特输入（五个通过模糊测试，两个通过符号执行）
其中两个输入导致断言失败（即漏洞）
断言失败发生在func_one和func_two函数中

我们可以快速验证触发这些失败的输入（显示在"Results"部分）。以Hybrid Echidna对func_one的输入15032385536为例，回想一下结果为2表示断言失败：

1
2


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

正如我们所看到的，Hybrid Echidna找到了满足func_one中非常特定条件的随机输入，改进了Echidna的性能。换句话说，它发现了更多漏洞！

未来展望

尽管存在当前的局限性（例如缺乏对符号keccak操作的支持和无法考虑gas使用情况），但我们已经看到了Hybrid Echidna的有希望的结果。这些结果增强了我们对模糊测试方法的信心，并使我们希望在将来分享更多令人兴奋的结果。

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

尝试安装Optik并在VulnerableContract.sol示例（或您自己的合约）上测试Hybrid Echidna，并告诉我们您的想法！

混合模糊测试：提升Echidna智能合约漏洞检测能力

本文介绍了Trail of Bits开发的混合模糊测试工具Hybrid Echidna，它结合了Echidna模糊测试和Maat符号执行框架，能有效发现传统方法难以检测的智能合约漏洞，并通过具体案例展示了其优势。