形式化验证一个ERC-20代币

Certora 的形式化验证

形式化验证 ERC-20 代币

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

最后更新日期：2026 年 2 月 13 日

引言

在本章中，我们将形式化验证 Solmate 的 ERC-20 实现，其中包括以下内容：

• 标准的状态变更函数：transfer()、approve()、transferFrom()
• 标准的视图函数：totalSupply()、balanceOf()、allowance()
• 扩展的内部函数：_mint()、_burn()

请注意，尽管 Solmate 的 ERC-20 实现包含一个 permit() 函数，但我们有意将其排除，因为本系列尚未涵盖对加密签名的形式化验证。

Solmate 的 ERC-20 代币之所以有趣，在于其在修改总供应量和余额时使用 unchecked 块以节省 gas。由于 unchecked 块绕过了 Solidity 内置的溢出检查，因此形式化验证对于数学证明溢出不可能发生至关重要。

以下是简化的 Solmate ERC-20 实现，仅移除了 permit() 函数：

Copy// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity >=0.8.0;

/// @notice 现代且节省 gas 的 ERC20 + EIP-2612 实现。
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author 修改自 Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev 在不更新 totalSupply 的情况下，请勿手动设置余额，因为所有用户余额的总和不得超过它。
abstract contract ERC20 {
    /*//////////////////////////////////////////////////////////////
                                 EVENTS
    //////////////////////////////////////////////////////////////*/

    event Transfer(address indexed from, address indexed to, uint256 amount);

    event Approval(address indexed owner, address indexed spender, uint256 amount);

    /*//////////////////////////////////////////////////////////////
                            METADATA STORAGE
    //////////////////////////////////////////////////////////////*/

    string public name;

    string public symbol;

    uint8 public immutable decimals;

    /*//////////////////////////////////////////////////////////////
                              ERC20 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 public totalSupply;

    mapping(address => uint256) public balanceOf;

    mapping(address => mapping(address => uint256)) public allowance;

    /*//////////////////////////////////////////////////////////////
                               CONSTRUCTOR
    //////////////////////////////////////////////////////////////*/

    constructor(
        string memory _name,
        string memory _symbol,
        uint8 _decimals
    ) {
        name = _name;
        symbol = _symbol;
        decimals = _decimals;
    }

    /*//////////////////////////////////////////////////////////////
                               ERC20 LOGIC
    //////////////////////////////////////////////////////////////*/

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        allowance[msg.sender][spender] = amount;

        emit Approval(msg.sender, spender, amount);

        return true;
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        balanceOf[msg.sender] -= amount;

        // 不会溢出，因为所有用户余额的总和不会超过 uint256 的最大值。
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(msg.sender, to, amount);

        return true;
    }

    function transferFrom(
        address from,
        address to,
        uint256 amount
    ) public virtual returns (bool) {
        uint256 allowed = allowance[from][msg.sender]; // 为有限的批准节省 gas。

        if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

        balanceOf[from] -= amount;

        // 不会溢出，因为所有用户余额的总和不会超过 uint256 的最大值。
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(from, to, amount);

        return true;
    }

    /*//////////////////////////////////////////////////////////////
                        INTERNAL MINT/BURN LOGIC
    //////////////////////////////////////////////////////////////*/

    function _mint(address to, uint256 amount) internal virtual {
        totalSupply += amount;

        // 不会溢出，因为所有用户余额的总和不会超过 uint256 的最大值。
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(address(0), to, amount);
    }

    function _burn(address from, uint256 amount) internal virtual {
        balanceOf[from] -= amount;

        // 不会下溢，因为用户的余额永远不会大于总供应量。
        unchecked {
            totalSupply -= amount;
        }

        emit Transfer(from, address(0), amount);
    }
}

上述 ERC-20 实现是一个抽象合约，需要一个继承合约使其具体化。我们还需要通过外部函数暴露 _mint() 和 _burn()，以便 Prover 在验证过程中调用它们。为了满足这两个要求，我们使用一个 harness 合约。

一个 harness 合约继承自待验证的合约，通过将其内部函数封装为外部函数，使其可供 Prover 访问。它还可以定义辅助视图或纯函数，提供状态查询和实用计算，以简化规则和不变量逻辑。

