保留块及其在不变量验证中的作用

这篇文章详细介绍了 Certora 形式化验证中“保留块”（preserved blocks）的作用和用法。它解释了如何利用保留块来指导 Certora Prover 避免在探索不切实际的符号状态时产生虚假告警，从而确保对智能合约不变量（invariants）的验证更加准确和有效。文章以 WETH 合约为案例，逐步演示了如何通过添加保留块来解决验证失败的问题。

形式化验证与 Certora

保留块及其在不变量验证中的作用

模块 2：不变量、存储Hook、幽灵和形式化验证通证

上次更新于 2026 年 2 月 13 日

不变量是一个属性，它在智能合约部署后及其整个执行过程中必须始终为真。乍一看，验证不变量似乎很简单：假设不变量在函数调用前为真，运行函数，然后确认它之后仍然为真。

在实践中，这个过程很少如此简单。Certora Prover 在一个符号世界中运行，它探索合约的所有可能状态，而不仅仅是那些在已部署系统中实际发生的状态。这种详尽的符号探索是其设计的基础；它允许 Prover 在开发者可能从未考虑过的情景中找到错误。

然而，Prover 探索的并非所有符号状态都是合约业务逻辑范围内的有效或可达状态。如果没有额外的指导，Prover 可能会从“不可能”的状态或条件开始推理，或者基于这些状态进行推理，而这些状态在真实的区块链执行中永远不会出现。当这种情况发生时，Prover 可能会标记一个违规，即使合约本身是正确的，仅仅是因为分析从一个无效的假设开始。

为了防止此类假性违规，CVL 提供了保留块（preserved block），这是一种允许我们指定关于实际合约行为的额外假设的机制。这些假设有助于 Prover 专注于有效和相关的执行路径，排除逻辑上或上下文上不可能的状态。

在本章中，我们将探讨保留块在形式化验证中的作用。我们将讨论它们为什么是必要的，如何在 CVL 中编写它们，以及它们如何帮助确保不变量只在现实条件下被检查。我们还将通过验证 WETH 合约中，合约的 ETH 余额始终等于或超过其总代币供应的实际例子来应用这个概念。

为了更清楚地理解它们的作用，我们首先回顾一下 Prover 如何检查一个函数是否保留了不变量，以及为什么这个过程有时会中断。

为什么不变量需要额外的假设

正如我们所知，在验证不变量时，Prover 遵循类似于数学归纳法的结构化推理过程：

  1. 初始状态检查（基本情况）： Prover 首先验证不变量在合约构造函数执行完毕后立即为真。这确立了不变量在起始点为真。
  2. 假设（前置状态）： 对于每个公共和外部函数，Prover 假设不变量在函数执行前为真。
  3. 符号执行和后置状态检查： 然后，它在所有可能的输入和控制流路径上符号化执行函数，并验证不变量在函数执行后仍然为真。

如果不变量满足所有这些检查，则认为它在所有合约执行中都被保留。但困难在于：Prover 并不局限于实际的执行路径。它还会探索极不可能甚至不可能的状态。

例如，在验证 ERC-20 不变量“所有账户余额之和必须始终等于总代币供应量”时，Prover 可能会探索一个合约最终调用自身函数的执行路径。在实践中，这种情况永远不会发生，因为 transfer 等 ERC-20 函数旨在仅由外部用户或其他合约调用。然而，由于 Prover 系统地探索所有可能的调用者，它也会考虑合约调用自身函数的轨迹。

这种自调用会产生荒谬的情景，其中余额和总代币供应量显得不一致，导致 Prover 报告违规，尽管真实的执行不可能触发它。这些是假性违规的典型例子：不变量看起来被破坏了，仅仅是因为 Prover 推理了现实中不可能发生的状态。

这就是保留块的作用。保留块允许我们在不变量验证期间引入额外的假设，引导 Prover 忽略不可能或不相关的状态，并只关注现实的状态。

现在我们了解了保留块为什么是必要的，接下来我们看看如何在 CVL 中编写它们。

如何定义一个保留块？

保留块是 CVL 中的一个特殊结构，它允许我们在证明不变量时添加额外假设。可以把它看作是给 Prover 一个关于系统实际行为的小“提示”，这样它就不会浪费时间探索不可能的场景。

我们使用 preserved 关键字，在不变量表达式之后定义一个保留块。最简单的形式如下：

invariant invariant_name()
    invariant_expression
{
    preserved {
        // assumptions about the invariant (关于不变量的假设)
    }

}

