形式化验证与测试

形式化验证——使用数学方法“检查”一个程序或智能合约在任意输入下的过程——通常被视为编写高质量、更安全代码的传统测试更简明、全面的替代方案。但实际上，形式化验证是一个开放式和互动的过程。就像单元测试一样，开发人员必须动态定义并层叠形式规范，随着代码和分析的演变不断迭代他们的方法。此外，形式化验证的有效性取决于其规范，而编写规范可能会耗费大量时间（并且通常伴有陡峭的学习曲线）。

对于许多觉得这一过程令人生畏的开发人员而言，单元测试通常是较为经济且省时的寻找程序正确性的途径。在实践中，形式化验证并不是单元测试的更为全面的替代品，而是互补的。这些过程各有优缺点，搭配使用时能够提供更大的保障。开发人员始终需要编写单元测试——那如果我们可以使用相同的属性进行形式化验证呢？

Halmos，我们的开源形式化验证工具，允许开发人员通过符号测试重用为单元测试编写的相同属性作为形式规范。开发人员无需从一开始就创建一整套稳健的属性，而是可以避免重复工作，以少量规范逐步改进他们的测试，而不必从头开始。我们设计这个工具的目的是为形式化验证过程中的其他工具提供入门，开发人员可以在初期进行几个分析，几乎无需努力，之后再在这个过程的后期加入更多分析。

在本文中，我们讨论形式化验证面临的挑战，以及通过符号测试弥合单元测试与形式化验证之间的差距的潜力。接着，我们将通过使用现有智能合约代码的 Halmos 演示，快速查看开发人员可用的其他形式化验证工具（许多是开源的）。

形式化验证 vs 测试

形式化验证——一般被区块链开发者偏爱的严谨和全面——是通过验证程序满足某些正确性属性来证明程序正确性的过程。这些特定于程序的属性通常是外部提供的，并使用被所用验证工具支持的形式语言或符号表达。开发人员通常将形式化验证视为自动测试属性的“一键式解决方案”，但是实际上，形式化验证可能是一个劳动密集和高度互动的过程。

像形式化验证一样，单元测试涉及评估一个程序是否按预期工作；然而，测试仅检查程序在 某些 输入下的行为，而形式化验证可以对 所有 可能的输入进行检查。测试和形式化验证都需要程序预期行为的描述（测试中使用测试用例，形式化验证中使用形式规范）。但当两者结合使用时，可以为程序提供更全面的检查。例如，测试有效地发现简单的错误和失误，但通常更快且更容易执行。形式化验证尽管使用起来更为繁琐，但足够强大，能够证明错误的缺失或揭示在测试或代码审查中容易被忽视的微妙错误。

规范开销

形式化验证的主要挑战之一是撰写和维护形式规范的开销。这个过程通常涉及使用专门的语言手动编写规范的耗时任务（许多开发人员需要先学习这种语言）。这个过程也是逐渐增量的，通常从编写简单属性和首先验证它们入手，然后逐渐添加更复杂的属性。像测试一样，这也是一个开放式的过程，没有明确的停止点，只有在可用的时间范围内添加尽可能多的属性。此外，当开发人员在验证时更改代码时，他们也必须更新现有的规范，从而造成额外的维护工作。这些因素可能使得形式化验证对于一些不愿意承担额外开销的开发人员而言是一项艰巨的任务。

虽然测试和形式化验证结合使用可以改善代码质量，但两者均需要（有时是类似的）以不同语言和格式描述程序的预期行为。撰写和维护这些描述是劳动密集型的，维护同一个描述的两种不同形式会使人感到重复努力。这就提出了下一个问题：是否有可能以一种方式描述预期行为，使开发人员可以将其同时用于测试和验证？

通过符号测试和 Halmos 弥合测试与形式化验证之间的差距

符号测试是使用符号输入运行测试的实践，作为一种有效的形式化验证方法，它减少了规范开销。这种方法允许对测试和形式化验证使用相同的测试用例。与传统测试不同，后者仅验证程序在有限输入集合上的正确性，符号测试则对程序进行检查，应用于所有可能的输入，因此通过符号测试的程序可以视为正式验证过的。

