简介

在上一章中，我们演示了 Sstore Hook 对于验证涉及映射（mapping）值更改的属性是必要的。该 Hook 会监控存储（storage）写入操作，捕获每个键的旧值和新值，并执行自定义的 CVL 代码来更新 Ghost 变量。

我们通过一个简单的合约 PointSystem 进行演示，该合约为用户增加积分，将其记录在 pointsOf[address] 中，并在 totalPoints 中更新总积分：

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

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

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

下面的合约演示了这一点——在向 pointsOf[address] 增加积分时，安全地使用了 unchecked 块：

Copy
contract 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 的情况下执行，因此如果发生溢出它将回滚（revert），从而起到熔断器的作用。由于每次增加 pointsOf[_user] 也会同时增加 totalPoints，因此任何用户累积的积分永远不可能超过总积分。

然而，Prover 并未考虑这种逻辑推理。一旦我们添加了 unchecked 块，Prover 就不再假设算术的安全性。这意味着它会有意分配那些会在 unchecked 操作中触发回绕（wraparound）行为的初始状态。

Prover 在 unchecked 块中不假设算术安全性

为了演示，让我们在新的 PointSystemUnchecked 合约上运行针对 PointSystem 编写的规范（specifications）。下面是相关的规范（包括 invariant 和 rule），由于 unchecked 块的存在，现在它们会验证失败：

Copy
ghost mathint g_sumOfUserPoints { 
    init_state axiom g_sumOfUserPoints == 0;
}

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

invariant sumOfUserPointsEqualsTotalPoints_i() // fails
    totalPoints() == g_sumOfUserPoints;
    
rule sumOfUserPointsEqualsTotalPoints_r(env e, method f, calldataarg args) { // fails
    require totalPoints() == 0 && g_sumOfUserPoints == 0;

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

Prover 运行结果（失败）：link

这引出了一个问题：为什么在使用 unchecked 块时，totalPoints 和 g_sumOfUserPoints 会产生分歧？答案是，unchecked 块触发了 Prover 为某个任意用户（pointsOf[address]）分配非零初始值，以便在执行路径上制造溢出场景，而 totalPoints 却是从零开始的（实际的初始状态）。结果就是，Prover 测试了一种某个用户的积分大于总积分的状态——这在合约中是一种不可能出现的状态。

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

现在，让我们分析一下我们所写的 rule 和 invariant 的调用追踪（call trace），以了解这种违规（即误报）是如何产生的。

Rule 调用追踪

Prover 将一个非零值分配给地址 0xf（pointsOf[0xf] = 0x2），这样之后通过增加一个在 uint256 范围内足够大的值，它就可以模拟出溢出：

接着执行调用 addPoints(_user=0xf, _amount=2^256 - 2)，这导致 pointsOf[address] = 0x2 + (2^256 - 2) = 2^256 ≡ 0（新值由于溢出回绕为零）：

在合约中调用 addPoints() 也会增加 totalPoints 的值。由于 totalPoints 最初为零，加上 2^256 - 2（传入的参数）导致最终值为 2^256 - 2，如下面的追踪图所示：

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

Copy
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 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）：

Invariant 调用追踪

同样的问题也发生在 invariant 验证中。Prover 在调用前状态中有意植入了 pointsOf[address] = 0xc00…000，这大于 totalPoints：

我们不需要另一个调用追踪就能看出，在最终状态下会发生记账不一致的情况，从而导致 totalPoints 与 g_sumOfUserPoints 不等。

核心问题

totalPoints 和 g_sumOfUserPoints 都是从零开始的（正如 rule 的前提条件和 invariant 的 init_state 公理所示），但 Prover 将 pointsOf[user] 设置为了非零值以测试溢出路径。

原因是如果 pointsOf[user] 从零开始，就不可能发生溢出。将 max_uint256 值加到零上只会达到 uint256 的极限，而不会超出它。为了在 unchecked 操作 pointsOf[_user] += _amount 中制造溢出，pointsOf[_user] 的初始值必须已经大于零——例如，2 + (2²⁵⁶ − 2) = 2²⁵⁶ ≡ 0。

这种设置创造了一种不现实的状态：即 pointsOf[user] > 0 而同时 totalPoints = 0。这在真实执行中是不可能发生的，因为在 addPoints() 中这两个值总是同时变化的。

定义 Ghost 与存储之间的真实关系

让我们再次看一下 Sstore Hook 的实现。

Sstore Hook 通过加上每次写入 pointsOf[address] 时产生的变化量（newVal - oldVal），来更新 Ghost 变量 g_sumOfUserPoints：

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

然而，Prover 并不知道 Ghost 变量 g_sumOfUserPoints 和存储映射 pointsOf[address] 之间的真实关系。

g_sumOfUserPoints 只是简单地接受它所处理的值，而 Prover 无法确定输入到 g_sumOfUserPoints 的 pointsOf[address] 的真实值应该是什么。结果，Prover 会测试所有可能的值，包括那些可能导致失败的不现实的值。

接下来我们需要做的是，显式地指导 Prover 了解每个单个用户的积分（pointsOf[user]）与用户总积分（g_sumOfUserPoints）之间的预期关系：g_sumOfUserPoints 应当始终大于或等于 pointsOf[user]。我们可以使用 Sload Hook 来强制执行这种关系。

针对映射的 Sload Hook 语法

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

Copy
hook Sload uint256 val balances[KEY address user] {
	// implement hook logic
}

在一个 Sload Hook 中，Hook 本地变量 val 会捕获从具有键 user 的存储映射中读取到的值。

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

因此，至关重要的是，在将从存储映射中“读取的值”进行数据处理并将其分配给 Ghost 变量（通过 Sstore Hook）之前，该值必须是准确的。

由于 Prover 不知道存储变量与 Ghost 变量之间的关系，我们必须如下显式地定义这种关系：

Copy
hook Sload uint256 points pointsOf[KEY address account] {
	require g_sumOfUserPoints >= points;
}

在这里，points 是 Hook 本地变量，它捕获了从映射 pointsOf[address] 中读取到的值。这一实现限制了 Prover，使其仅探索 g_sumOfUserPoints 大于或等于 points 的状态。

另外，我们可以将该 require 视为将 pointsOf[address]（任何特定用户的积分）的值约束为始终小于或等于 g_sumOfUserPoints。这意味着 Prover 永远不会测试单个用户的积分超过由 Ghost 变量跟踪的总积分的场景。

使用 Sload Hook 修复 Ghost 与存储的不一致问题

在我们的规范中，我们添加了上面展示的 Sload Hook，以强制要求表示所有积分总和的 Ghost 变量（g_sumOfUserPoints）始终大于或等于从存储中读取出来的任何单个 pointsOf[account] 的值。

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

Copy
hook Sload uint256 points pointsOf[KEY address account] {
	require g_sumOfUserPoints >= points;
}

有了这层约束之后，CVL 的 rule 和 invariant 都能成功通过，属性也就得到了验证：

Prover 运行结果（已验证）：link

总结

• unchecked 块会禁用 Solidity 内置的溢出检查，这导致 Prover 通过分配会触发溢出的初始值来探索不安全的算术操作，从而测试该实现。
• 可以通过在 Sload Hook 中使用 require 来防止产生这些不现实的初始值，这样 Prover 就只会探索指定边界内的状态，例如要求单个积分的值不能超过总计。

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