以太坊即将推出的 Pectra 硬分叉通过 11 个 EIP 引入了若干提升用户体验和验证者操作的增强功能。其中有三个 EIP 引入了链上系统合约，这些合约使用汇编语言来优化 Gas 效率。虽然这种做法在提升效率方面有效，但由于汇编语言本身较为底层，且缺乏编译器强制的安全检查，使用汇编语言的做法也带来了安全隐患。
应对这些风险的一种方法是使用形式化验证来消除潜在的汇编级安全漏洞。为此，我们使用了 Halmos 这一形式化验证工具，确保 Pectra 系统合约的正确性，从而巩固了 Pectra 升级的安全性。
通过形式化验证生成的结果文档也可以作为依赖汇编代码的其他智能合约的具体示例。尽管形式化验证通常被认为是一个抽象且复杂的概念，但像这些实际示例能够展示其在更广泛应用场景中的实用性。
在这篇文章中，我们首先简要介绍 Pectra 系统合约及汇编实现的挑战。接着，我们将形式化验证过程分解为若干步骤，并展示如何使用 Halmos 完成这些任务。
Pectra 系统合约与汇编实现的挑战
如前所述，Pectra 硬分叉计划在今年早些时候发布，其中包括 11 个 EIP，其中三个 EIP 引入了执行链上逻辑的系统合约：
- EIP-2935 提议将最后的 8191 个区块哈希存储在一个系统合约中，以支持无状态执行。该合约使用环形缓冲区来高效存储区块哈希。
- EIP-7002 引入了一种机制，允许验证者通过其执行层的提取凭证直接发起退出和提取操作，且提取请求存储在专用的系统合约中。此处使用队列来管理提取请求。
- EIP-7251 提议增加验证者的最大有效余额，允许较大的验证者合并操作。此类合并请求由一个单独的系统合约管理，使用队列来进行处理。
与典型的使用 Solidity 编写的智能合约不同，这些系统合约完全采用汇编语言编写，以提高 Gas 效率。使用汇编语言编写智能合约并不罕见——Seaport 和 Solady 便是著名的例子——尤其是在 Solidity 编译器生成的代码不够优化的情况下。生成不优化代码的典型情形包括处理字节数组用于 calldata 准备、Keccak 哈希输入、以及读取或写入动态大小字节到 / 从内存的其他操作码。
尽管汇编语言在 Gas 效率方面具有优势，但其编程挑战较大，因为它容易引入缺陷和安全漏洞。在编写汇编代码时，编译器通常会自动处理的安全检查（如 calldata 验证、内存清理、隐式类型转换）需要开发者手动实现。
缺少检查可能导致无效输入或被滥用的脏内存，从而潜在地引发安全漏洞。然而，手动实现这些检查要求开发者具备高级知识，并且容易出错。这种额外的工作量，加上底层编程带来的复杂性，使得编写安全的汇编代码变得极为困难且劳动强度大。
形式化验证提供了一种系统化的解决方案，通过提供正确性和安全性的数学保证，帮助解决这些挑战。
形式化验证的蓝图
让我们简要介绍一个形式化验证的基本框架。虽然其他框架也存在，并且具体细节可能会根据目标系统和上下文有所不同，但这个框架提供了一个有用的思维模型，适用于 Pectra 系统合约。由于形式化验证的全面解释超出了本文的范围，因此这里不会详细展开。关于智能合约形式化验证的更多信息，读者可以参考这篇指南作为一个良好的起点。
端到端的全面形式化验证通常包括以下几个步骤，这些步骤可分为两个阶段：
阶段 1：模型验证
- 步骤 1：形式化规范。将规范（通常以自然语言形式呈现，例如 EIP）转化为形式化规范语言。
- 步骤 2：定义属性。确定规范必须满足的关键属性（例如，确保 EIP-2935 中的环形缓冲区始终保持有效的区块哈希）。
- 步骤 3：证明属性。验证步骤 1 中定义的形式化规范是否满足步骤 2 中识别的属性。
阶段 2：细化证明
- 步骤 4：模型实现。将实现代码转化为数学模型。
- 步骤 5：证明细化。证明实现的形式化模型（来自步骤 4）是否忠实于形式化规范（来自步骤 1）。
模型验证和细化证明解决了验证过程中的不同方面。模型验证确保规范是合理的，而细化证明确认低级实现与规范的一致性。通过这两者的结合，可以确保实现符合关键属性。
将关注点分为这两个阶段，有助于在验证过程中提供清晰性和模块化。它还提供了执行的灵活性，可以为每个阶段应用不同的工具和方法，或根据时间和资源约束并行化任务或优先处理任务。
在 Pectra 合约的背景下，模型验证相当于对其 EIP 规范文档进行推理，而细化证明确保实现代码与 EIP 文档一致。
选择工具
开发者可以从多种工具中选择，可能会选择不同的工具来进行模型验证和细化证明。
模型验证最适合使用多功能和表达力强的工具。常用的工具包括交互式定理证明器（例如 Lean、Coq、Isabelle、ACL2）、模型检查器（例如 TLA+、Alloy、Quint）和演绎验证器（例如 Dafny、Why3）。这些工具能够对属性进行严格的推理。对于较简单的规范，手动的纸上证明也可能有效，尽管这种方法增加了信任基础，并且需要细致的审查。附带说明：将模型验证与安全审计结合起来可能会非常有益，因为审计员可能会识别规范中附加的安全属性或潜在漏洞。
细化证明则更适合使用特定于其实现语言的自动化验证工具。这样的自动化工具（例如 halmos、hevm、Kontrol、Certora 用于以太坊智能合约）能够内部处理实现的建模，减少人工错误的风险以及与手动转化相关的信任基础。此外，由于实现代码经常因优化或重构而发生频繁变化，自动化验证对于持续验证特别有价值。这些工具简化了过程，确保实现始终与规范保持一致，而无需对每次代码更新进行全面的人工审查。
在了解了形式化验证框架后，我们可以讨论如何将其应用于 Pectra 系统合约。接下来，我们将详细介绍如何使用 Halmos 进行细化证明。请注意，我们基于 Halmos 的形式化验证专注于细化证明，模型验证不包括在内。模型验证可以通过前述方法和工具单独执行，相关内容留待未来的工作中讨论。
Pectra 系统合约的细化证明
Halmos 是一个专为 EVM 字节码设计的形式化验证工具，非常适合用于执行细化证明。它自动化了验证过程中的关键部分，特别是第 4 步（实现的建模），并直接验证第 5 步中规范与实现字节码之间的细化关系。
使用 Halmos 时，细化条件被表示为常规的 Solidity 测试，具体通过断言来确保实现行为与规范一致。这些断言仅关注验证实现是否符合规范，而不涉及验证规范本身的属性——后者是在模型验证阶段处理的任务。
我们将 Halmos 应用于 Pectra 系统合约时，首先手动将 EIP 规范转化为 Solidity 测试断言。然后，我们使用这些测试来验证汇编实现的编译字节码。该过程确保系统合约在所有可能的输入和合约状态下都能按规范行为运行。尽管 Halmos 提供了一个“有限的”形式化保证——受限于如循环迭代或字节数组大小等执行约束——但它仍是一种有效且实用的确保正确性的方法。
该过程的信任基础包括 EIP 规范到 Solidity 测试的手动转化——由我们的安全工程师独立审查——以及 Halmos 工具本身。重要的是，汇编编译器被排除在信任基础之外，因为验证直接面向编译后的字节码。
效率与持续验证
我们在几天内完成了初步的验证过程，随后在几周内对测试结构、断言和文档进行了改进，以提升其效果。Halmos 在初步验证和持续验证过程中均表现出色，后者涉及在代码更新后重新验证实现。每次重新验证只需几个小时，使得即便在迭代开发过程中也能实用地保持正确性。
持续验证的重要性在于，Halmos 测试在重构过程中发现了一个越界错误。重构的定义是应当保持原有代码行为。然而，测试未通过，标示出不一致之处。深入调查后发现了一个微妙的错误，这突显了持续验证作为在迭代更改中及早捕获错误的强大安全网，增强了代码的可靠性。