对于此规范，harness 是一个最小合约，它继承了抽象的 ERC-20 实现，既提供了具体合约，又使其内部函数（_mint() 和 _burn()）可供验证。

以下是 harness 合约：

Copy// SPDX-License-Identifier: MIT
pragma solidity ^0.8.25;

import "src/Solmate/ERC20.sol";

contract ERC20Harness is ERC20 {
    constructor (
        string memory _name,
        string memory _symbol,
        uint8 _decimals
    ) ERC20(_name, _symbol, _decimals) {}

    /// 留待访问控制；集成者应实现自己的访问控制。
    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }

    /// 留待访问控制；集成者应实现自己的访问控制。
    function burn(address _from, uint256 _amount) external {
        _burn(_from, _amount);
    }
}

形式化验证 ERC-20 属性的顺序方法

在本章中，我们采用顺序方法形式化验证 ERC-20 合约的属性。大纲如下：

• 意图是什么？用户希望发生什么？
  • 哪些函数实现此意图？
  • 如果调用成功，预期的状态变化如何体现？
  • 如果调用成功，对于未涉及方，不应发生哪些意想不到的副作用或状态变化？
  • 如果调用回滚，是什么导致了回滚？
• 哪些不变量必须始终成立？
• 哪些未经授权的操作（由函数或调用者执行）必须不允许？

该过程如下图所示：

然后，我们按照下面的编号顺序进行每个步骤：

1. 验证函数正确性（调用成功或回滚）

transfer()

让我们从发送代币的意图开始——我们验证当发送者转移代币时，接收者收到指定的确切数量。这是通过 transfer() 函数实现的。

以下是 transfer() 函数的实现：

Copyfunction transfer(address to, uint256 amount) public virtual returns (bool) {
    balanceOf[msg.sender] -= amount;

    // 不会溢出，因为所有用户余额的总和不会超过 uint256 的最大值。
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

以下是验证发送者余额减少和接收者余额增加确切数量的 CVL 规则：

Copyrule transfer_effectOnBalances(env e) {
    address receiver;
    uint256 amount;

    require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // 将被不变量替换

    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    }
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

让我们进一步解释这条规则。

前置条件限制 Prover 不得分配其总和超过 $max\_uint256$ 限制的余额，如下所示：

Copyrequire balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // 将被不变量替换

这是必要的，因为 transfer() 函数在将 $amount$ 转移到 balanceOf[address] 时使用了 unchecked 块，这会导致 Prover 将溢出视为“可能”并报告误报。

然而，由于此前置条件将值限制在 $max\_uint256$ 范围内，Prover 无法测试实际可能发生的溢出条件，这可能会掩盖溢出错误。因此，应通过已验证的不变量正式排除此情况，我们将在“requireInvariant”部分讨论此问题。

在前置条件之后，我们执行以下步骤：

• 记录 transfer() 调用前发送者和接收者的余额。
• 调用 transfer()。
• 再次记录调用后发送者和接收者的余额。我们将使用这些值在断言中推断发送者和接收者的余额变化。

Copymathint senderBalanceBefore = balanceOf(e.msg.sender);
mathint receiverBalanceBefore = balanceOf(receiver);

transfer(e, receiver, amount);

mathint senderBalanceAfter = balanceOf(e.msg.sender);
mathint receiverBalanceAfter = balanceOf(receiver);

现在是断言：

• 如果发送者和接收者不同，我们断言：
  • 发送者的余额减少了 $amount$。
  • 接收者的余额增加了 $amount$。
• 如果发送者与接收者相同，我们断言余额保持不变：

Copyif (receiver != e.msg.sender) {
    assert senderBalanceAfter == senderBalanceBefore - amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}
else {
    assert senderBalanceAfter == senderBalanceBefore;
    assert receiverBalanceAfter == receiverBalanceBefore;
}

断言确认了直接的价值转移，没有扣除，如 Prover 运行所示。

transfer() 回滚

我们刚刚介绍了成功的转账路径。接下来，我们验证 transfer() 在失败条件下会回滚。

以下 CVL 规则解释了断言中的所有回滚条件。它使用双条件运算符 (<=>) 来表示当且仅当列出的某个条件为真时才会发生回滚。这些条件是：

• 发送者余额不足。
• ETH 随同不可支付的函数调用发送。

Copyrule transfer_reverts(env e) {
    address receiver;
    uint256 amount;

    mathint senderBalance = balanceOf(e.msg.sender);

    transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        senderBalance < amount || // 发送者余额不足
        e.msg.value != 0 // 随调用 transfer 发送 ETH（不可支付）
    );
}

