混合模糊测试：强化Echidna的尖刺

智能合约模糊测试是一种有效的漏洞发现技术，在Trail of Bits的审计过程中被广泛使用。在我实习期间，我致力于扩展我们的模糊测试能力，开发了Hybrid Echidna——一种“混合模糊测试器”，它将我们的智能合约模糊测试器Echidna与符号执行框架Maat结合，以改进漏洞发现过程。虽然Echidna是一个优秀的工具，但它仍然难以发现某些漏洞。通过Hybrid Echidna，我们增强了过程，发现了更多漏洞！

在本文中，我们将看一个包含漏洞的合约示例，这些漏洞只能通过非常特定的256位整数输入（例如0xee250cacdb8de774585208b1e85445fca3bd09da95683133ed06742b71ec2434）触发。我们将首先展示使用随机模糊测试技术的Echidna如何难以发现这些漏洞。然后，我们将检查Hybrid Echidna如何改进传统随机模糊测试，并亲自查看结果！

问题

以下合约包含两个漏洞（表示为断言失败）。触发这些漏洞需要找到由特定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
    |        }
    |    }
    | }

Echidna可以成功发现漏洞（并且在许多情况下已经发现），归根结底，发现的漏洞就是发现的漏洞。然而，如本例所示，其结果可以改进。你问如何？好吧，如果只有工具的变异，某种弗兰肯斯坦版本，将Echidna与能够锐化其能力的东西结合，形成一个超级漏洞发现器——比如Hybrid Echidna。

Hybrid Echidna来救援

注意：如果你想跟随这里，请通过运行以下命令安装Optik工具套件：

1

pip install optik-tools

Hybrid Echidna是Optik的一部分，Optik是一套用于分析以太坊智能合约的新工具。Optik旨在包括独立工具和改进现有工具（通常是模糊测试器）以动态分析智能合约的工具。到目前为止，其唯一工具是Hybrid Echidna，它通过将Echidna与Maat（一个也是由Trail of Bits内部开发的符号执行框架）结合来改进Echidna。在夏天开始时，Hybrid Echidna代码库是一个最小化的代码库，只运行Echidna。现在，Hybrid Echidna是一个完整的工具（尽管仍在开发中）， consistently improves upon Echidna.

它是如何工作的？

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

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

因此，Hybrid Echidna获取Echidna找到的数据，使用Maat找出如何更改其输入以到达困难路径，然后再次模糊测试程序（使用新发现的输入），直到无法改进发现。将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函数中。

我们可以快速验证触发这些失败的输入（显示在“结果”部分）。取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，并告诉我们您的想法！

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News