形式化验证账户余额

Certora 形式化验证

形式化验证地址余额

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

最后更新于 2026 年 2 月 13 日

在上一章中，我们讨论了如何在 CVL 中推理依赖于环境的函数，重点关注非 payable 上下文中的 msg.sender。在这些示例中，访问控制取决于调用者的地址。我们还解释了如何处理由意外的非零 msg.value 导致的 reverts。

本章将介绍如何：

• 为需要非零支付的函数（即，标记为 payable 的函数）编写规则
• 如何对账户余额进行断言
• 如何获取当前合约的余额，类似于 Solidity 中的 address(this).balance

e.msg.sender 和 e.msg.value (payable)

考虑一个白名单合约，用户通过调用 register() 函数进行注册，该函数被标记为 payable，并且发送至少 0.05 ETH。注册成功后，调用者的地址 (msg.sender) 通过将其值设置为 true 在 whitelisted 映射中标记为 whitelisted：

Copy/// Solidity

contract PayableWhitelist {
    mapping(address => bool) public whitelisted;

    function register() external payable {
        require(msg.value >= 0.05 ether, "whitelist fee is 0.05 eth");
        require(!whitelisted[msg.sender], "already whitelisted");

        whitelisted[msg.sender] = true;
    }

    function isWhitelisted(address _account) external view returns (bool) {
        return whitelisted[_account];
    }
}

我们将形式化验证以下属性：“调用者当且仅当支付至少 0.05 ETH 时才能成功调用 register()”。为了验证这一点，我们编写了以下 CVL 规则：

Copyrule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    register@withrevert(e);
    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

注意：CVL 中的指数运算使用 ^，而 Solidity 使用 **。

正如我们所知，由于我们使用了双条件运算符，我们必须通过前置条件排除其他 revert 情况。我们添加 $require(!isWhitelisted(e.msg.sender))$ 作为前置条件，以排除 $e.msg.sender$ 最初未在白名单中的情况。

现在，对于双条件断言：

assert $!lastReverted \Leftrightarrow e.msg.value >= 5 * 10^{16}$。

由于我们排除了发送者在白名单中的情况（$require !isWhitelisted(e.msg.sender)$），我们期望这会被 VERIFIED（验证通过），这意味着只有当 $e.msg.value >= 5 * 10^{16}$ 时，函数才不会 revert。

然而，正如形式化验证中常见的情况，一个隐蔽的反例出现了，导致违规。它发生在发送者的 ETH 余额小于预期的发送金额或余额不足时：

这可以通过在前置条件中添加 $require(nativeBalances[e.msg.sender] >= e.msg.value)$ 来修复，从而排除余额不足作为 revert 的原因。

CVL 中的 nativeBalances

$nativeBalances[address]$ 是 CVL 中的一个内置函数，它检索给定地址的当前 ETH 余额。下面，我们要求发送者的 $nativeBalances$ 至少与 $e.msg.value$ 一样大：

Copyrule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

现在，规则是 VERIFIED（验证通过）：

Prover 运行：链接

验证白名单状态

现在我们已经验证了“调用者当且仅当支付至少 0.05 ETH 时才能成功调用 register()”，让我们通过断言调用成功后调用者处于 isWhitelisted 状态来改进规则范围。

以下是要形式化验证的更新属性：“当且仅当调用者发送至少 0.05 ETH 并被列入白名单时，交易才成功。”为了实现这一点，我们可以重用之前的规则并添加一个额外的断言：isWhitelisted。

以下是更新后的 CVL 规则：

Copyrule register_payEthToWhitelist_modified(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16 && isWhitelisted(e.msg.sender);
}

上述规则意味着当且仅当发送者发送至少 0.05 ETH（$e.msg.value >= 5 * 10^{16}$）并被列入白名单（$isWhitelisted(e.msg.sender)$）时，交易才不会 revert（$!lastReverted$）。

换句话说，如果 $!lastReverted$ 为 true（交易成功），那么必须同时满足两个条件——足够的 ETH 和白名单状态。

以下是 Prover 报告，它被 VERIFIED（验证通过）：

Prover 运行：链接

