Echidna 验证与探索模式：利用 hevm 增强的符号执行

+++ title = "Echidna 进入符号执行的新纪元" date = "2025-08-19" description = "一篇描述 Echidna 新的符号执行能力的博客文章，包括初步结果和近期未来" tags = [ "echidna", "symbolic-execution", "fuzzing" ] +++

在这篇文章中，我们将了解使用来自 hevm 的增强型符号执行的 Echidna 的一些新功能。简而言之，符号执行的工作方式与模糊测试相同，检查程序是否存在特定问题，例如断言失败。但是，与模糊测试不同，它要么通过显示没有路径会导致这些问题来确认程序可以正常工作，要么它会找到证明此类问题存在的例子。Echidna 符号执行功能的初始实现已于去年添加，但在合并了PR 1349之后，最近进行了巩固，该版本以两种“风格”实现了符号执行：

• 无状态测试的验证模式：此模式旨在证明不存在错误，与 hevm、Halmos 和 Certora 等工具保持一致。
• 有状态测试的探索模式：此模式将符号执行与模糊测试相结合，以识别涉及状态更改的场景中的断言失败。

将符号执行集成到 Echidna 中的关键原则是：漏洞研究工具应最大限度地减少对用户的要求。在智能合约安全性的上下文中，这意味着不需要新的作弊码或专门的测试，只需与传统模糊测试活动中使用的相同的代码库即可。

在深入研究之前，我们要感谢 hevm 团队 过去一年所做的出色工作。他们在 最近的发布 中详细介绍了符号执行性能和功能的改进，这对于与 Echidna 等工具实现无缝集成至关重要。

验证模式

验证模式类似于应用于无状态（或单笔交易）代码的形式验证技术。在 Echidna 的新验证模式中，该工具通过首先执行其构造函数，然后以符号方式测试每个方法来分析合约。这种方法非常适合完全无状态的函数（例如，数学逻辑），但也可以像 Halmos 的方法 一样，策略性地用于有状态代码中。

当使用验证模式下的符号引擎探索测试时，会产生一些可能的结果：

• 已验证 ✅ 代码已完全探索，翻译或解决问题期间没有任何问题。正如预期的那样，没有反例。
• 已通过 👍 代码已完全探索，没有检测到任何反例，但 SMT 求解器无法确定某些查询的答案（例如，超时），因此断言可能仍然会失败。
• 失败 💥 探索揭示了一个反例，该反例已在具体模式下成功重放。
• 错误 ❌ 错误或缺少的功能阻止了某些路径的探索或解决。
• 超时 ⏳ 存在可扩展性问题，阻止了创建模型来探索所有程序路径。

因此，当交易在验证期间检出时，以下是幕后发生的事情：

• 完全覆盖检查：该工具基本上检查了合约在构造函数完成使用单个交易后可能采取的每条路径。如果你曾经调整合约代码，则需要从头开始重新启动整个检查。
• 未找到反例：你的断言应该成立！
• 外部调用：如果你的合约可以调用任意地址，我们只会查看你在测试中实际部署的地址。这意味着我们无法检测到源自你正在测试的合约之外的合约的潜在重入攻击。
• 细则：所有 calldata 参数、msg.sender、msg.value、block.timestamp 和 block.number 都被视为符号变量，允许分析探索所有可能的值。
  • 发送者地址仅限于你在测试配置中指定的地址（如所有者和非所有者帐户）。如果你需要使用其他地址进行测试，请确保它们在你的配置中！
  • 交易价值不能超过你在配置文件中指定的最大值。
  • 它将考虑的最大时间戳和区块号跳跃恰好是你在配置中设置的跳跃。如果你的测试需要更大的更改，你需要更新这些值
  • 为了简化分析，hevm 默认假设无限 gas。这意味着解决方案可能包括需要不切实际的 gas 限制的场景，这可能不切实际。但是，这种过度近似确保不会遗漏任何有效的发现，即使某些理论结果过于乐观。

我们决定对 Algebra 最近的一项活动进行试驾，其中包含许多无状态测试。所有测试均在使用 10 个求解器（bitwuzla 0.7）的 MacBook Pro M4 Max 上进行：

<details>

<summary>点击我查看结果</summary>

</details>

正如你所看到的，还有很长的路要走，但很明显，符号执行工具开始变得足够成熟，可以处理实际代码，即使它们需要花费一些时间。请记住，所需的时间存在很大的差异，因为对于简单的代码，时间范围从几秒钟到最复杂的情况下的几个小时或几天。

