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

形式验证——使用数学方法跨任意数量的输入“检查”程序或智能合约的过程——通常被视为比传统测试更简洁、更全面的替代方法，可以编写更高质量、更安全的代码。 但实际上，形式验证是一个开放式的交互过程。 与单元测试非常相似，开发人员必须动态定义和分层正式规范，随着代码和分析的发展迭代他们的方法。 此外，形式验证仅与其规范一样有效，编写规范可能非常耗时（并且通常伴随着陡峭的学习曲线）。 

对于发现过程令人生畏的许多开发人员来说，单元测试通常是检验程序正确性的更具成本效益和时间效率的途径。 在实践中，形式验证并不是单元测试的更全面的替代方案，而是一种补充。 这些过程具有不同的优势和局限性，一起使用时可提供更大的保证。 开发人员总是需要编写单元测试——那么如果我们可以使用相同的属性进行形式验证呢？

哈尔莫斯，我们的开源形式验证工具，允许开发人员 重用 通过符号测试为正式规范的单元测试编写相同的属性。 开发人员不必从一开始就创建一组健壮的属性，而是可以避免重复工作并一次改进他们的测试几个规范，而无需从头开始。 我们设计这个工具是为了与形式验证过程中的其他工具一起使用，作为形式验证的入口； 开发人员可以轻松地从一些分析开始，然后再在此过程中添加更多分析。

在这篇文章中，我们介绍了形式验证的挑战，以及通过符号测试弥合单元测试和形式验证之间差距的潜力。 然后，我们使用现有的智能合约代码浏览 Halmos 的演示，并快速浏览开发人员可用的其他形式验证工具（许多开源工具）。

形式验证与测试

正式验证 - 因其严谨性和全面性而受到区块链开发人员的普遍青睐 - 是通过验证程序是否满足某些正确性属性来证明程序正确性的过程。 特定于程序的属性通常由外部提供，并使用所使用的验证工具支持的形式语言或符号表示。 开发人员通常将形式验证视为一种按钮解决方案，用于自动测试所有可能场景中的属性，但实际上，形式验证可能是一个劳动密集型和高度交互的过程。

与形式验证一样，单元测试涉及评估程序是否按预期工作； 然而，测试只检查程序的行为 一些 输入，而形式验证可以检查它 所有 可能的输入。 测试和形式验证都需要描述程序的预期行为（测试用例使用测试用例，形式验证使用形式规范）。 但是，当一起使用时，它们可以对程序进行更彻底的检查。 例如，测试可以有效地发现简单的错误和错误，但通常执行起来更快、更容易。 形式验证虽然使用起来比较麻烦，但功能强大，足以证明不存在错误或揭示在测试或代码审查中容易遗漏的细微错误。

规范开销

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

尽管测试和形式验证一起使用可以提高代码质量，但两者都需要（有时是相似的）以不同语言和格式描述程序的预期行为。 编写和维护这些描述是劳动密集型的，维护相同描述的两种不同形式感觉像是重复的工作。 这就提出了以下问题：是否有可能以开发人员可用于测试和验证的方式来描述预期行为？

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

符号测试是使用符号输入运行测试的实践，是一种有效的形式验证方法，可减少规范开销。 这种方法允许使用相同的测试用例进行测试和形式验证。 与验证程序对一组有限的输入是否正确工作的传统测试不同，符号测试检查程序的所有可能输入，因此通过符号测试的程序可以被认为是正式验证的。

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

因此，开发人员可以更灵活地从一系列质量保证选项中进行选择，包括单元测试、模糊测试和形式验证，具体取决于他们当前的需求。 例如，测试可以快速识别简单的错误，可能借助于生成随机输入的模糊器，然后 Halmos 可以进一步提高程序在所有输入中的正确性的信心。

示例：测试 isPowerOfTwo() 功能

例如，请考虑以下内容 isPowerOfTwo() 函数，它确定给定数字是否为 XNUMX 的幂。 这个函数使用一个 位操作算法 为了提高效率，但证明其正确性可能具有挑战性，特别是在输入不是 XNUMX 的幂的情况下。

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

您可以使用此测试来检查 isPowerOfTwo() 通过单元测试或模糊测试功能，使用选择的输入运行它。 像这样的测试不能正式证明函数的正确性，因为对每个可能的输入运行测试在计算上是不可行的。