对于此规则，我们没有定义任何前置条件，因此我们直接记录转账调用之前的状态。以下行捕获转账调用之前的值：

Copymathint senderBalance = balanceOf(e.msg.sender);

对于断言，只有两种情况被列为回滚原因。第一种情况是发送者的余额小于要转账的 $amount$，因为发送者不应该能够发送比他们拥有的更多的代币：

Copyassert isLastReverted <=> (
    senderBalance < amount || // 余额不足
    e.msg.value != 0
);

第二种情况（$e.msg.value \neq 0$）导致回滚，因为该函数是不可支付的。任何非零的 $msg.value$ 都会导致其失败。这是一个不可支付函数的回滚条件，在 ERC-20 的形式化验证中会频繁出现。

断言使用双条件运算符来保证函数仅在两种情况之一发生时回滚。这意味着不应有其他条件导致函数回滚。以下是 Prover 运行。

transferFrom()

在这里，我们验证当授权的 spender 代表持有者转移代币时，接收者收到指定的确切数量。这是通过 transferFrom() 函数完成的，如下面的 Solidity 实现所示。此转移引起的 allowance 变化将在后面的部分进行分析。

Copyfunction transferFrom(
    address from,
    address to,
    uint256 amount
) public virtual returns (bool) {
    uint256 allowed = allowance[from][msg.sender]; // 为有限的批准节省 gas。

    if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

    balanceOf[from] -= amount;

    // 不会溢出，因为所有用户余额的总和不会超过 uint256 的最大值。
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(from, to, amount);

    return true;
}

以下规则几乎与 transfer_effectOnBalances 规则相同——唯一的区别是它调用了 transferFrom()。它执行以下操作：

• 前置条件：将持有者和接收者余额的总和限制在 $max\_uint256$ 范围内，以防止 Prover 在 unchecked 块中探索溢出场景。
• 调用前和调用后状态：记录 transferFrom() 调用前后两个账户的余额，以便我们在断言中验证确切的余额变化。
• 断言：
  • 如果 $receiver \neq holder$，断言它们的余额相差 $amount$。
  • 如果 $receiver = holder$，断言余额保持不变。

Copyrule transferFrom_effectOnBalances(env e) {
    address holder;
    address receiver;
    uint256 amount;

    require balanceOf(holder) + balanceOf(receiver) <= max_uint256; // 稍后将形式化验证

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    }
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

查看 Prover 运行。

transferFrom() 回滚

transferFrom() 回滚规则模式也与 transfer() 规则相似，除了涉及 spender 的一个额外情况。如下所示，如果 spender 没有足够的 allowance（即，如果 $spenderAllowance < amount$），事务将回滚：

Copyrule transferFrom_reverts(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint holderBalance = balanceOf(holder);
    mathint spenderAllowance = allowance(holder, e.msg.sender);

    transferFrom@withrevert(e, holder, receiver, amount); // spender 是 msg.sender
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        holderBalance < amount ||
        spenderAllowance < amount ||
        e.msg.value != 0
    );
}

所有其他回滚场景与 transfer() 规则中的相同。以下是 Prover 运行。

allowance 的变化

当 transferFrom() 调用成功时，持有者对 spender 的批准 allowance 会改变。transferFrom() 实现中包含此条件：