是否可以实际证明现在通过的大多数不变量？当 hevm 借助 “just solve it” 等工具同时切换为使用多个 SMT 求解器时，很有可能做到这一点，特别是对于少数查询超时的不变量。最重要的是，虽然我们在这些实验中没有发现失败的属性，但还有更多值得关注的地方：从本质上讲，我们能够在不以任何方式更改测试的情况下提供超出模糊测试的保证，这非常有价值。

符号执行免责声明

重要的是要讨论在实践中验证的含义。你可能知道，形式验证很少是完全万无一失的：有许多需要考虑的缺点和限制，这些缺点和限制来自理论（例如，keccak256 哈希很难反转）和实践（例如，SMT 求解器可能会卡住）。这就是为什么使用符号执行的工具的输出反映任何潜在的缺点或限制非常重要，因为开发人员可能会错误地将其解释为“这里没有错误”。在最近的 Galois 博客文章 “What Works and Doesn't Selling Formal Methods” 中有一个有趣的讨论。hevm 和 halmos 文档描述了在 EVM 中进行符号执行时需要考虑的一些事项。

我们还想强调的是，鉴于当前工具的状态，不建议尝试验证具有无限循环的代码，包括任何将动态数据结构作为输入（例如，bytes）的函数。事实上，Echidna 不会对任何将动态数据结构作为输入的函数执行符号执行。虽然有一些技术可以具体化它们的大小，但需要小心使用它们，以避免在代码验证过程中出现盲点。

探索模式

这种模式对区块链来说有点新。这种模式结合了传统的模糊测试和符号执行，试图发现触发断言失败的新输入，其灵感来自 Driller (2016) 等开创性研究。 通常，FV 工具将从合约的部署状态开始工作，并尝试执行多个符号执行交易，以便逐步达到越来越深的状态：

这种方法的直接问题是，每个符号交易的状态数量都会趋于增长，从而使得每个新的约束条件集越来越难以解决。FV 工具使用许多技巧来减少可能的交易组合（例如，分析插槽的读取/写入方式）

另一方面，模糊测试工具使用具体交易探索合约状态。在这里，我们考虑一个可以包含许多交易的语料库，但仅显示第一个交易：

模糊测试的直接问题是，到达断言失败需要大量的“运气”，这取决于如何为当前语料库构建状态。Echidna 使用符号执行的探索模式允许结合这两种方法，依赖于随着时间积累的语料库，但在其之上执行单个符号执行交易。

效果是执行潜在的更具可扩展性的交易，但我们减少了对运气的依赖，因为符号执行器将更详尽地探索该特定状态。

作为符号执行能力的示例，让我们看一下这段代码，该代码显示了一个 ERC4626 金库的示例，该金库聚合了其他三个金库：

contract MultiVault {
    uint256 internal vaultNumber;
    uint256[3] internal vaultBalance;
    uint256 internal minSupply = 100 ** 18;

    function sqrt(uint x) internal returns (uint y) {
        uint z = (x + 1) / 2;
        y = x;
        while (z < y) {
            y = z;
            z = (x / z + z) / 2;
        }
    }

    function addVault(uint128 supply, uint8 decimals) public {
        require(vaultNumber < 3);
        require(decimals >= 8);
        require(decimals <= 18);
        uint256 normalizedSupply;
        if (decimals <= 18)
            normalizedSupply = supply * (10 ** (18 - decimals));
        else 
            normalizedSupply = supply / (10 ** (decimals - 18));

        require(normalizedSupply > 100 ** 18); // 最小供应量
        vaultBalance[vaultNumber] = sqrt(normalizedSupply);
        vaultNumber++;
    }

    function previewWithdraw(uint256 assets) external returns (uint256 shares) {
        if (vaultNumber < 3)
            return 0;

        uint256 totalSupply = assets - (vaultBalance[0] + vaultBalance[1] + vaultBalance[2]);
        assert(totalSupply > 0);
    }
}

请注意，添加金库的过程涉及使用循环计算平方根，这是一项符号执行工具难以处理的操作，因为它需要将循环展开最大次数（我们不知道该次数，因为它取决于输入）或使用合适的循环不变量（Runtime Verification 的人有一系列关于循环不变量的精彩博客文章）。

对于实际的不变量，我们添加了一个简单的断言，指出取款后的总供应量不能为空。当然，这不是一个非常有趣的不变量，但足以说明这种模式是如何工作的。要运行此程序，我们执行：