有时，我们不希望保留块到处都适用——而只是针对某个特定函数，或只针对某些环境细节（如 msg.sender 或 msg.value）。在这种情况下，我们可以通过可选的函数签名和可选的 with 子句（用于访问事务环境）来扩展语法：

invariant invariant_name(param_1, param_2,...)
    invariant_expression;
{
    preserved functionName(type arg, ...) with (env e) {
        // additional assumptions applicable only for this particular function (仅适用于此特定函数的额外假设)
    }

}

通用保留块和函数特定保留块都在不变量检查的归纳步骤中应用。它们在不变量被假定在前置状态中成立之后、在相应方法被符号执行之前执行，确保 Prover 从一个既数学上有效又上下文上实际的状态开始每个归纳步骤。

到目前为止，保留块决定了分析每个相关函数所依据的假设。然而，在某些情况下，我们可能还想限制不变量首先要检查哪些函数。CVL 为此提供了一个过滤块，写成 filtered { … }。（你可以在 这里 阅读更多关于过滤块的信息）

invariant invariant_name()
    invariant_expression;
    filtered {
        // restrict which functions are checked (限制检查哪些函数)
    }
{
    preserved functionName(type arg, ...) with (env e) {
        // assumptions or requireInvariant statements (假设或 requireInvariant 语句)
    }

}

当存在过滤块时，不变量只针对过滤块中包含的函数进行检查，并且任何保留块都在该受限集合内应用。因此，保留块写在过滤块之后。

过滤块限制了不变量针对哪些函数进行检查。然后，一个通用保留块 (preserved with (env e) { ... }) 适用于该过滤集合中的每个函数。一个函数特定保留块 (preserved functionName(…) with (env e) { ... }) 仅在 Prover 检查该命名函数时应用。如果命名函数未被过滤器包含，则该保留块不起作用。

简而言之，过滤器缩小了不变量应用的范围，而保留块描述了在执行这些函数时必须仍然成立的条件。两者结合使用，为 Prover 提供了检查不变量的清晰路径，而不会被不相关或不可能的状态分散注意力。

然而，在实践中，当不变量由于不切实际的符号执行而失败时，保留块通常比过滤块更受欢迎。这两种机制都限制了 Prover 的搜索空间，并且必须小心使用，以避免削弱证明，但过滤器风险更高，因为它们将整个函数从不变量检查中移除。

保留块通常更安全，因为它们限制了关于状态或执行环境的假设，而不是完全排除行为。因此，它们更适合于排除不可能的状态，同时仍然确保不变量针对所有相关的合约功能进行检查。

现在我们已经了解了理论和语法，让我们通过将其应用于一个真实的合约：Solady 的 WETH 来看看保留块在实践中是如何工作的。

综合应用：验证 WETH 不变量

为了将所有内容整合起来，让我们验证 Solady WETH 合约的一个不变量——这是一个 ERC-20 实现，代表了 Ether (ETH) 与 WETH 代币以 1:1 的比例。该合约的一个关键属性是其 ETH 余额必须始终大于或等于流通中的 WETH 代币总数。

image

定义我们的 WETH 不变量

要验证此不变量，请按照以下步骤操作：

  1. 在你的 Certora 项目目录中，在 contracts 子目录中创建一个名为 ERC20.sol 的新文件，并从 Solady 中复制此代码到其中。
  2. 在相同的 contracts 子目录中创建另一个名为 WETH.sol 的文件，并复制此代码到其中。
  3. 在 specs 子目录中，创建一个名为 weth.spec 的新文件。
  4. 在 weth.spec 中，如下定义不变量 tokenIntegrity()：
invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply();

注意：在 CVL 中，nativeBalances 是原生代币余额的映射——例如，以太坊上的 ETH。地址 $a$ 的余额可以用 $nativeBalances[a]$ 表示。标识符 currentContract 指的是正在验证的主合约。因此，$nativeBalances[currentContract]$ 表示正在验证的合约的原生代币余额。

  1. 添加一个包含 totalSupply() 函数签名的 methods 块：