Copyif (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

这意味着如果当前 allowance 未设置为 uint256 的最大值，则花费的 $amount$ 将从中扣除。如果 allowance 设置为最大值，则它表现为无限 allowance 且保持不变。

此行为在下面显示的 CVL 规则的断言部分中捕获：

Copyrule transferFrom_allowanceChange(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint spenderAllowanceBefore = allowance(holder, e.msg.sender);

    transferFrom(e, holder, receiver, amount);
    mathint spenderAllowanceAfter = allowance(holder, e.msg.sender);

    if (spenderAllowanceBefore != max_uint256) {
        assert spenderAllowanceAfter == spenderAllowanceBefore - amount;
    }
    else {
        assert spenderAllowanceAfter == spenderAllowanceBefore;
    }
}

Prover 运行：链接

approve()

Allowance 在 transferFrom() 函数中扣除，但实际的 allowance 批准是在 approve() 函数中设置的。以下是其实现：

Copyfunction approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount;

    emit Approval(msg.sender, spender, amount);

    return true;
}

allowance 变量是一个公共的嵌套映射。因此，Solidity 会自动生成一个 getter 函数，允许它在 CVL 中直接调用（allowance(e.msg.sender, spender)）：

Copyrule approve_spenderAllowance(env e) {
    address spender;
    uint256 amount;

    approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;

    mathint approvedAmountAfter = allowance(e.msg.sender, spender);

    assert !isReverted => approvedAmountAfter == amount;
    assert isReverted <=> e.msg.value != 0;
}

Prover 运行：链接

为了简洁，上面的规则结合了成功和回滚两种情况，使用蕴含和双条件运算符，而不是为每种情况创建单独的规则或使用 if/else 块。

approve() 函数必须在 $env \ e$ 上下文中调用，因为它依赖于全局环境变量，例如 $msg.sender$ 和 $msg.value$。具体来说，该函数使用 $msg.sender$ 来确定哪个地址正在为 $spender$ 设置 allowance：

Copyfunction approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount; // 依赖于 msg.sender
    ...
}

现在进行断言：

• 如果函数调用成功，allowance 将设置为指定的 $amount$。
• 当且仅当 $e.msg.value$ 非零时，函数才会回滚，这意味着 ETH 随 approve 函数调用发送。

Copyassert !isReverted => approvedAmountAfter == amount;
assert isReverted <=> e.msg.value != 0;

transfer()、transferFrom() 和 approve() 在成功调用时返回 true

除了它们的状态变更操作外，transfer()、transferFrom() 和 approve() 在成功执行时必须返回 true，这是 ERC-20 标准所要求的。

以下规则调用其各自的函数，带有 @withrevert 以捕获它们是否回滚，将结果存储在 isLastReverted 中，并断言如果调用未回滚，则必须返回 true：

