使用 Sload Hook与存储映射

Certora 的形式化验证

将 Sload Hooks 与存储映射结合使用

模块 2：不变量、存储Hook、ghost 变量以及形式化验证通证不变量、存储Hook、ghost 变量以及形式化验证通证

上次更新于 2026 年 2 月 13 日

简介

在上一章中，我们演示了 Sstore hooks 对于验证涉及映射值变化的属性是必要的。该 hook 监控存储写入，捕获每个键的旧值和新值，并执行自定义 CVL 代码以更新 ghost 变量。

我们通过一个简单的 PointSystem 合约来演示这一点，该合约为用户添加点数，将其记录在 pointsOf[address] 中，并更新 totalPoints 中的总数：

Copycontract PointSystem {
    mapping (address => uint256) public pointsOf;
    uint256 public totalPoints;

    function addPoints(address _user, uint256 _amount) external {
        pointsOf[_user] += _amount;
        totalPoints += _amount;
    }
}

然而，在实践中，合约会为了 gas 效率而优化，并在溢出实际上不可能发生的情况下使用 unchecked blocks。例如，上面的 PointSystem 合约可以使用一个 unchecked block，并以一种不会溢出的方式实现。

下面的合约演示了这一点 — 在添加到 pointsOf[address] 时安全地使用了 unchecked block：

Copycontract PointSystemUnchecked {
    mapping (address => uint256) public pointsOf;
    uint256 public totalPoints;

    function addPoints(address _user, uint256 _amount) external {
        totalPoints += _amount;

        unchecked {
            pointsOf[_user] += _amount;
        }
    }
}

这之所以可行，是因为 totalPoints += _amount 首先执行，没有 unchecked，因此它在溢出时回滚并充当断路器。由于 pointsOf[_user] 的每次增量也增加了 totalPoints，因此任何用户累积的点数都不会超过总点数。

然而，Prover 不会考虑这种推理。一旦我们添加了 unchecked block，Prover 就不再假定算术安全性。这意味着它将有意分配初始状态，以触发 unchecked 操作中的环绕行为。

Prover 假定 unchecked blocks 中没有算术安全性

为了演示，让我们针对新的 PointSystemUnchecked 合约运行我们的 PointSystem 规范。以下是规范（不变量和规则），它们现在由于 unchecked block 而失败：

Copyghost mathint g_sumOfUserPoints { // ghost mathint g_sumOfUserPoints
    init_state axiom g_sumOfUserPoints == 0; // 初始状态公理 g_sumOfUserPoints == 0
}

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) { // Sstore hook pointsOf[KEY address account] uint256 newVal (uint256 oldVal)
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal; // g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal
}

invariant sumOfUserPointsEqualsTotalPoints_i() // fails // 不变量 sumOfUserPointsEqualsTotalPoints_i() // 失败
    totalPoints() == g_sumOfUserPoints; // totalPoints() == g_sumOfUserPoints

rule sumOfUserPointsEqualsTotalPoints_r(env e, method f, calldataarg args) { // fails // 规则 sumOfUserPointsEqualsTotalPoints_r(env e, method f, calldataarg args) { // 失败
    require totalPoints() == 0 && g_sumOfUserPoints == 0; // 要求 totalPoints() == 0 && g_sumOfUserPoints == 0

    f(e, args); // f(e, args);
    assert totalPoints() == g_sumOfUserPoints; // 断言 totalPoints() == g_sumOfUserPoints
}

Prover 运行（失败）：链接

这提出了一个问题：当使用 unchecked block 时，为什么 totalPoints 和 g_sumOfUserPoints 会出现差异？答案是，unchecked block 触发 Prover 为任意用户（pointsOf[address]）分配一个非零初始值，以沿执行路径创建溢出场景，而 totalPoints 从零开始（实际初始状态）。结果是，Prover 测试了一个用户的点数大于总点数的状态——这在合约中是不可能的状态。

Prover 设置初始状态以有意触发溢出

现在，我们来分析我们编写的规则和不变量的调用跟踪，以理解违规（一个误报）是如何产生的。

规则调用跟踪

Prover 为地址 0xf 分配一个非零值（pointsOf[0xf] = 0x2），以便稍后，通过在 uint256 范围内添加足够大的值，它可以模拟溢出：

然后执行调用 addPoints(_user=0xf, _amount=$2^{256} - 2$)，这导致 $pointsOf[address] = 0x2 + (2^{256} - 2) = 2^{256} \equiv 0$（由于溢出，新值环绕为零）：

调用 addPoints() 也会增加合约中的 totalPoints。由于 totalPoints 最初为零，添加 $2^{256} - 2$（参数）会得到最终值 $2^{256} - 2$，如下面的跟踪所示：

现在，我们来看看 Sstore hook 逻辑是如何计算 g_sumOfUserPoints 的：

Copyhook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) { // Sstore hook pointsOf[KEY address account] uint256 newVal (uint256 oldVal)
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal; // g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal
}

初始值：

• $g\_sumOfUserPoints = 0$（初始值）
• pointsOf[0xf] (oldVal) = 0x2（初始值）

调用 addPoints(0xf, $2^{256} - 2$) 后的值：

• pointsOf[0xf] (newVal) = 0x0（添加 0x2 和 $2^{256} - 2$ 后的环绕值）
• pointsOf[0xf] (oldVal) = 0x2
• $g\_sumOfUserPoints = 0 + (0x0 - 0x2) = -0x2$