Halmos 是一个为符号测试设计的形式化验证工具。它不需要单独的规范或学习新语言，Halmos 使用现有的测试作为形式规范。通过 Halmos 运行测试将自动验证它们在所有可能的输入下通过，或者提供反例。这不仅消除了额外规范编写的需要，还允许将为单元测试或模糊测试编写的测试重用于形式化验证的目的。

因此，开发人员可以根据当前的需求，从多种质量保证选项中选择，包括单元测试、模糊测试和形式化验证。例如，测试可能迅速发现简单错误，可能辅以生成随机输入的模糊测试工具，然后 Halmos 可以进一步增强对程序在所有输入下的正确性信心。

示例：测试 isPowerOfTwo() 函数

作为一个示例，考虑以下的 isPowerOfTwo() 函数，它决定给定的数字是否是二的幂。这个函数使用 位操作算法 来提高效率，但证明其正确性可能会非常具有挑战性，尤其是在输入不是二的幂的情况下。

设想以下对 isPowerOfTwo() 函数的测试：它比较函数的实际输出与给定输入的预期输出。这是一个参数化测试（也称为基于属性的测试），这意味着你可以轻松地用不同的输入值运行它，可能借助像 Foundry 这样的模糊工具。

你可以使用这个测试通过单元测试或模糊测试来检查 isPowerOfTwo() 函数，运行一系列输入。然而，这样的测试无法正式证明函数的正确性，因为在每一个可能输入的情况下运行测试在计算上是不可行的。

然而，Halmos 允许开发人员重用这些已有的测试进行形式化验证，只需少量的额外努力。该工具通过对测试进行符号执行，检查测试在所有可能输入下是否通过，然后验证断言是否从未被违反（或者如果断言 被 违反，通过提供反例）。这意味着如果测试在 Halmos 中通过，则函数的正确性被正式验证，表明算法已正确实现，并且已被编译器准确转译为字节码。

限制：有界符号执行

通常无法执行完全自动的完整符号测试，因为这需要解决 停机问题，而该问题已知是 不可判定。原因之一是通常无法自动确定循环应该在符号上迭代多少次。因此，完全自动形式化验证通常是不可判定的。

考虑到这些基本限制，Halmos 优先考虑自动化而非完整性。为此，Halmos 被设计为对无界循环（其迭代次数取决于程序输入）或可变长度数组（包括字符串）执行有界符号推理。这虽然牺牲了一些完整性，但可以避免要求用户提供额外的注释，如循环不变量。

例如，考虑以下迭代版本的 isPowerOfTwo() 函数，它具有一个无界的 while 循环，循环的迭代次数由表示输入数字所需的最小位数决定。

Halmos 仅在指定的边界内符号迭代这个无界循环。例如，如果边界设置为 3，Halmos 将最多迭代这个循环 3 次，并不会考虑导致循环迭代超过 3 次（即，任何大于或等于 2^3 的值）的输入。在这种情况下，将边界设置为 256 或更高将使 Halmos 实现完整性。

演示：使用 Halmos 对 ERC721A 进行形式化验证

为了展示 Halmos 的能力，我们使用它对 ERC721A 进行符号测试和形式化验证，这是一种高度优化的 ERC721 标准实现，几乎与单个铸造的成本相同，允许批量铸造。ERC721A 包含几个创新的 优化 来实现这种效率；例如，铸造时将Token所有权数据的更新延迟到Token转移时，可以节省煤气。这需要使用复杂的数据结构和算法，从惰性数据结构中有效获取所有权信息。尽管这种优化提高了 gas 效率，但它也增加了代码复杂性，使得证明实现的正确性变得具有挑战性。这使得 ERC721A 成为形式化验证的良好候选者，因为它可以增加对实现的信心，并使潜在用户受益。

符号测试属性

由于 ERC721A 的现有测试是用 JavaScript 和 Hardhat 编写的（目前 Halmos 不支持），我们用 Solidity 为 mint()、burn() 和 transfer() 等主要入口函数编写了新测试。这些测试检查每个函数是否正确更新Token所有权和余额，并且仅影响相关用户而不更改其他用户的余额或所有权。由于在 ERC721A 中使用惰性数据结构算法，后者的证明并不简单。例如，以下测试检查 transfer() 函数是否正确更新指定Token的所有权：

另一个测试检查 transfer() 函数是否不更改其他地址的余额，正如之前提到的，这一点也很难证明：

验证结果