echidna multiVault.sol --test-limit 1000000000000 --sym-exec true 

对于模糊测试器来说，打破此断言很困难，因为它需要创建三个金库，然后选择要提取的确切金额。通常，如果你必须处理代码中的这种模式，则需要引入一个“幽灵变量”来累计标准化余额，并确保模糊测试器可以访问它（例如，它应该是公共的）。这些约束很容易由符号工作器解决，该工作器在几秒钟内找到一个反例来触发断言失败并最小化序列：

 调用序列：
    addVault(187437275246714327976927632528824801846,17)
    addVault(212381979343444824622226965412329656662,13)
    addVault(340282366920938463463374607431768211452,9)
    previewWithdraw(340303606993245560412980109897585769705914218460)

值得一提的是，在本示例中，我们知道将在三个交易后到达代码的某个部分，因此我们可以创建一个测试来模拟这三个交易，也许使某些输入成为符号。但是，不这样做会更快，因为我们并不真正在意用于达到该状态的交易，这就是随机测试的力量！

以下是此模糊测试活动期间发生的情况的摘要：

1. 在开始之前，静态分析工具检测到重要的常量并识别出具有断言的函数。
2. 模糊测试引擎最初探索了合约状态，并找到了一些有趣的状态（使用覆盖率）。
3. 符号引擎要求提供其中一个状态，选择一个带有断言的函数（例如，previewWithdraw），并从那里开始运行完全符号的交易。
4. 符号执行创建了一个模型，解决了约束条件，并为触发断言失败的交易生成了一个输入。
5. 模糊测试引擎验证了符号引擎生成的交易，并确认了断言失败。
6. 模糊测试引擎减少了触发断言失败所需的交易数量。

我们刚刚看到了一个工具，它结合了所有主要的程序分析技术来自动发现和简化破坏不变量的输入，这非常酷！

如何使用它？

目前，符号执行模式仅在断言模式下运行，并且仅限于检测断言失败。如果你正在测试这些功能，请牢记这一点。

你需要安装 SMT 求解器。强烈建议使用 bitwuzla，特别是与其他替代方案（如 Z3）相比。安装完成后，你可以使用 --sym-exec true 打开符号执行。为了知道使用哪种模式，Echidna 使用其他参数：

• 在验证模式下，我们关闭模糊测试工作器并使用单个交易，因此这需要 --workers 0 --seq-len 1。
• 在探索模式下，我们可以使用正数个工作器和任意数量的交易。

如你所见，此界面不是很直观，最终应替换为更好的界面，例如专用模式（例如，--test-mode verification 或类似的东西）。

Echidna 启动后，我们可以检查符号工作器日志，以查看是否需要调整某些参数。通常可以使用 --format text 来了解符号工作器正在做什么（但相同的信息在 TUI 中可用）。特别是，有一些重要的警告需要注意：

• Partial explored path(s) during symbolic verification of method …: Branches too deep at program counter: …，然后你必须增加 symExecMaxExplore。这可能是最重要的符号执行参数，它确定了要探索的最大分支数。请记住，当你使用诸如 20 之类的值时，这意味着它可以达到最多 2**20 个状态，因此请小心使用它！
• Max Iterations Reached in contract: …，然后你必须增加 symExecMaxIters。此参数向符号引擎发出信号，表示允许探索访问给定指令的次数。通常，这适用于循环，但是，当多次调用同一函数或当 solc 优化器通过查找重复的代码片段来减小合约的大小时，它也可能很有用。
• Error(s) during symbolic exploration: "Result unknown by SMT solver"，然后你需要增加 symExecTimeout 参数。默认情况下为 30 秒，你可以尝试使用 120 甚至 300 之类的数字。

何时使用它？

那么，智能合约开发人员或安全研究人员何时应该使用符号执行？根据我们测试此新功能的有限经验，它不应该是默认选择。在大多数情况下，模糊测试器在探索状态和发现反例方面已经非常有效。相反，符号执行应该应用于我们想要提供更强大的安全保证的上下文中。特别是：

• 在处理没有状态的数学密集型函数时（验证模式）。
• 在广泛的模糊测试活动后添加额外的保证层时。

仍然有一个值得讨论的有趣挑战，一个与模糊测试活动中经常使用的常见模式相关的挑战。考虑以下示例：

contract TestTarget {
   function callOperation(uint256 p1, uint256 p2, address p3) { 
     Target.operation(p1, p2, p3);
     … 
   }

   function checkAsserts() { 
        assert(..);
   }
}