methods {
    function totalSupply() external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply();
  1. 在 confs 子目录中，创建一个名为 weth.conf 的配置文件：
{
    "files": [\
        "contracts/WETH.sol:WETH"\
    ],
    "verify": "WETH:specs/weth.spec",
    "optimistic_loop" : true,
    "msg": "Check WETH contract integrity"
}

运行验证

完成以上所有步骤后，运行 certoraRun confs/weth.conf 命令来验证我们的规范，并查看类似下图的结果：

image

我们验证运行的上述结果显示，tokenIntegrity 不变量失败了，因为 Prover 发现了一种情况，即合约的 ETH 余额可能小于报告的总供应量。

理解违规

我们的详细分析报告发现，tokenIntegrity 不变量通过了“归纳基础：构造函数之后” ✅，这意味着属性在部署后立即成立。然而，它在“归纳步骤：外部（非视图/纯）方法执行之后” ❌ 失败了，这表明尽管不变量一开始是有效的，但在某些改变状态的函数调用之后，它并不总是成立。

image

为了理解违规的原因，我们需要分析失败函数的调用轨迹。

image

让我们从 deposit() 函数开始。

理解 deposit() 调用的违规

我们对 deposit() 函数调用轨迹的分析揭示了一些不寻常的情况：发送方和接收方都是合约本身 (WETH)。

image

这种情况——合约调用自己的 deposit()——从实际角度来看是荒谬的，因为 WETH 合约不包含任何可以直接或间接调用 deposit() 的代码路径。尽管 Prover 正确地将其识别为理论上可能的交互，但我们可以通过 preserved 块明确告知它忽略此类情况。

理解 receive() 调用的违规

Solidity 合约中的 receive() 函数是一个特殊函数，当合约接收到带有空 calldata 的 Ether 时，它会自动执行。合约只能定义一个这样的函数，并且它必须具有以下形式：

receive() external payable { ... }

receive() 函数不能带参数，不能返回值，并且在纯 ETH 转账（例如通过 .send、.transfer 或原始 ETH 转账）时触发。

在 WETH 实现中，receive() 函数只是将调用转发给 deposit() 函数：

// @dev Equivalent to `deposit()`. (等同于 `deposit()`。)
receive() external payable virtual {
    deposit();
}

正因为如此，任何导致 deposit() 失败的不切实际的执行路径也可能导致 receive() 失败。Prover 将 receive() 视为另一个外部入口点，因此它可能会符号性地假设合约调用自己的 receive() 函数。

这正是在失败轨迹中发生的情况：就像 deposit() 一样，Prover 选择了一条路径，其中发送方和接收方都是合约本身 (WETH)，从而导致了不可能的自调用场景，这在实际执行中不会发生，但会导致不变量符号性地失败。

image

理解 withdraw() 调用的违规

withdraw() 的调用轨迹揭示了一个问题，该问题是由于 Prover 测试了一个极不真实的场景而导致的。要理解它为何失败，让我们使用 Prover 使用的精确值，逐步分析调用轨迹。

前置状态检查（全局状态 #1）

在前置状态检查期间，Prover 假设不变量在函数运行之前成立。在这一点——捕获为全局状态 #1——它设置了一个符号环境，代表在符号化执行 withdraw() 函数之前可能的起始条件。

image

在这种状态下，合约的 ETH 余额被设置为 $2^{256} - 3$，而总代币供应量仅为 $2$。

这意味着合约开始于一个不可能的状态——它持有大量的 ETH，但总代币供应量只有 $2$。没有真实的部署能够达到这种条件，但由于我们没有限制初始状态，Prover 可以自由选择任意值。

此时，我们的不变量成立，因为：

$$ 2^{256} - 3 \geq 2 \quad \text{✅} $$

withdraw() 的符号执行（全局状态 #2）

接下来，Prover 符号化执行 withdraw() 函数：

image

在这里，调用者 (0x8200) 试图提取 $2^{256} - 6$。withdraw() 函数调用内部的 _burn(from, amount)。在实际执行中，如果 $amount > balanceOf(from)$，_burn() 会立即回滚。

然而，Prover 进行符号推理。当它到达检查 $if ($amount > balanceOf(from)$) 时，它将 balanceOf(0x8200) 视为一个无界符号变量。为了探索一条不回滚的路径，它必须假设一个足够大的值来通过检查。

我们可以通过查看 Global State #3 下方的 _burn 操作来找到这个假定的值。轨迹显示了一个经典的“读-修改-写”模式，作用于单个存储槽（调用者的余额）：

image

这告诉我们：

  • Prover 加载了调用者的余额。为了继续，它假设余额为 $2^{256} - 2$。
  • 然后它存储了减法后的新余额 (0x4)。

我们可以用简单的数学来证实这一点：

$$ \begin{aligned} \text{调用前 } 0x8200 \text{ 的余额} &= 2^{256} \ \text{提取数量} &= 2^{256} - 6 \ \text{调用后 } 0x8200 \text{ 的余额应为} &= (2^{256} - 2) - (2^{256} - 6) = 4 \end{aligned} $$

计算结果 $4$ 与存储值 $0x4$ 完全匹配。

算术下溢（全局状态 #3）

一旦 _burn() 更新了调用者的 WETH 余额，它就会更新 WETH 的总供应量。

image

此时，$totalSupply$ 从 $2$ 变为 $8$，因为 $2 - (2^{256} - 6)$ 在 $uint256$ 下溢出，并以模 $2^{256}$ 的方式环绕。

注意：在 Solidity 版本 $\geq 0.8.0$ 中，正常的算术运算（例如 totalSupply -= amount）在下溢时会回滚。然而，当合约使用 unchecked 块或在内联汇编中执行操作时，这不会发生，因为两者都遵循低级算术语义，其中值以模 $2^{256}$ 的方式环绕。

未解决的 ETH 转移和 AUTO-Havoc（全局状态 #5）

_burn() 完成后，withdraw() 尝试使用低级 call 将 ETH 转移给调用者：

call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)