我们使用 Halmos 对 ERC721A 智能合约进行了验证实验，共编写了 19 个测试。这些测试通过 Halmos 执行，循环展开限制为 3，耗时 16 分钟完成。验证时间的细分见下表。该实验在一台配备 M1 Pro 芯片和 16GB 内存的 MacBook Pro 上进行。

虽然大部分测试在几秒钟内完成，但其中一些耗时几分钟。由于需要考虑的情况复杂，这些耗时长的测试验证起来较为困难，与惰性数据结构算法的正确性息息相关。

总体而言，该实验的结果表明 Halmos 能有效地验证智能合约代码的正确性。尽管智能合约的复杂性和潜在边际情况，但它提供了对代码完整性的更加信心。

带有注入缺陷的实验

为了展示 Halmos 的有界推理的有效性，我们使用它来在 ERC721A 合约的早期版本中检测缺陷。这个版本有一个处理算术溢出的错误，可能允许批量铸造大量Token，这可能破坏惰性数据结构的完整性，导致某些用户失去他们的Token所有权（这一问题在当前版本中已 解决）。我们在有缺陷版本的 ERC721A 上运行了相同的一组 19 个测试，Halmos 能够找到 mint() 函数属性的反例。具体来说，Halmos 提供的输入值导致了上述的漏洞场景。该实验结果表明，尽管 Halmos 不完整，但其有界推理可能是检测和预防智能合约中可被利用缺陷的有效方法。

相关工作

各种团队已经开发了用于以太坊智能合约字节码的形式化验证工具。包括 Halmos 在内的这些工具可以帮助确保智能合约的安全性和正确性。比较和理解不同工具的特性、能力和局限，可以帮助开发人员选择最适合其独特需求的工具。

虽然 Halmos 是智能合约验证工具集中一个有价值的补充，但它的目的在于补充（而非替代）现有工具。开发人员可以将 Halmos 与其他工具结合使用，以实现对其合约的更高信心。以下是 Halmos 与一些支持 EVM 字节码的选定形式工具的比较。

• K 是一个强大的形式化验证框架，支持演绎验证和交互式定理证明。其底层理论和实现提供了较高的表达能力，适合用于验证复杂程序和算法。然而，需要注意的是，K 不强调自动化验证，并且缺乏某些可能在验证过程中需要更多手动工作的自动化特性。要使用 K 框架，必须提前学习 K 语言来编写形式规范。它的强大在于特别适用于验证复杂系统，这些系统可能难以通过自动推理进行分析。
• Certora 是一个专注于自动化验证的智能合约形式化验证工具，支持有界模型检查，类似于 Halmos。要使用 Certora，开发人员需要学习其新的语言 CVL，以编写规范。这种语言允许通过合同不变性简洁地描述许多重要特性，而 Halmos 当前不支持该特性。尽管 Certora 是一个闭源的专有工具，但它提供了强大的形式化验证工具，伴随持续开发和良好的用户支持。

另一方面，Halmos 是一个开源工具，规模较小，目前缺少 Certora 提供的某些特性，但它旨在作为公共利益，旨在为快速验证智能合约提供一个小众解决方案，无需大范围的设置和维护。

• HEVM 是一个与 Halmos 类似的形式化验证工具。它曾是 DappTools 的一部分，这是 Foundry 的前身。HEVM 和 Halmos 都具有不需要单独规范的特性，可以符号执行现有测试以识别断言违规。这允许用户交替使用这两个工具，或者对相同的测试进行并行执行，从而为他们提供了多种符号测试的选择。

值得注意的是，尽管 HEVM 和 Halmos 有相似之处，但它们是独立开发的，在实现细节上有所不同；特别是在优化和符号推理策略方面。此外，HEVM 是用 Haskell 编写的，而 Halmos 是用 Python 编写的，提供了接触丰富的 Python 生态系统的机会。能够同时使用这两个工具使用户在确保智能合约的安全性和正确性方面拥有更多的灵活性和选择。

Halmos 是开源的，当前处于测试阶段。我们正在积极开发新的 特性 和功能，包括 Foundry 的作弊代码以及其他一些关键的可用性特性。我们非常希望了解你认为最重要的功能，并欢迎任何反馈、建议和贡献，以使 Halmos 成为一个更好的工具，惠及所有人。

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