小技巧：使用 Halmos 实现有状态不变性测试

编者按：我们经常收到的关于 Halmos，a16z crypto 的开源形式化验证工具的常见问题是：“你能用它进行有状态不变性测试吗？”它不支持开箱即用；但在这篇文章中，独立安全研究员 Antonio Viggiano 分享了一种新的有状态不变性测试方法，这是在与我们的工程团队合作进行 Halmos 的性能研究时发现的。请参阅他的博客 Fuzzy，了解更多关于模糊测试、不变性测试、符号测试和形式化验证的信息。

形式化验证 和不变性测试是评估程序是否按预期运行的两种不同方法。与形式化验证不同，不变性测试评估程序对某些输入的行为，而形式化验证可以检查它对所有可能输入的行为。形式化验证似乎是更有效、更全面的解决方案。但实际上，这些过程是互补的：它们具有不同的优势，并且一起使用时可以提供最大的保证。

Halmos 是 a16z crypto 开发的开源形式化验证工具，它允许开发者通过符号测试重用为不变性测试编写的相同属性作为形式规范，从而帮助开发者弥合不变性测试和形式化验证之间的差距。同样，我们可以使用 Halmos 进行不变性测试，以证明协议不变性可以保持到任意数量的交易。虽然不变性测试不是其预期用例，但寻找创新方法来扩展其质量保证工具集的开发者也可以使用 Halmos 进行无状态测试，现在，只需进行一些小的调整即可进行有状态测试。

在这篇文章中，我们将深入研究使用 Halmos（一种用于 EVM 智能合约的符号测试工具）实现有状态不变性测试。首先，我们将简要概述符号测试和有状态不变性测试；然后讨论 Halmos 与传统模糊测试工具相比如何。最后，我们将研究 Multi-Collateral DAI 系统的简化版本的实际案例研究，以及 Halmos 如何用于增强智能合约的可靠性和安全性。

Halmos 符号测试简要概述

符号测试涉及使用符号值执行测试，从而显著减少了对大量规范的需求。与传统的测试（确认程序对特定输入的运行功能）不同，符号测试会根据所有可想象的输入来评估程序。这种严格性和全面性在区块链环境中特别有用，因为程序正确性至关重要。

Halmos 是 a16z crypto 开发的用于 EVM 智能合约的符号测试工具。它通过使用现有测试作为形式规范的基础来简化该过程，而不是需要新的规范或语言。

来源：使用 Halmos 进行符号测试：利用现有测试进行形式化验证

符号测试领域与模糊测试密切相关，不同之处在于，Halmos 不是尝试随机输入以破坏系统属性或不变量，而是针对整个有效输入范围检查不变量。因此，Halmos 可以提供比模糊器更高的保证。虽然 Foundry、Echidna 或 Medusa 可以相对较快地验证是否存在错误，但通常无法断言其不存在。

当通过 Halmos 运行测试时，它要么确认测试对所有输入都有效，要么提供测试失败的示例。这种方法利用现有的单元测试或模糊测试进行形式化验证，因此开发者可以专注于改进和扩展测试套件，而不是创建新的规范。

那么有状态不变性测试呢？

我之前的研究 表明，复杂的协议可能需要许多不同的函数调用，并且输入必须在特定范围内才能破坏不变量——有时多达 10 个不同的交易。这表明有状态不变性测试可以在项目中应采用的质量保证策略中发挥关键作用，同时采用无状态不变性测试。

有状态测试包括在多个函数执行的测试用例中维护系统的内部状态。这种方法可以更接近真实世界的场景，因为它考虑了先前的交易对新交易的影响，并探索了破坏系统不变量的不同路径的依赖性。

大多数模糊器都支持开箱即用的有状态模糊测试，这涉及使用来自预定合约的指定函数调用的随机序列来评估一系列不变式表达式。这些不变量在每次函数调用执行后都会被检查，并且是揭示复杂协议状态和非典型场景中的逻辑错误的有效方法。

Halmos 本身支持无状态不变性测试，该测试通过在每个测试用例之间重置系统状态来运行，但默认情况下不支持有状态测试。该工具旨在插入现有的 Foundry 基于属性的测试中，这些测试通常不会在多次执行之间保留状态。

虽然这不是其预期用例，但有一种方法可以让有状态测试与 Halmos 协同工作。

来源：协议上有状态模糊测试的 Echidna 输出

使用 Halmos 实现有状态不变性测试

为了规避 Halmos 当前的限制（或者更确切地说，是设计决策），我们选择利用符号测试的优势并以符号方式执行函数调用。