在调用 withdraw() 之前，WETH 合约持有 $2^{256} - 3$ wei。成功调用 withdraw() 将导致 $2^{256} - 6$ wei 转移给调用者，并且应该将合约的 ETH 余额从 $2^{256} - 3$ 减少到 $3$。

如果我们查看 Global State #5 的轨迹，我们看到 Prover 首先正确地进行了这个计算：

image

然而，Prover 并没有就此止步。call 是对一个外部、未知地址 (caller()) 的调用。Prover 无法确定这个被调用者（即调用者的 fallback 函数）的行为。

当 Prover 遇到这种未解决的外部调用时，它会自动应用一个 AUTO-havoc 摘要。

在 AUTO-havoc 下，Prover 假设外部调用成功，但可能任意修改与调用相关的状态变量。它这样做是因为它缺少被调用者代码的具体模型。

在调用轨迹中，我们看到这在正确计算后立即发生：

image

这种 havoc 覆盖了计算出的余额。在下一个状态（全局状态 #6）中，合约的余额为：

image

这意味着 Prover 忽略了计算结果 (3)，并将其任意赋值为 (5) 作为 havoc 摘要的一部分。这个 havoc 后的值将在后置状态检查中使用。

后置状态与不变量失败（全局状态 #7）

withdraw 函数完成后，Prover 在后置状态检查不变量：

$$ nativeBalances[currentContract] \geq totalSupply() $$

此时，符号值为：

  • WETH.balance = 0x5 (由 AUTO-havoc 设置)
  • WETH.totalSupply() = 0x8 (因下溢而损坏)

因此不变量评估为：

$$ 5 \geq 8 \quad \text{❌ (假)} $$

Prover 认为不变量被违反了。

根本原因

这个违规是一个典型的假阳性。它不是因为 WETH 合约的 withdraw() 实现存在逻辑缺陷而发生的。相反，它是由于 Prover 受限的符号推理造成的：

  1. 整个执行路径之所以可能，是因为 Prover 假设了一个不可能的前置状态，其中 balanceOf(msg.sender) ($2^{256} - 2$) 远大于 $totalSupply$ ($2$)。
  2. 这种不切实际的假设，由无限制的符号变量所允许，直接触发了 $totalSupply$ 变量的算术下溢，将其从 $2$ 损坏为 $8$。

auto-havoc 步骤也对最终值有所贡献，但状态已经因下溢而不可挽回地受到影响。

使用保留块修复假性违规

现在已经很清楚，Prover 标记的违规并非因为 WETH 合约存在缺陷，而是因为它探索了在实际执行中永远不会发生的符号状态，我们的下一步是引导 Prover 回归实际行为。

我们通过添加保留块来实现这一点，这些保留块在前置状态检查和符号执行之间引入了额外的假设。这些假设阻止 Prover 进入不可能的执行路径，例如合约自调用或荒谬的代币余额。

修复 deposit() 和 receive() 违规

这两个违规都是由 Prover 假设自调用引起的，其中 WETH 合约被建模为自己的调用者。这在实际执行中是不可能的，但在符号执行中如果不加以限制则是有效的。

我们通过添加一个保留块来修复这个问题，该保留块排除了合约调用自身函数的任何场景：

methods {
    function totalSupply() external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with(env e) {
        require e.msg.sender != currentContract;
    }
}

这一个假设消除了所有自调用轨迹，立即消除了 deposit() 和 receive()（在 Prover UI 中报告为 receiveOrFallback()）中的假阳性。

解决了 deposit() 和 receive() 的自调用问题后，我们现在可以转向第二类假性违规源：withdraw() 中不切实际的符号假设。

