在CVL中测试msg.sender和msg.value

Certora 的形式化验证

在 CVL 中测试 msg.sender 和 msg.value

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

上次更新于 2026 年 2 月 13 日

引言

在本章中，我们介绍 CVL 中的 env 变量，它使我们能够为依赖于 msg.sender、msg.value 以及 Solidity 中其他全局变量（如 block 和 tx）的函数制定规则。

我们将重点关注前两个，它们可以从 CVL 变量 env e 中作为 e.msg.sender 和 e.msg.value 访问。

在我们之前的示例中，我们忽略了它们，因为我们验证的函数不依赖于环境变量。因此，我们在 methods 块中将这些函数标记为 envfree。这告诉 Prover 将它们视为纯逻辑，并忽略环境（全局）变量以简化分析。

然而，在实践中，事务严重依赖这些环境变量 (env)，在这里我们将探讨如何使用 msg.sender 和 msg.value 创建规则。

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

考虑一个简单的由所有者控制的计数器合约，其中只允许所有者增加计数器：

contract OwnerCounter {
    uint256 public counter;
    address public owner;

    constructor(address _owner) {
        owner = _owner;
    }

    function increment() public {
        require(msg.sender == owner, "not owner");
        counter++;
    }
}

函数 increment() 有一个 require 语句，如果调用者不是所有者，则会导致 revert。因此，我们的规则需要依赖于 msg.sender。

为了验证属性：“只有所有者才能成功调用 increment()”，我们编写了以下 CVL 规则：

methods {
  function owner() external returns (address) envfree;
  function counter() external returns (uint256) envfree;
}

rule increment_onlyOwnerCanCallIncrement(env e) {
    address current = owner();

    increment@withrevert(e);
    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

在 methods 块中，函数 owner() 和 counter() 被标记为 envfree，因为它们是存储变量的 view 函数，不依赖于环境变量或 env。

然而，函数 increment() 是环境依赖的（因此有参数 e）。如果函数被认为是依赖于环境的，则无需在 methods 块中显式声明。因此，我们没有将 increment() 包含在 methods 块中。

在 rule 块中，env e 声明可以作为参数放置，也可以放置在 rule 块内部。两者都有效，并且仅仅是代码风格偏好：

rule increment_onlyOwnerCanCallIncrement(env e) {
    ...
}

rule increment_onlyOwnerCanCallIncrement() {
    env e;
    ...
}

现在，当我们调用一个环境依赖的 Solidity 函数时，我们必须包含参数 e：

increment@withrevert(e);

省略 (e) 将导致编译器错误，强制你在 methods 块中将函数声明为 envfree。但是，如果你盲目遵循此操作并将其声明为 envfree，则会发生违规，并且 Prover 将指示该函数是环境依赖的。

现在，最后，让我们转向断言：

assert !lastReverted <=> e.msg.sender == current, "access control failed";

这检查 increment() 不会 revert 当且仅当 msg.sender == owner。如果断言失败，则意味着 Prover 找到了一个反例——要么正确的 owner 被阻止调用 increment()，要么一个非 owner 能够成功调用它。

然而，当我们运行这条规则时，我们遇到了一个意外的 revert 情况——当 msg.value != 0 时。这发生是因为 increment() 是一个 non-payable 函数，这意味着它不能接受 Ether。

在 Solidity 中，合约可以通过函数调用接收 Ether，但前提是该函数被显式标记为 payable；否则，事务将 revert。发送的 Ether 数量存储在全局变量 msg.value 中，它以 wei（Ether 的最小单位）为单位保存值。

由于 increment() 未被标记为 payable，任何非零的 msg.value 都会导致 revert，如下面的报告所示：

为了解决这个问题，我们需要将 e.msg.value == 0 作为前置条件。

然后，当 counter == max_uint256 时，又发生了一个意外的 revert。由于 max_uint256 是计数器可以持有的最大值，尝试 counter++ 将导致 overflow revert（请注意，我们使用 withrevert 标签调用该函数）：

为了解决这个问题，我们需要添加另一个前置条件 require(counter() < max_uint256) 以防止计数器溢出。

在确定了这两个意外的 revert 情况后，这两个条件都必须作为前置条件包含在内。下面是修正后的规则和 Prover 报告。正如预期的那样，验证通过：

rule increment_onlyOwnerCanCallIncrement(env e) {
    address current = owner();

   require e.msg.value == 0;
   require counter() < max_uint256;

   increment@withrevert(e);

   assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

Prover 运行：链接

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

我们上面创建的规则是“当且仅当调用者不是所有者时，函数才会 revert”。由于存在其他有效的 revert 条件，即 msg.value != 0 和 counter() == max_uint256，我们必须在前置条件中消除这些可能性，以便“当且仅当调用者不是所有者时，函数才会 revert”为真。

如果我们想改写为“如果非所有者调用函数，则事务会 revert”，我们可以使用蕴含运算符而无需前置条件。其他 revert 情况（即 msg.value != 0 和计数器达到最大值）不会导致违规。我们只关心非所有者调用函数会 revert。

话虽如此，以下是需要形式化验证的属性：“如果调用者不是所有者，则函数必须 revert。” 下面是针对此的规则——一个更简单的规则——正如预期的那样，此规则通过：

rule increment_notOwnerCannotCallIncrement(env e) {
    address current = owner();

    increment@withrevert(e);
    assert e.msg.sender != current => lastReverted, "access control failed";
}

Prover 运行：链接

现在，我们了解了如何为环境依赖的函数编写规则。Prover 使用 e.msg.sender 根据调用者推理执行，并使用 e.msg.value 推理 ETH 转移。在下一章中，我们将更广泛地探讨这两个概念。

总结

• CVL 中的 env 变量允许对依赖于 msg.sender、msg.value 和其他全局变量的函数进行推理。
• 此类函数必须包含 env e，可以作为规则参数或在规则块内。
• 这些环境依赖的函数不需要在 methods 块中声明，而 envfree 函数必须显式声明并标记为 envfree。
• 如果环境依赖的函数没有正确实现，它仍然会在 Prover 上编译和运行，但会产生违规和警告。
• 如果 msg.value 没有得到正确处理，Prover 将生成由此产生的违规和反例。

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

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