使用Sstore Hook与存储映射

使用 Certora 进行形式化验证

将 Sstore Hook用于存储映射

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

最后更新于 2026 年 2 月 13 日

简介

在“存储Hook和幽灵变量简介”一章中，我们介绍了带有简单存储变量的存储Hook和幽灵变量。我们展示了Hook可以跟踪那些无法通过公共或外部方法直接访问的存储变量。我们还演示了当某些数量未显式存储但在规范推理中是必需的时，Hook结合幽灵变量可以用于计算并持久化这些值。

如果这些变量是公共或外部可访问的，它们的数值可以通过直接在 CVL 中调用来轻松读取，这将允许根据需要计算任何派生量。

然而，映射是不同的。它们不可枚举——要访问一个值，必须已经知道其键，并且没有内置方法可以从映射中检索“所有键”或“所有值”。

这个限制给验证带来了巨大挑战：许多重要的合约属性需要对映射的所有条目进行推理。由于我们无法直接枚举或检查所有键，我们需要一种机制来跟踪映射的变化。

在本章中，我们将 Sstore Hook的使用扩展到整数、地址和布尔值之外，并将其应用于存储映射——这是规范中的常见模式，因为许多合约都大量依赖映射。

映射的 Sstore Hook语法

在进行代码演示之前，我们首先学习 Sstore Hook用于映射的代码语法/模式。

Sstore Hook——捕获新旧值

以下是捕获存储映射新旧值的 Sstore Hook语法：

hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    // 为 balances 映射实现Hook逻辑，其中：
        // - KEY 为 `user`
        // - 旧（先前）值为 `oldVal`
        // - 新（当前）值为 `newVal`
}

每当一个映射值被写入时，旧值和新值都可以被捕获。

例如，为了验证用户的余额增长不超过 10，我们计算新旧余额之间的差值，并将结果赋给幽灵变量 g_balanceDelta：

ghost mathint g_balanceDelta;

hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    g_balanceDelta = newVal - oldVal;
}

该Hook计算差值（$newVal - oldVal$）并将其存储在幽灵变量 g_balanceDelta 中，该变量表示用户余额在该存储更新期间的变化量。

g_balanceDelta 值随后可以用于验证变化限制。例如：

rule deltaNotMoreThan10() {
    ...
    assert g_balanceDelta <= 10;
}

Sstore Hook——仅捕获新值

我们可以选择只捕获新值而省略旧值，因为旧值是可选的：

hook Sstore balances[KEY address user] uint256 newVal {
    // 实现Hook逻辑
}

这主要用于存储只是被设置，并且验证逻辑中不需要差值（变化量）的情况。

例如，如果我们要推理用户的余额不超过 2000，我们只需捕获 newVal 并将其赋给一个幽灵变量：

ghost mathint g_balance;

hook Sstore balances[KEY address user] uint256 newVal {
    g_balance = newVal;
}

g_balance 值随后可以用于验证余额是否保持在定义的限制内。例如：

rule balanceDoesNotExceed2000() {
    ...
    assert g_balance <= 2000;
}

如果没有 Sstore Hook，跟踪映射中的所有键值是不可能的

为了理解为什么Hook对于验证涉及映射的属性是必不可少的，让我们从一个简单的合约 PointSystem 开始，它执行以下操作：

• 为特定用户添加积分并增加总积分。
• 在映射 pointsOf[address] 中保存每个用户的记录。
• 在变量 totalPoints 中跟踪总体总数。

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

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

现在，我们来验证这个属性：“单个用户积分之和等于总积分。”

不使用 Sstore Hook，一种方法是处理有限数量的用户——例如，两个。我们直接从映射 pointsOf 中读取他们的余额，加上他们的积分，并断言这个和等于 totalPoints。

下面的规则演示了这种方法，其中 totalPoints 和所有 pointsOf 值都从零开始：

rule sumOfUserPointsEqualsTotalPoints() {
    address account1; address account2;
    uint256 amount1; uint256 amount2;

    require account1 != account2;
    require pointsOf(account1) == 0 && pointsOf(account2) == 0; // 每个用户的积分从零开始
    require totalPoints() == 0; // 总数从零开始

    addPoints(account1, amount1);
    addPoints(account2, amount2);

    assert to_mathint(totalPoints()) == pointsOf(account1) + pointsOf(account2);
}

在此证明器运行中，我们看到该属性已得到验证：

证明器运行：链接

通过仅使用两个用户断言相等（即使通过声明额外的账户变量手动添加更多用户），该属性也仅限于该账户子集。这并非我们想要验证的精确属性，因为映射中可能存在许多其他用户，他们的积分被排除在检查之外。

现在，让我们改进这条规则。让 totalPoints 和用户积分 (pointsOf[address]) 从任意值开始，而不是零，方法是删除前置条件 require pointsOf(account1) == 0 && pointsOf(account2) == 0 和 require totalPoints() == 0。

然后我们记录 addPoints() 方法调用前后 totalPoints 和 pointsOf[address] 的值。这样做可以让我们计算由调用引起的增量，并确定每个变量变化了多少。

最后，我们断言总积分 (totalPointsAfter) 等于初始总积分 (totalPointsBefore) 加上 account1 和 account2 积分变化量的总和。这种调整使得无论初始状态如何，该规则都能工作：