修复 withdraw() 违规

withdraw() 中的失败是由不同的原因造成的：Prover 假设 balanceOf(msg.sender) 可以任意大，甚至大于总供应量。这迫使 _burn() 沿着一条应该回滚的路径执行，从而触发下溢并损坏 $totalSupply$。

为了防止这种情况，我们专门为 withdraw() 添加了一个保留块：

methods {
    function totalSupply() external returns (uint256) envfree;
    //we also added the signature of balanceOf() (我们也添加了 balanceOf() 的签名)
    function balanceOf(address) external returns(uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    // Generic Block (通用块)
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    // Function-Specific Block (函数特定块)
    preserved withdraw(uint256 amount) with (env e) {
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

在上面更新的规范中，require balanceOf(e.msg.sender) <= totalSupply(); 这一行指示 Prover 忽略任何用户代币余额超过总供应量的执行路径。

这些保留块共同消除了以前导致假性违规的所有不切实际的执行路径。有了这些约束，我们现在可以重新运行 Prover，检查不变量在实际假设下是否成立。

重新运行验证

应用了这两个修复后，再次运行 Prover 并打开验证结果链接，查看类似于下图的输出。

image

这次，Prover 确认 tokenIntegrity 不变量在所有验证阶段都成立，通过了归纳基础和归纳步骤。

报告显示所有相关函数——包括 deposit()、withdraw()、transfer() 和 approve()——现在都保留了不变量。

image

此时，不变量已成功验证，规范是正确的。然而，我们可以进一步简化它。我们之前添加的两个假设具有相同的结构，并且不依赖于任何函数参数，这意味着我们可以将它们合并到一个更简洁的保留块中。

更简洁统一的规范

在我们的案例中，我们之前添加的两个假设都具有一个重要属性：

“它们仅依赖于事务环境 (env) 和合约的全局状态。它们不依赖于任何特定函数的参数。”

这意味着它们是关于合约的全局真理：

  1. 合约绝不会是自己的调用者。
  2. 调用者的余额绝不会超过总供应量。

由于这两个条件都不依赖于函数的参数，因此都可以安全地放入一个通用的保留块中，如下所示：

methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

当我们使用这个组合块运行 Prover 时，规范被接受而没有错误，不变量在所有验证阶段都成立，如下图所示：

image

构造函数保留块（基本步骤假设）

到目前为止，我们已经讨论了保留块作为在不变量验证的归纳步骤中约束 Prover 的一种方法——即，当检查公共和外部函数是否在假设其先前已成立的情况下保留不变量时。

从 Prover 版本 $8.5.1$ 开始，CVL 也支持构造函数保留块，它适用于不变量验证的基本步骤。

在基本步骤中，Prover 符号化执行构造函数，以验证不变量在部署后立即成立。主合约的存储 (currentContract) 被初始化为零，但在多合约场景中，验证场景中的其他合约以任意符号状态启动。

这与早期 Prover 版本有所不同，在早期版本中，所有合约的存储都被假定为零——对应于一次性全新部署整个系统。当前行为能够更真实地建模已部署的系统，但也意味着基本步骤验证可能从实际部署中永远不会出现的状态开始。

当不变量依赖于与这些外部合约的关系时，符号环境可能会违反在实践中成立的假设，导致基本步骤因纯粹的符号原因而失败。构造函数保留块允许我们显式地重新引入这些假设，确保基本步骤反映真实的部署上下文。

其语法与其他的保留块相似，但作用域限定为构造函数：

preserved constructor() with (env e) {
    require e.block.timestamp != 0;
}

此块仅适用于基本步骤，对归纳步骤或单个函数验证没有影响。

在本章中，WETH 案例研究中的假性违规发生在归纳步骤，因此它们使用通用和函数级保留块解决。当不变量在部署后立即因初始符号环境的不切实际假设而失败时，构造函数保留块最有用。

结论

保留块是细化 CVL 中不变量验证的强大工具。通过将 Prover 约束在切合实际的假设下——无论是在函数执行期间，还是在必要时在部署期间——它们消除了假阳性，同时保持了证明的严谨性。

通过 WETH 案例研究，我们看到精心选择的保留块如何引导 Prover 远离不可能的符号状态，转向有意义的执行，确保不变量在准确反映实际行为的条件下得到验证。

本文是关于使用 Certora Prover 进行形式化验证系列文章的一部分。

  • 原文链接： rareskills.io/post/certo...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
RareSkills
RareSkills
https://www.rareskills.io/

RareSkills

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！