使用 => 而不是 <=> 放宽前置条件

另一种方法是使用蕴含运算符。如果你的目标只是检查当发送不正确的 $msg.value$ 时函数是否 revert，以下规则就足够了。此规则不排除其他 revert 原因，例如发送者没有足够的余额。它只表示如果发送少于 0.05 ether，那么它必定 revert。

Copyrule register_payEthToWhitelist_implication(env e) {
    register@withrevert(e);
    assert e.msg.value < 5 * 10^16 => lastReverted;
}

如果我们使用此规则，我们会看到它被 VERIFIED（验证通过）：

Prover 运行：链接

验证 ETH 余额转移 和自我转移的边界情况

假设我们想形式化验证余额更新，其中 $msg.sender$'s balance decreases by $msg.value$，并且合约的余额增加相同金额。

以下是 CVL 规则，将在下一节中解释：

Copyrule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

currentContract

在上述规则中，我们检索了 $currentContract$ 的先前 ETH 余额（$balanceBefore$）和最终余额（$balanceAfter$）。$currentContract$ 是一个内置变量，指代正在验证的合约。将此变量传递给 $nativeBalances[currentContract]$ 检索所述合约的余额。在这些检索调用之间，register() 函数被调用，因此我们期望余额增加的金额等于 $e.msg.value$。

一个意外的反例将导致此规则失败。Prover 将生成一个反例，其中 $e.msg.sender == currentContract$。Prover 探索所有可能的场景，包括合约调用自身的情况。

这表明合约是向自身发送 ETH，而不是从外部发送者接收新的 ETH。因此，余额实际上并未如预期增加（因为向自身发送 ETH 不会改变总余额），导致断言 $balanceAfter == balanceBefore + e.msg.value$ 失败。

为了解决这个问题，由于 $e.msg.sender$ 不应该是合约本身（$currentContract$），我们需要通过添加前置条件 $require(e.msg.sender != currentContract)$ 来过滤掉 ETH 余额变化验证中的自我转移。

然而，有一个注意事项：在实际项目中，请确保合约不能调用其自身的函数，因为某些情况仍可能导致自我调用。如果未正确检查，这可能会隐藏一个 bug。

以下是修正后的规则和 Prover 报告。正如预期的那样，这被 VERIFIED（验证通过）：

Copyrule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];

    require e.msg.sender != currentContract;
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

Prover 运行：链接

使用 $\Leftrightarrow$ 和 || 验证所有 Revert 情况

假设我们想验证每个可能的 revert 原因都已明确考虑在内。我们可以将断言表示为双条件（$\Leftrightarrow$）并以析取（使用 ORs ||）列出所有 revert 情况。

以下规则指出，revert 的唯一可能原因是：

• 发送者已在白名单中
• 发送者的余额不足
• 发送者转移的资金不足

如果 register() 因任何其他原因 revert，我们将收到断言违规。

以下是规则：

Copyrule register_allRevertCases(env e) {
    bool wasWhitelisted = isWhitelisted(e.msg.sender);
    mathint balanceBefore = nativeBalances[e.msg.sender];

    register@withrevert(e);

    assert lastReverted <=> (
        wasWhitelisted ||              // 发送者已在白名单中
        balanceBefore < e.msg.value || // 发送者余额不足
        e.msg.value < 5 * 10^16        // 发送者转移金额不足
    );
}

正如预期的那样，规则是 VERIFIED（验证通过）：

Prover 运行：链接

总结

• 在 CVL 中，环境变量 $e.msg.value$ 用于表达和验证一个 payable 函数是应该成功还是 revert，通常通过断言最小或精确的所需金额。
• $nativeBalances[address]$ 是一个内置函数，用于检索给定地址的当前 ETH 余额，并可用于通过检查余额变化来验证转移。
• $currentContract$ 是一个内置变量，指代正在验证的合约。
• Prover 会在测试用例中包含自我调用，因此在我们的示例中，我们通过添加 $require(e.msg.sender != currentContract)$ 来排除它们，以避免虚假的反例；请务必谨慎，因为自我调用在某些情况下可能是合理的，并可能在实际合约中揭示真正的 bug。

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

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