rule sumOfUserPointsEqualsTotalPoints_modified() {
    address account1; address account2;
    uint256 amount1; uint256 amount2;

    require account1 != account2;

    // 在方法调用前捕获状态
    mathint totalPointsBefore = totalPoints();
    mathint pointsOfAccount1Before = pointsOf(account1);
    mathint pointsOfAccount2Before = pointsOf(account2);

    // 方法调用
    addPoints(account1, amount1);
    addPoints(account2, amount2);

    // 在方法调用后捕获状态
    mathint totalPointsAfter = totalPoints();
    mathint pointsOfAccount1After = pointsOf(account1);
    mathint pointsOfAccount2After = pointsOf(account2);

    // 计算每个账户的积分变化量
    mathint deltaPointsOfAccount1 = pointsOfAccount1After - pointsOfAccount1Before;
    mathint deltaPointsOfAccount2 = pointsOfAccount2After - pointsOfAccount2Before;

    // 断言：总积分等于初始总积分加上 account1 和 account2 的积分变化量
    assert totalPointsAfter == totalPointsBefore + deltaPointsOfAccount1 + deltaPointsOfAccount2;
}

证明器运行：链接

即使这条规则得到了改进，它也没有准确地表示该属性，因为它只考虑了两个特定用户，而忽略了映射中的所有其他用户。它只证明了用户子集与总数一致。

如果没有 Sstore Hook，即使映射是外部可访问的，跟踪所有用户积分也是不可能的。

使用 Sstore Hook枚举存储映射值

每当合约写入 pointsOf[address] 时，Sstore Hook会捕获新旧值，从而可以计算差值（变化量）并将其赋给一个幽灵变量。我们不通过（从合约中）直接查询所有可能的键来查询映射，而是维护一个幽灵变量跟踪器，该跟踪器记录每次存储写入发生的情况。

让我们实现 Sstore Hook逻辑。如前所述，我们捕获旧值和新值，计算差值（变化量）并将其添加到幽灵变量中以记录总积分。我们将此幽灵变量声明为 g_sumOfUserPoints：

ghost mathint g_sumOfUserPoints;

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

现在，g_sumOfUserPoints 幽灵变量中可以量化单个用户积分之和，下一步是将其用于规则或不变量中，以检查此跟踪器始终等于合约的存储变量 totalPoints。

规则和不变量中的幽灵变量

幽灵变量既可以在规则中也可以在不变量中使用。在以下示例中，我们验证 totalPoints（存储变量）等于 g_sumOfUserPoints（幽灵变量），其值在 Sstore Hook中被跟踪和计算。

将 totalPoints() 等于 g_sumOfUserPoints 作为规则验证

以下是参数化形式的规则，其中 f(e, args) 允许证明器针对所有带有任意参数的合约函数验证该规则。对于下面的规则，我们要求 totalPoints 和 g_sumOfUserPoints 从零开始：

rule sumOfUserPointsEqualsTotalPoints(env e, method f, calldataarg args) {
    require totalPoints() == 0 && g_sumOfUserPoints == 0;

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

证明器运行：链接

或者，我们可以允许 totalPoints 和 g_sumOfUserPoints 从任意值开始，只要它们从相同的值开始：

rule sumOfUserPointsEqualsTotalPoints_alt(env e, method f, calldataarg args) {
    require totalPoints() == g_sumOfUserPoints; // 只要它们从相同的值开始，就可以是任意值

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

证明器运行（已验证）：链接

将 totalPoints() 等于 g_sumOfUserPoints 作为不变量验证

为了归纳（基本情况和归纳步骤）验证同一属性，我们将其写为 CVL 不变量。幽灵变量被初始化为零，并且应用与前一条规则相同的 Sstore Hook：

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_inv()
    totalPoints() == g_sumOfUserPoints;

证明器运行（已验证）：链接

当在 CVL 不变量中使用幽灵变量时，需要使用 init_state axiom 对其进行初始化，以设置正确的起始值——在本例中，g_sumOfUserPoints 为零。

由于每个用户的积分都从零开始，所有用户积分的总和 (g_sumOfUserPoints) 也从零开始。这一点很重要，因为作为归纳过程的一部分，不变量会检查属性是否在基本情况（紧接在构造函数之后）中成立。

当我们之前作为规则验证此属性时，我们测试了两者都从零开始的情况，然后测试了从非零（但相等）值开始的情况。作为不变量，我们只测试两者都从零开始。

原因是不变量必须在构造函数之后立即开始测试（基本情况），其中未初始化的存储变量默认为零。这意味着不变量只能在构造函数显式设置这些值时才能从非零值开始。然而，规则可以假设任何任意的起始状态——可以是零，也可以是非零。

总结

• 在证明涉及值变化的属性时，Sstore Hook对于映射是不可避免的。它通过监视存储槽并捕获映射键的旧值和新值来解决枚举问题。
• 如果没有 Sstore Hook，属性只能针对有限的手动查询键集进行证明，而无法直接监视存储。
• 在规则中，幽灵变量的初始值使用 require 语句进行约束。
• 在不变量中，幽灵变量使用 init_state 断言进行初始化。

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

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