这意味着，我们不是实现一个目标合约来进行模糊测试（这通常是我们使用 Echidna 会做的事情），而是实现一个目标函数，该函数接收一个函数选择器数组，该数组可以执行任何任意的函数调用。然后，我们只需遍历此数组，过滤掉我们感兴趣的选择器，创建符号输入 Halmos cheat codes，并将它们绑定到有效范围 以优化 SMT 求解阶段。

    function check_minivat_n_full_symbolic(bytes4[] memory selectors) public {
        for (uint256 i = 0; i < selectors.length; ++i) {
            assumeValidSelector(selectors[i]);  // 假设选择器有效
            assumeSuccessfulCall(address(minivat), calldataFor(selectors[i]));  // 假设调用成功
        }

        assertEq(
            minivat.debt(),
            minivat.Art() * minivat.rate(),
            "The Fundamental Equation of DAI"  // DAI 的基本等式
        );
    }

    function calldataFor(bytes4 selector) internal view returns (bytes memory) {
        if (selector == minivat.init.selector) {
            return abi.encodeWithSelector(selector);
        } else if (selector == minivat.move.selector) {
            return
                abi.encodeWithSelector(
                    selector,
                    svm.createAddress("dst"),
                    svm.createInt256("wad")
                );
        } else if (selector == minivat.frob.selector) {
            return abi.encodeWithSelector(selector, svm.createInt256("dart"));
        } else if (selector == minivat.fold.selector) {
            return abi.encodeWithSelector(selector, svm.createInt256("delta"));
        } else {
            revert();
        }
    }

来源：aviggiano/property-based-testing-benchmark

由于这种设置，Halmos 现在将使用一系列 N 个符号函数选择器执行此测试，并从我们的目标合约执行这些函数，序列的大小等于循环展开限制的数量：

$ halmos --function check_minivat_n_full_symbolic --contract HalmosT

[⠢] Compiling...   // 正在编译...
[⠊] Compiling 1 files with 0.8.21   // 使用 0.8.21 编译 1 个文件
[⠒] Solc 0.8.21 finished in 743.63ms  // Solc 0.8.21 在 743.63 毫秒内完成
Compiler run successful!   // 编译器运行成功!

Running 1 tests for test/HalmosTester.sol:HalmosTester Counterexample:  // 正在运行 test/HalmosTester.sol:HalmosTester 的 1 个测试 反例：
halmos_dart_int256_01 = 0x00000000000000000000000000000000000000
  p_selectors[0]_bytes4 = 0x380dc3ca000000000000000000000000000000
  p_selectors[1]_bytes4 = 0xe1c7392a000000000000000000000000000000
Symbolic test result: 0 passed; 1 failed; time: 12.62s  // 符号测试结果：0 个通过；1 个失败；时间：12.62 秒

为了评估 EVM 字节码的符号执行工具，我们针对 MiniVat 智能合约实现了由 Palina Tolmach 创建的 Multi-Collateral DAI 系统的简化版本。在此示例中，Halmos 能够在 12 秒内找到 已损坏不变量 的具体值的反例，尽管对于更高的循环展开限制，超时时间可能会迅速增加。

此实验可以理解为运行序列长度为 N 的 Echidna，它会产生类似的输出：

$ echidna . --contract CryticTester --config config.yaml --seq-len 2

[2023-11-15 13:48:36.74] Compiling .... Done! (5.483472s) Analyzing contract: property-based-testing-benchmark/projects/dai-ce   // [2023-11-15 13:48:36.74] 正在编译.... 完成! (5.483472s) 正在分析合约：property-based-testing-benchmark/projects/dai-ce
[2023-11-15 13:48:42.96] Running slither on .... Done!  // [2023-11-15 13:48:42.96] 正在 ... 上运行 Slither. 完成!
(9.04136s) invariant: failed!  // (9.04136s) 不变量：失败！
 Call sequence:  // 调用顺序：
 frob(1)
 init()
Event sequence:  // 事件顺序：
Panic(1): Using assert  // Panic(1)：使用断言
Log(«The Fundamental Equation of DAI») from: 0xa329c0648769a73afac7f  // 来自的日志（«DAI 的基本等式»）：0xa329c0648769a73afac7f
Unique instructions: 1251  // 唯一指令：1251
Unique codehashes: 2  // 唯一代码哈希：2
Corpus size: 4  // 语料库大小：4
Seed: 7112067775457772404  // 种子：7112067775457772404

运行具有函数选择器数组的 Halmos 可用于检查依赖于多个函数调用序列的不变量。此方法还展示了 Halmos 作为符号执行工具的灵活性。 通过应用此策略，我们希望进一步的研究将有助于确定 Halmos 在评估复杂项目的协议级别不变量中的适用性。更广泛、更灵活的质量保证选项，包括不变性测试、模糊测试和形式化验证，可以帮助确保关键协议按预期运行。

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