形式化验证 OpenZeppelin 中的 Nonces.Sol

使用Certora进行形式化验证

形式化验证OpenZeppelin中的Nonces.Sol

模块 1：规则和基础CVL语法

最后更新于 2026年2月17日

Nonces，代表"一次性使用的数字"，在数字签名方案中用于防止重放攻击。就本文而言，我们假设读者已经熟悉nonce是什么以及如何使用它们。

OpenZeppelin的nonces.sol 库通过为每个地址使用递增的计数器来跟踪签名者的nonce。以下是完整的库（为简洁起见删除了注释）：

Copyabstract contract Nonces {

    error InvalidAccountNonce(address account, uint256 currentNonce);

    mapping(address account => uint256) private _nonces;

    function nonces(address owner) public view virtual returns (uint256) {
        return _nonces[owner];
    }

    function _useNonce(address owner) internal virtual returns (uint256) {
        unchecked {
            return _nonces[owner]++;
        }
    }

    function _useCheckedNonce(address owner, uint256 nonce) internal virtual {
        uint256 current = _useNonce(owner);
        if (nonce != current) {
            revert InvalidAccountNonce(owner, current);
        }
    }
}

简而言之，这个合约包含：

• nonces(address owner) 是一个视图函数，返回owner的当前nonce。
• _useNonce(address owner) 递增所有者的nonce并返回递增前的nonce值。例如，如果Alice的nonce是2，我们为她的账户调用_useNonce，那么_useNonce将返回2，但在函数执行后，她当前的nonce变为3。
• _useCheckedNonce(address owner, uint256 nonce) 会递增nonce，但如果nonce参数不等于当前nonce，则会回滚。例如，如果Alice的当前nonce是15，那么提供除15以外的任何nonce参数都会导致回滚。函数调用后，Alice的nonce将变为16。

这与我们教程前面介绍的Counter示例没有太大不同，因此Certora为该库编写的规则将很容易解释。

以下是一些将被证明的属性：

• Nonce只递增
• 递增nonce永远不会失败
• 递增一个nonce不会影响其他nonce

Nonces.sol规范

这是Certora为nonces.sol编写的规范。

辅助函数

该规范包含一个辅助CVL函数，用于检查nonce是否不是uint256的最大值。实际上，计数器不可能达到那么高：

Copyfunction nonceSanity(address account) returns bool {
    return nonces(account) < max_uint256;
}

Nonce只递增

我们将从最简单的规则开始，因为我们在参数化规则章节中看到了类似的内容：

Copy// address account in the argument is equivalent to
// declaring it inside the function body
rule nonceOnlyIncrements(
address account)
 {
    require nonceSanity(account);

    mathint nonceBefore = nonces(account);

    env e; method f; calldataarg args;
    f(e, args);

    mathint nonceAfter = nonces(account);

    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1, "nonce only increments";
}

这条规则表示“所有交易要么导致nonce不变，要么恰好增加1。”

useNonce规则

useNonce规则包含两个断言：

• 调用useNonce()永远不会回滚
• 对账户A递增nonce不会影响所有其他账户，即他们的nonce不会改变。

Copyrule useNonce(address account) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    mathint nonceUsed = useNonce@withrevert(account);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    // liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

让我们逐段解释：

Copyrequire nonceSanity(account);

这行代码确保证明器不会测试当nonce为type(uint256).max时的（不可能的）情况。

Copyaddress other;

这个other是我们如何获取规则参数中指定的account之外的“任何其他账户”的引用。注意，规则并不要求account != other作为先决条件——这稍后会处理。

Copymathint nonceBefore = nonces(account);
mathint otherNonceBefore = nonces(other);

这读取状态转换前account和other的nonce值。

Copymathint nonceUsed = useNonce@withrevert(account);
bool success = !lastReverted;

mathint nonceAfter = nonces(account);
mathint otherNonceAfter = nonces(other);

代码mathint nonceUsed = useNonce@withrevert(account);是关键行，因为nonce在那里递增。我们在nonceAfter和otherNonceAfter中记录新的nonce状态。

现在让我们看看这些断言：

Copy// liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";

回想一下，函数useNonce返回刚刚被消耗的nonce，因此断言nonceBefore == nonceUsed。

最后的断言表明没有其他nonce被改变。其逻辑可以使用逆否规则推导出来。

根据蕴含的逆否规则，如果 A → B，那么 !B → !A。假设A表示other ≠ account，B表示otherNonceBefore = otherNonceAfter。那么我们可以说“如果other不等于account，那么other的nonce没有改变”。因此，我们可以写成other ≠ account蕴含otherNonceBefore = otherNonceAfter，或者说 A → B。使用逆否规则，我们可以说 !B → !A，或者等价地，otherNonceBefore ≠ otherNonceAfter（发生了改变）蕴含other = account，这正是最后一个断言所陈述的内容。

useCheckedNonce规则

最终的规则复用了之前示例中的大量逻辑，我们在此不再解释。关键的区别在于这一行：assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";。回想一下，useCheckedNonce只有在传递给它的nonce等于用户的当前nonce时才会成功（不回滚）。因此，双向条件运算符编码了“如果nonce匹配，则交易保证成功。否则，保证回滚。”

Copyrule useCheckedNonce(address account, uint256 currentNonce) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    useCheckedNonce@withrevert(account, currentNonce);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    //// 看这里 ////
    // liveness
    // the to_mathint cast makes it explicit to have the same type on both sides
    assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";

    // effect
    assert success => nonceAfter == nonceBefore + 1, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

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

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