Copyrule transfer_successReturnsTrue(env e) {
    address receiver;
    uint256 amount;

    bool retVal = transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule transferFrom_successReturnsTrue(env e) {
    address holder;
    address receiver;
    uint256 amount;

    bool retVal = transferFrom@withrevert(e, holder, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule approve_successReturnsTrue(env e) {
    address spender;
    uint256 amount;

    bool retVal = approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;

    assert !isReverted => (retVal == true);
}

Prover 运行：链接

这些规则验证 transfer()、transferFrom() 和 approve() 在成功调用时返回 true。

mint()

增加总供应量是 mint 的意图。同时，新铸造的代币被分配给接收者，增加了他们的余额。下面的 Solidity 实现显示 totalSupply 和 balanceOf[to] 都增加了 $amount$：

Copyfunction _mint(address to, uint256 amount) internal virtual {
    totalSupply += amount;

    // 不会溢出，因为所有用户余额的总和不会超过 uint256 的最大值。
    unchecked {
        balanceOf[to] += amount;
    }
    ...
}

balanceOf[address] 的增加发生在 unchecked 块内，而 totalSupply 的增加发生在 unchecked 块外，并受到 Solidity 编译器溢出检查的保护。

由于 unchecked 块，Prover 探索了余额溢出的可能性，即使这实际上不可能发生，因为余额会随着 totalSupply 的增加而增加。为了防止误报，我们添加了前置条件 require totalSupply() >= balanceOf(receiver)。

以下是捕获总供应量增加和接收者余额相应增加的 CVL 规则：

Copyrule mint_increasesTotalSupplyAndBalance() {
    address receiver;
    uint256 amount;

    require totalSupply() >= balanceOf(receiver); // 将被不变量替换

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}

Prover 运行：链接

按照既定模式，我们捕获 mint() 方法调用前后的状态：

Copymathint totalSupplyBefore = totalSupply();
mathint receiverBalanceBefore = balanceOf(receiver);

mint(receiver, amount);

mathint totalSupplyAfter = totalSupply();
mathint receiverBalanceAfter = balanceOf(receiver);

现在是断言，其中总供应量增加和接收者余额的相应增加都等于 $amount$：

Copyassert totalSupplyAfter == totalSupplyBefore + amount;
assert receiverBalanceAfter == receiverBalanceBefore + amount;

mint() 回滚

当且仅当总供应量和铸造 $amount$ 的总和超过 $max\_uint256$ 时，mint() 函数才会回滚。这表示一个溢出场景。以下是捕获此行为的 CVL 规则：

Copyrule mint_reverts() {
    address receiver;
    uint256 amount;

    mathint totalSupply = totalSupply();

    mint@withrevert(receiver, amount);
    bool isReverted = lastReverted;

    assert isReverted <=> totalSupply + amount > max_uint256;
}

Prover 运行：链接

burn()

铸造增加了总供应量，而销毁的意图是减少总供应量。每次销毁操作都会减少总供应量和代币所有者的余额。

以下是实现：

Copyfunction _burn(address from, uint256 amount) internal virtual {
    balanceOf[from] -= amount;

    // 不会下溢，因为用户的余额永远不会大于总供应量。
    unchecked {
        totalSupply -= amount;
    }

    emit Transfer(from, address(0), amount);
}

以下是捕获总供应量减少和代币所有者余额减少的规则：

Copyrule burn_decreasesTotalSupplyAndBalance() {
    address holder;
    uint256 amount;

    require totalSupply() >= balanceOf(holder); // 将被不变量替换

    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Prover 运行：链接

在 _burn() 函数中，操作 totalSupply -= amount 位于 unchecked 块内。因此，Prover 探索了下溢的可能性，即使这实际上不可能发生。为了防止这种情况，我们在规则中添加了前置条件 require totalSupply() >= balanceOf(holder)。

对于代码的其余部分，模式与 mint() 相似，只是余额和总供应量都按指定的 $amount$ 减少，这与销毁时的预期相符。

burn() 回滚

当且仅当持有者的余额小于要销毁的 $amount$ 时，burn() 函数才会回滚。这是一个 Solidity 强制的安全检查，当 balanceOf[from] -= amount（在 unchecked 块外部执行）尝试减去的数量超过可用余额时，会触发回滚。

以下是验证此行为的 CVL 规则：

Copyrule burn_reverts(env e) {
    address holder;
    uint256 amount;

    mathint holderBalance = balanceOf(holder);

    burn@withrevert(holder, amount);
    bool isReverted = lastReverted;

    assert isReverted <=> holderBalance < amount;
}

Prover 运行：链接

2. transfer、transferFrom、mint 和 burn 的意外副作用

在验证了函数在成功和回滚场景下行为正确，并且没有发生意外副作用之后，我们现在验证对于未涉及方没有意外副作用或状态变化。

一个函数可能会无意中导致未参与操作的账户存储发生变化。对于此合约，我们形式化验证了 transfer()、transferFrom()、mint() 或 burn() 不会修改未参与账户的余额。

每条规则都遵循相同的模式：我们指定一个地址为未参与（通过 require 语句），捕获其操作前的余额，执行函数，然后断言余额保持不变。这证明只有明确作为参数传递的账户才受到影响：

Copyrule noUninvolvedBalancesAreAffectedByDirectTransfer(env e) {
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != e.msg.sender;

    mathint otherBalanceBefore = balanceOf(other);
    transfer(e, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByTransferFrom(env e) {
    address holder;
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != holder;

    mathint otherBalanceBefore = balanceOf(other);
    transferFrom(e, holder, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByMint() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    mint(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByBurn() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    burn(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

Prover 运行：链接

3. 不变量

现在我们已经验证了成功和回滚路径，并且没有发生意外副作用，我们可以继续讨论不变量——无论调用哪个函数，使用什么参数，或者按顺序进行多少次有效调用，都必须始终成立的条件。

余额总和必须等于总供应量

在任何情况下，所有余额的总和都不应与总供应量不同，因为任何差异都表明代币在 mint() 或 burn() 之外被创建或销毁——要么给予用户比实际存在的代币更多的代币，要么导致代币从系统中消失。以下 CVL 规范形式化验证了此不变量：

Copyghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

hook Sload uint256 balance balanceOf[KEY address account] {
    require g_sumOfBalances >= balance;
}

invariant totalSupplyEqualsSumOfBalances()
    to_mathint(totalSupply()) == g_sumOfBalances;

Prover 运行：链接

让我们进一步讨论。

第一个块将幽灵变量 $g\_sumOfBalances$ 声明为 mathint 并将其初始化为零。如果没有此初始化，Prover 将分配任意起始值，这可能导致误报：

Copyghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

现在，这是 Sstore Hook，其中幽灵变量 $g\_sumOfBalances$ 用于存储和跟踪总账户余额的变化：

Copyhook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

下面的 Sload Hook限制余额读取，以防止 Prover 分配大于跟踪余额总和的值：

Copyhook Sload uint256 balance balanceOf[KEY address account] {
    require g_sumOfBalances >= balance;
}

最后，我们形式化验证了总供应量等于所有余额的总和：

Copyinvariant totalSupplyEqualsSumOfBalances()
    to_mathint(totalSupply()) == g_sumOfBalances;

requireInvariant — 作为前置条件的不变量

不变量 totalSupplyEqualsSumOfBalances 不仅作为一个通用属性有用，而且我们还将其作为已证明的假设用于代替前置条件。

除了其明显的含义（总供应量等于所有余额的总和）之外，不变量 $totalSupply() = g\_sumOfBalances$ 还隐含着：

• 总供应量始终大于或等于任何单个余额。
• 总供应量和余额总和都保持在 $max\_uint256$ 范围内。

回想一下，早期的 transfer 和 transferFrom 规则包含一个前置条件，要求余额保持在 $max\_uint256$ 范围内。这可能隐藏了一个溢出错误，因为前置条件假定并限制了余额，这可能无意中过滤掉了错误可能出现的状态。

因此，使用经过验证的不变量 totalSupplyEqualsSumOfBalances 作为前置条件更安全，因为它确保规则在“所有”可达状态中都具有此属性时执行。

我们现在将 require 语句替换为 requireInvariant totalSupplyEqualsSumOfBalances，如下所示：

Copyrule transfer_effectOnBalances_requireInvariant(env e) {
    address receiver;
    uint256 amount;

    // 之前是: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    }
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

rule transferFrom_effectOnBalances_requireInvariant(env e) {
    address holder;
    address receiver;
    uint256 amount;

    // 之前是: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    }
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

此外，burn 和 mint 规则包含一个前置条件，要求总供应量大于或等于持有者和接收者的余额。此 require 前置条件是一个假定的约束，为了安全起见，我们将其替换为已证明的不变量。

由于不变量 totalSupplyEqualsSumOfBalances 也隐含着总供应量大于或等于所有单个余额，因此我们可以将 require 前置条件替换为 requireInvariant totalSupplyEqualsSumOfBalances：

Copyrule mint_increasesTotalSupplyAndBalance_requireInvariant() {
    address receiver;
    uint256 amount;

    // 之前是: `require totalSupply() >= balanceOf(receiver)`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}

rule burn_decreasesTotalSupplyAndBalance_requireInvariant() {

    address holder;
    uint256 amount;

    // 之前是: `require totalSupply() >= balanceOf(holder)`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Prover 运行：链接

4. 未经授权的操作——不允许方法和调用者改变状态

这验证了某些状态更改或操作不应在明确允许的函数或调用者之外发生。

只有某些方法可以改变存储/状态

让我们从属性开始：“只有 mint() 和 burn() 可以改变总供应量。”

下面的规则是一个参数化规则（参见“参数化规则简介”章节），其中函数可以任意调用（通过 $f(e, args)$），但只有 mint() 和 burn() 允许改变 totalSupply。这是通过断言强制执行的，其中 $totalSupplyAfter \neq totalSupplyBefore$ 隐含（$\implies$）只有这两个函数可能导致这种变化：

Copyrule onlyMethodsCanChangeTotalSupply(env e, method f, calldataarg args) {
    mathint totalSupplyBefore = totalSupply();

    f(e, args);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter != totalSupplyBefore => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:burn(address,uint256).selector
    );
}

虽然这断言了哪些函数被允许修改 totalSupply，但也暗示了所有其他函数都无权这样做。

此类别中其余的规则如下所示，并遵循相同的模式：

• 只有 mint()、burn()、transfer() 和 transferFrom() 可以改变账户余额：

Copyrule onlyMethodsCanChangeAccountBalances(env e, method f, calldataarg args) {
      address account;
      mathint balanceBefore = balanceOf(account);

      f(e, args);
      mathint balanceAfter = balanceOf(account);

      assert balanceBefore != balanceAfter => (
          f.selector == sig:transfer(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector ||
          f.selector == sig:mint(address,uint256).selector ||
          f.selector == sig:burn(address,uint256).selector
      );
}

• 只有 approve() 和 transferFrom() 可以改变 allowance：

Copyrule onlyMethodsCanChangeAllowance(env e, method f, calldataarg args) {
      address holder;
      address spender;

      mathint allowanceBefore = allowance(holder, spender);

      f(e, args);
      mathint allowanceAfter = allowance(holder, spender);

      assert allowanceAfter != allowanceBefore => (
          f.selector == sig:approve(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector
      );
}

既然我们已经编写了验证哪些方法可以修改状态的规则，我们就可以编写验证哪些调用者被允许减少持有者余额的规则。

只有持有者和 spender 可以减少持有者的余额

另一个未经授权的操作是，当调用者不是持有者或经批准的 spender 时，减少余额。以下规则验证了此属性：

Copyrule onlyHolderAndSpenderCanReduceHolderBalance(env e, method f, calldataarg args) filtered {
    // 排除 `burn()`，因为权限检查留给集成者/开发者
    f -> f.selector != sig:burn(address,uint256).selector
} {
    requireInvariant totalSupplyEqualsSumOfBalances();

    address account;

    mathint spenderAllowanceBefore = allowance(account, e.msg.sender);
    mathint holderBalanceBefore = balanceOf(account);

    f(e, args);
    mathint holderBalanceAfter = balanceOf(account);

    assert (holderBalanceAfter < holderBalanceBefore) => (
        e.msg.sender == account ||
        holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
    );
}

以下行表示我们在参数化调用中排除了 burn() 函数：

Copyf -> f.selector != sig:burn(address,uint256).selector

burn() 被过滤掉是因为，如前所述，它故意没有权限检查。将其包含在规则中会导致其失败，因为任何调用者都可以减少持有者的余额，这将违背规则的意图。

我们已经在不变量部分介绍了 requireInvariant，并且我们从早期部分熟悉了在方法调用前后记录状态，因此我们可以直接跳到断言。

下面的断言意味着如果持有者的余额减少，它必须是由于以下两个原因之一：

• $e.msg.sender = account$

  持有者发起了此操作，或者

• $holderBalanceBefore - holderBalanceAfter \le to\_mathint(spenderAllowanceBefore)$

  减少量在经批准的 allowance 限制内，这也意味着调用者是经批准的 spender 且 allowance 非零。

Copyassert (holderBalanceAfter < holderBalanceBefore) => (
    e.msg.sender == account ||
    holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
);

这条特定规则是 OpenZeppelin 的 onlyAuthorizedCanTransfer 的修改版本。区别在于，原始规则中 sig:burn(address,uint256).selector 在断言中，而在此规则 onlyHolderAndSpenderCanReduceHolderBalance 中我们将其 filtered 掉。

这是本节中所有规则的 Prover 运行。

ERC-20 的完整 CVL 规范

这是完整的 CVL 规范和 Prover 运行。

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

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