简介

在本章中，我们将介绍 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（非 payable）

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

Copy
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 语句，如果调用者不是 owner，则会导致 revert。因此，我们的规则需要依赖于 msg.sender。

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

Copy
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() 包含在 method 块中。

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

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

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

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

Copy
increment@withrevert(e);

省略 (e) 会导致编译器错误，迫使你在 methods 块中将该函数声明为 envfree。然而，如果你盲目地遵循这一点并将其声明为 envfree，就会发生 violations，并且 Prover 会指出该函数是依赖于环境的。

现在，最后让我们来看断言：

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

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

然而，当我们运行此规则时，遇到一个意外的 revert 情况——当 msg.value != 0 时。发生这种情况是因为 increment() 是一个非 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++ 会导致溢出 revert（请注意，我们使用的是带有 withrevert 标签的函数调用）：

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

识别出这两种意外的 revert 情况后，必须将这两个条件都作为前置条件包含在内。以下是修改后的规则和 Prover 报告。正如预期，验证通过：

Copy
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 运行记录：link

使用 => 替代 <=> 来放宽前置条件

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

如果我们改为声明“如果非 owner 调用该函数，交易将 revert”，我们可以使用蕴含操作符而不需要前置条件。其他 revert 情况（即 msg.value != 0 和计数器达到最大值）不会引起 violation。我们只关心非 owner 调用该函数时会发生 revert。

话虽如此，现在我们需要形式化验证的属性是：“如果调用者不是 owner，则函数必须 revert。”下面是对应的规则——一个更简单的版本——正如预期，该规则通过了测试：

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

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

Prover 运行记录：link

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

总结

• CVL 中的 env 变量允许对依赖于 msg.sender、msg.value 以及其他全局变量的函数进行推理。
• 这些函数必须包含 env e，可以作为规则参数或者放在规则块内部。
• 这些依赖环境的函数不需要在 methods 块中声明，而 envfree 函数必须被显式声明并标记为 envfree。
• 如果一个依赖环境的函数没有被正确地实现为这样，它仍然可以在 Prover 上编译和运行，但会产生 violations 和警告。
• 如果未充分考虑 msg.value，Prover 将生成由其引发的 violations 和反例。

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