因此，totalPoints（$2^{256} - 2$）不再等于 $g\_sumOfUserPoints$（$-2$）：

不变量调用跟踪

同样的问题也发生在了不变量上。Prover 有意播种了 pointsOf[address] = 0xc00…000，这在调用前状态下大于 totalPoints：

我们不需要另一个调用跟踪就能看出，在最终状态中，记账不一致会发生，并且它们会导致 totalPoints 与 g_sumOfUserPoints 不同。

核心问题

totalPoints 和 g_sumOfUserPoints 都从零开始（如规则前置条件和不变量的 init_state 公理所示），但 Prover 将 pointsOf[user] 设置为非零值以测试溢出路径。

原因是如果 pointsOf[user] 从零开始，则不会发生溢出。将 max_uint256 值加到零只会达到 uint256 的限制，而不是超出它。要在 unchecked 操作 pointsOf[_user] += _amount 中产生溢出，pointsOf[_user] 的初始值必须已经大于零——例如，$2 + (2^{256} - 2) = 2^{256} \equiv 0$。

这种设置创建了一个不切实际的状态，即 $pointsOf[user] > 0$ 而 $totalPoints = 0$，这在实际执行中不会发生，因为这两个值总是在 addPoints() 中一起改变。

定义 ghost 变量和存储之间的真实关系

让我们再次查看 Sstore hook 的实现。

Sstore hook 通过添加每次写入 pointsOf[address] 的变化量（newVal - oldVal）来更新 ghost 变量 g_sumOfUserPoints：

Copyhook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) { // Sstore hook pointsOf[KEY address account] uint256 newVal (uint256 oldVal)
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal; // g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal
}

然而，Prover 不知道 ghost 变量 $g\_sumOfUserPoints$ 和存储 pointsOf[address] 之间的真实关系。

$g\_sumOfUserPoints$ 只是接受它处理的值，Prover 无法确定 pointsOf[address] 的实际值以输入到 $g\_sumOfUserPoints$。结果是，Prover 测试所有可能的值，包括可能导致失败的不切实际的值。

我们接下来需要做的是明确指示 Prover 每个单独用户的点数 (pointsOf[user]) 和用户点数总和（$g\_sumOfUserPoints$）之间的预期关系：$g\_sumOfUserPoints$ 应该始终大于或等于 $pointsOf[user]$。我们可以使用 Sload hook 来强制执行这种关系。

Sload hook 用于映射的语法

在我们继续之前，让我们首先看看用于映射的 Sload hook 的语法和模式。hook 的语法与简单变量的语法相同，只是对于映射，我们必须包含 KEY 关键字。例如：storageVar[KEY address user]：

Copyhook Sload uint256 val balances[KEY address user] { // Sload hook uint256 val balances[KEY address user]
    // implement hook logic // 实现 hook 逻辑
}

在 Sload hook 中，本地 hook 变量 val 捕获从存储映射中读取的值，其中键为 user。

在合约操作中，存储读取发生在变量更新或处理之前。例如，在这行 Solidity 代码 pointsOf[_user] += _amount 中，pointsOf[_user] 必须在添加 _amount 之前读取其当前值。

因此，在数据被处理并分配给 ghost 变量（通过 Sstore hooks）之前，从存储映射中“读取的值”准确无误至关重要。

由于 Prover 不知道存储变量和 ghost 变量之间的关系，我们必须如下明确定义这种关系：

Copyhook Sload uint256 points pointsOf[KEY address account] { // Sload hook uint256 points pointsOf[KEY address account]
    require g_sumOfUserPoints >= points; // 要求 g_sumOfUserPoints >= points;
}

这里，points 是本地 hook 变量，它捕获从映射 pointsOf[address] 中读取的值。此实现限制 Prover 仅探索 $g\_sumOfUserPoints \ge points$ 的状态。

或者，我们可以将 require 视为限制 pointsOf[address] 的值（任何特定用户的点数）始终小于或等于 $g\_sumOfUserPoints$。这意味着 Prover 绝不会测试单个用户的点数超过 ghost 变量跟踪的总点数的场景。

使用 Sload hook 修复 ghost 变量与存储不一致问题

在我们的规范中，我们添加了上面所示的 Sload hook，以强制表示所有点数总和的 ghost 变量（$g\_sumOfUserPoints$）在从存储中读取时始终大于或等于任何单个 $pointsOf[account]$ 值。

这可以防止 Prover 初始化单个账户余额超过总和的状态——这种情况，正如我们所见，会导致误报。

Copyhook Sload uint256 points pointsOf[KEY address account] { // Sload hook uint256 points pointsOf[KEY address account]
    require g_sumOfUserPoints >= points; // 要求 g_sumOfUserPoints >= points;
}

有了这个，CVL 规则和不变量都成功了，属性得到了验证：

Prover 运行（已验证）：链接

总结

• unchecked block 禁用了 Solidity 内置的溢出检查，这导致 Prover 通过分配触发溢出的初始值来探索不安全的算术，以测试实现。
• 这些不切实际的初始值可以通过在 Sload hook 中使用 require 来阻止，从而使 Prover 仅探索指定范围内的状态，例如要求单个点的值不超过总数。

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

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