然而，Halmos 允许开发人员重用这些预先存在的测试进行形式验证，只需付出一点额外的努力。 该工具通过执行测试的符号执行然后验证断言从未被违反（或者，如果断言 is 违反，通过提供反例）。 这意味着如果测试通过了 Halmos，函数的正确性就得到了正式验证，这意味着算法被正确实现并且已经被编译器准确地翻译成字节码。

限制：有界符号执行

通常不可能执行全自动、完整的符号测试，因为这需要解决 停顿问题，这是众所周知的 不可判定. 原因之一是通常无法自动确定循环应以符号方式迭代多少次。 因此，全自动形式验证通常是不可判定的。

鉴于这些基本限制，Halmos 将自动化置于完整性之上。 为此，Halmos 旨在为无界循环（其中迭代次数取决于程序输入）或可变长度数组（包括字符串）执行有界符号推理。 这牺牲了一些完整性，但允许 Halmos 避免要求用户提供额外的注释，例如循环不变量。

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

Halmos 仅象征性地将此无限循环迭代到指定的界限。 例如，如果边界设置为 3，Halmos 将最多迭代循环 3 次，并且不会考虑会导致循环迭代超过 3 次的输入值（即任何大于或等于 2^3 的值） ). 在这种特殊情况下，将界限设置为 256 或更高将使 Halmos 完整。

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

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

符号测试属性

由于 ERC721A 的现有测试是用带有 Hardhat 的 JavaScript 编写的（Halmos 当前不支持），我们在 Solidity 中为主要入口点函数编写了新测试： mint(), burn()及 transfer(). 这些测试检查了每个函数是否正确更新代币所有权和余额，并且只影响相关用户而不会改变其他用户的余额或所有权。 由于在 ERC721A 中使用了惰性数据结构算法，后者的证明并非易事。 例如，以下测试检查 transfer() 函数正确更新指定令牌的所有权：

另一个测试检查 transfer() 函数不会改变其他地址的余额，如前所述，这很难证明：

验证结果

我们使用 Halmos 在 ERC721A 智能合约上进行了验证实验，总共编写了 19测试. 测试通过 Halmos 运行，循环展开边界为 3，需要 16 分钟才能完成。 验证时间的细分可以在下表中看到。 实验在配备 M1 Pro 芯片和 16 GB 内存的 MacBook Pro 上进行。

测试	时间（秒）
测试BurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
测试BurnOtherBalancePreservation	5.69
测试BurnOtherOwnershipPreservation	189.70
测试BurnOwnershipUpdate	3.81
测试烧录要求	71.95
测试MintBalanceUpdate	0.20
测试 MintNextTokenIdUpdate	0.18
测试MintOtherBalancePreservation	0.26
测试MintOtherOwnershipPreservation	5.74
测试 MintOwnershipUpdate	1.38
测试薄荷要求	0.09
testTransferBalance不变	9.03
测试转账余额更新	53.53
testTransferNextTokenIdUnchanged	4.47
测试转移其他余额保存	19.57
测试转移其他所有权保留	430.61
测试转移所有权更新	18.71
测试转学要求	149.18

虽然大多数测试在几秒钟内完成，但其中一些测试需要几分钟。 这些耗时的测试由于要考虑的情况的复杂性而难以验证，并且与惰性数据结构算法的正确性密切相关。

总体而言，本次实验的结果表明 Halmos 能够有效验证智能合约代码的正确性。 尽管智能合约具有复杂性和潜在的边缘情况，但它提高了对代码完整性的信心。

试验注入的错误

为了证明 Halmos 有限推理的有效性，我们使用它来检测 ERC721A 合约先前版本中的错误。 这个版本有一个错误处理算术溢出的问题，并可能允许批量铸造大量令牌，这可能会破坏惰性数据结构的完整性并导致一些用户失去他们的令牌所有权（一个问题 解决 在当前版本中）。 我们在有缺陷的版本上对 ERC19A 运行了同一套 721 项测试，Halmos 能够找到 mint() 功能。 具体来说，Halmos 提供了导致上述利用场景的输入值。 该实验的结果表明，尽管 Halmos 的边界推理不完整，但它可以成为检测和防止智能合约中可利用错误的有效方法。

相关工作

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

虽然 Halmos 是对可用于智能合约验证的工具集的重要补充，但它旨在补充（而不是替代）现有工具。 开发人员可以将 Halmos 与其他工具结合使用，以在其合同中实现更高级别的保证。 下面，我们将 Halmos 与一些选定的支持 EVM 字节码的形式化工具进行比较。