对于当前的实现，符号执行对于这种模式不是很有效。一方面，callOperation 通常不包含断言，因此符号引擎会跳过它。另一方面，checkAsserts 没有符号输入（除了块时间戳/编号和 msg.sender），因此也会跳过它，因为其大多数数据是具体的。

一个常见的解决方法是将这两个函数组合成一个调用（例如，callOperationAndCheckAsserts）。虽然这适用于实验，但这不是一个理想的长期解决方案。当尝试有效地探索单个交易之外的内容时，传统的符号执行工具始终面临这一挑战。

幸运的是，静态分析引擎 Slither 可以提供帮助。它可以揭示函数之间的数据依赖关系，例如：

"functions_relations": {
        "TestTarget": {
            "callOperation(uint256,uint256,address)": {
                "impacts": [
                    "checkAsserts()",
                    …
                ],
             }
        }
}

此信息使我们能够识别用于符号执行的有意义的交易链，仅将探索重点放在最相关的组合上。

即将推出的功能和要解决的问题

用户的力量！

即使未找到反例或某些状态仍未探索，也必须清楚地向用户显示符号执行的结果。一个有趣的建议是将模糊测试活动覆盖率报告扩展到具体执行之外，添加一个 "符号覆盖率" 层来高亮显示符号引擎到达的行。例如，在这种情况下，我们可以用 s 标记以符号方式到达的行：

*rs |     function liquidate(address user, uint256 amount) public {
*rs |         require(amount > 0, "Invalid amount");
    |
* s |         uint256 debt_user = debt[user];
* s |         uint256 collateralETH_user = collateralETH[user];
*rs |         require(debt_user > 0, "No debt");
    |
* s |         uint collateralUSD = (collateralETH_user * ethPrice) / ETH_UNIT;
* s |         uint ratio = (collateralUSD * 100) / debt_user;
    |
*rs |         require(ratio < MIN_COLLATERAL_RATIO, "Healthy position");
    |
*   |         if (ratio >= EMERGENCY_MODE_RATIO) {
    |             require(amount <= debt_user, "Amount exceeds debt");
    |         } else {
*r  |             revert("emergency mode active");
    |         }
    |         … 

这种报告将帮助开发人员和审计人员更好地了解符号执行的优势和局限性。它还可以鼓励他们简化代码，使其更易于使用工具。

请注意，这不是一个全新的想法：Halmos 最近引入了对类似功能的支持。

自动边界提取

许多智能合约开发人员在函数的开头使用 require 语句来定义前提条件，特别是对于给定的参数。例如：

 function f(uint256 x, uint256 y) external {
      require(x <= balance[msg.sender]);
      require(y + 1 >= 0x99);
      …
  }

如果我们能够提取 x 和 y 的有效范围，以便 Echidna 知道哪些输入是“有效的”，并且可以更有效地探索合约状态，该怎么办？这实际上可以通过一点符号执行来实现：自动边界提取的基本原型在此处可用。你已经可以检查它产生的边界。例如，对于上面的函数，一组可能的提取约束是：

已解决的约束：
arg1 <= 0x100000000
arg2 >= 0x98

在这种情况下，一个约束取决于合约的状态。在本示例中，Echidna 产生一个约束，其中 balance[msg.sender] 为 0x100000000。

最初的原型构建起来出奇地容易。但是，将其集成到模糊测试引擎的工作流程中具有挑战性：我们需要同步具体和符号工作器，以便在探索特定状态时传播边界。我们需要完全重构活动代码，然后才能做到这一点。

这段代码是在 @GalloDaSballo 发起的讨论之后开发的，他询问是否可以使用符号执行来提取简单的输入约束，以防止恢复，从而加快模糊测试活动的速度（类似于 pyrometer 计算的内容）。答案是肯定的，此想法最终将集成到模糊测试引擎中，以实现更快的探索。

基准测试，基准测试，基准测试

使用一组真实的智能合约的基准测试正在进行中，该基准测试旨在测试符号和具体探索。它将作为不同符号执行框架和工具的试验台，使我们能够评估它们处理复杂代码的效果。敬请关注！

哦，还有一件事

如果你注意到此博客文章中的任何不正确、不精确或可能具有误导性的内容，请随时与我联系以进行澄清。如果你测试了此新的 Echidna 功能并遇到任何问题，请打开一个问题。

• 原文链接： github.com/gustavo-griec...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～