• K 是一个强大的形式验证框架，支持演绎验证和交互式定理证明。 其底层理论和实现提供了高水平的表现力，使其适用于验证复杂的程序和算法。 但是，应该注意的是，K 的设计并没有特别强调自动验证，并且缺少某些自动化功能，在验证过程中可能需要更多的手动工作。 要使用K框架，正式的规范是用K语言编写的，必须在使用前学习。 它的优势在验证复杂系统时特别有用，使用自动推理进行分析可能具有挑战性。
• 切尔托拉 是智能合约的形式化验证工具，专注于自动化验证，支持有界模型检查，类似于Halmos。 要使用 Certora，开发人员必须学习他们的新语言， CVL, 以便编写规范。 这种语言允许通过契约不变量对许多关键属性进行简洁描述，这是 Halmos 目前不支持的功能。 尽管是封闭源代码的专有工具，但 Certora 提供了强大的形式验证工具，并具有持续的开发和良好的用户支持。
  
  另一方面，Halmos 是一个开源工具，规模较小，目前缺少 Certora 提供的一些功能，但它旨在作为一种公共产品，旨在作为一种利基解决方案，用于快速验证智能合约而无需需要大量的设置和维护。
• HEVM 是另一个类似于 Halmos 的形式验证工具。 它以前是 DappTools 的一部分，DappTools 是 Foundry 的前身。 HEVM 和 Halmos 都具有不需要单独规范的特性，并且可以象征性地执行现有测试以识别断言违规。 这允许用户互换使用这两种工具或并行运行它们以进行相同的测试，从而为他们提供多种符号测试选项。
  
  值得注意的是，尽管 HEVM 和 Halmos 有相似之处，但它们是独立开发的，并且在实现细节上有所不同； 特别是在优化和符号推理策略方面。 此外，HEVM 是用 Haskell 编写的，而 Halmos 是用 Python 编写的，提供了丰富的 Python 生态系统。 能够使用这两种工具为用户提供了更多的灵活性和选择，以确保智能合约的安全性和正确性。

哈尔莫斯 是开源的，目前处于测试阶段。 我们正在积极致力于新的 功能 和功能，包括 Foundry 作弊代码和其他几个关键的可用性功能。 我们非常感谢您对哪些功能最重要的想法，并欢迎任何反馈、建议和贡献，以使 Halmos 成为适合所有人的更好工具。

**

此处表达的观点是引用的个人 AH Capital Management, LLC (“a16z”) 人员的观点，而不是 a16z 或其关联公司的观点。 此处包含的某些信息是从第三方来源获得的，包括来自 a16z 管理的基金的投资组合公司。 虽然取自被认为可靠的来源，但 a16z 并未独立验证此类信息，也不就该信息的当前或持久准确性或其在特定情况下的适用性做出任何陈述。 此外，该内容可能包含第三方广告； a16z 未审查此类广告，也不认可其中包含的任何广告内容。

此内容仅供参考，不应被视为法律、商业、投资或税务建议。 您应该就这些事项咨询您自己的顾问。 对任何证券或数字资产的引用仅用于说明目的，并不构成投资建议或提供投资咨询服务的要约。 此外，本内容并非针对也不打算供任何投资者或潜在投资者使用，并且在任何情况下都不得在决定投资于 a16z 管理的任何基金时作为依据。 （投资 a16z 基金的要约仅通过私募备忘录、认购协议和任何此类基金的其他相关文件提出，并应完整阅读。）任何提及、提及或提及的投资或投资组合公司所描述的并不代表对 a16z 管理的车辆的所有投资，并且不能保证这些投资将是有利可图的，或者将来进行的其他投资将具有类似的特征或结果。 由 Andreessen Horowitz 管理的基金进行的投资清单（不包括发行人未允许 a16z 公开披露的投资以及对公开交易的数字资产的未宣布投资）可在 https://a16z.com/investments 获得/。

其中提供的图表仅供参考，在做出任何投资决定时不应依赖。 过去的表现并不预示未来的结果。 内容仅在所示日期生效。 这些材料中表达的任何预测、估计、预测、目标、前景和/或意见如有更改，恕不另行通知，并且可能与他人表达的意见不同或相反。 有关其他重要信息，请参阅 https://a16z.com/disclosures。