使用幽灵变量和Hook验证不变性

RareSkills
发布于 2026-02-14 13:32
阅读 17

本文介绍了如何使用Certora工具通过幽灵变量（ghost variables）和Hook（hooks）对ERC20代币合约进行形式化验证，确保“总供应量等于所有账户余额之和”这一核心不变性。文章详细阐述了在Sstore和SloadHook中放置约束条件的不同影响，并强调了SloadHook在排除不可能状态方面的优越性。

Certora 形式化验证

## 使用 Ghost 和 Hook 验证不变量

[模块 2：不变量、存储 Hook、Ghost 和形式化验证代币不变量、存储 Hook、Ghost 和形式化验证代币](https://rareskills.io/tutorials/certora-book)

上次更新时间：2026 年 2 月 13 日

在任何正确的 ERC20 实现中，**所有账户余额的总和必须始终等于代币总供应量**。此属性应在任何状态变更过程中始终保持为真。如果某个调用（无论是直接调用还是一系列调用的一部分）违反了此不变量，则表明合约的逻辑和设计存在根本性缺陷。

在本章中，我们将利用之前章节中学到的关于 ghost 变量和 hook 的知识，来形式化验证这个关键不变量。

## 添加智能合约进行验证

在本教程中，我们将使用来自 **Solmate 库**的 ERC20 合约，该库由 **Transmission11** 开发。要将此合约包含在你的项目中，请在 Certora 项目目录的 `contracts` 子目录中创建一个名为 `ERC20.sol` 的新文件。然后，将 **Solmate 的 ERC20 实现**的代码复制并粘贴到该文件中。

```solidity
// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity 0.8.25;

/// @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 的情况下，请勿手动设置余额，因为所有用户余额的总和不得超过它。
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;

/*//////////////////////////////////////////////////////////////
                            EIP-2612 STORAGE
    //////////////////////////////////////////////////////////////*/

uint256 internal immutable INITIAL_CHAIN_ID;

bytes32 internal immutable INITIAL_DOMAIN_SEPARATOR;

mapping(address => uint256) public nonces;

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

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

INITIAL_CHAIN_ID = block.chainid;
        INITIAL_DOMAIN_SEPARATOR = computeDomainSeparator();
    }

/*//////////////////////////////////////////////////////////////
                               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;

// Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        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]; // Saves gas for limited approvals.

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

balanceOf[from] -= amount;

// Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

emit Transfer(from, to, amount);

return true;
    }

/*//////////////////////////////////////////////////////////////
                             EIP-2612 LOGIC
    //////////////////////////////////////////////////////////////*/

function permit(
        address owner,
        address spender,
        uint256 value,
        uint256 deadline,
        uint8 v,
        bytes32 r,
        bytes32 s
    ) public virtual {
        require(deadline >= block.timestamp, "PERMIT_DEADLINE_EXPIRED");

// Unchecked because the only math done is incrementing
        // the owner's nonce which cannot realistically overflow.
        unchecked {
            address recoveredAddress = ecrecover(
                keccak256(
                    abi.encodePacked(
                        "\x19\x01",
                        DOMAIN_SEPARATOR(),
                        keccak256(
                            abi.encode(
                                keccak256(
                                    "Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"
                                ),
                                owner,
                                spender,
                                value,
                                nonces[owner]++,
                                deadline
                            )
                        )
                    )
                ),
                v,
                r,
                s
            );

require(recoveredAddress != address(0) && recoveredAddress == owner, "INVALID_SIGNER");

allowance[recoveredAddress][spender] = value;
        }

emit Approval(owner, spender, value);
    }

function DOMAIN_SEPARATOR() public view virtual returns (bytes32) {
        return block.chainid == INITIAL_CHAIN_ID ? INITIAL_DOMAIN_SEPARATOR : computeDomainSeparator();
    }

function computeDomainSeparator() internal view virtual returns (bytes32) {
        return
            keccak256(
                abi.encode(
                    keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"),
                    keccak256(bytes(name)),
                    keccak256("1"),
                    block.chainid,
                    address(this)
                )
            );
    }

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

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

// Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

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

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

// Cannot underflow because a user's balance
        // will never be larger than the total supply.
        unchecked {
            totalSupply -= amount;
        }

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

## 理解挑战

要将我们的不变量表达为 CVL 表达式，我们需要**两个**值：

1.  **代币总供应量**
2.  **所有账户余额的总和**

我们的合约有一个名为 `totalSupply` 的公共状态变量，它跟踪任何状态下的代币总供应量，并且可以使用 `totalSupply()` getter 函数读取其值。**然而，核心挑战是合约没有提供任何内置方法来获取所有余额的总和。**

## “解决方案”

为了获取所有账户余额的总和，我们将创建一个名为 `sumOfBalances` 的 ghost 变量，其初始值将使用 `init_state` axiom 设置为 0。ghost `sumOfBalances` 将通过一个 store hook 在每次对 `balanceOf` mapping 进行写入操作时更新。

我们知道，store hook 可以让我们访问正在更新的余额的旧值和新值。我们使用这些值来计算变更并相应地更新我们的 ghost：

```solidity
sumOfBalances = sumOfBalances - oldValue + newValue;
```

例如，如果用户的余额从 100 增加到 150，我们的 hook 会从 `sumOfBalances` 中减去 100 并加上 150，从而正确地将总额增加 50。通过对每次余额更新应用此增量计算，我们的 ghost `sumOfBalances` 将跟踪合约状态的变化，反映所有余额的总和。

一旦 Prover 可以访问这两个值（合约中的实际 `totalSupply` 和我们精确维护的 `sumOfBalances` ghost），我们就可以使用 CVL 中的 invariant 块正式声明不变量，以断言总供应量始终等于所有账户余额的总和。

## 逐步编写完整规范

现在，让我们将所有讨论付诸实践，编写一个完整的规范来验证所有余额的总和是否与代币总供应量匹配，具体步骤如下：

1.  在你的 Certora 项目目录中，导航到 `specs` 子目录并创建一个名为 `erc20.spec` 的新文件。
2.  在 `erc20.spec` 中，定义一个名为 `sumOfBalances` 的 ghost 变量。

```solidity
ghost mathint sumOfBalances;
```

3.  接下来，我们使用 `init_state` axiom 将 `sumOfBalances` 的初始值在不变量基本情况中设置为 `0`。

```solidity
ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}
```

此 axiom 仅在不变量基本情况下约束 ghost 变量，建立一致的构造函数后状态。没有这个基线，Prover 可能会为 ghost 假设任意初始值，使得不变量的保持变得毫无意义。

4.  定义一个 store hook，它跟踪对 `balanceOf` mapping 的更改并相应地更新我们的 ghost 变量 `sumOfBalances`。

```solidity
ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
```

5.  现在我们有了这两个值——合约的 `totalSupply()` 和我们的 ghost `sumOfBalances`——我们可以定义核心不变量，如下所示：

```solidity
ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;
```

6.  最后，添加一个 methods 块，其中将包含 `totalSupply()` 的函数签名。

```solidity
methods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;
```

7.  导航到 `confs` 子目录并创建一个名为 `erc20.conf` 的新文件。

```solidity
{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "msg": "Testing erc20 functionality"
}
```

## 运行验证

完成以上所有步骤后，通过在终端中运行 `certoraRun confs/erc20.conf` 命令提交代码进行验证。

在你选择的任何 Web 浏览器中打开 Prover 提供的**验证结果**，以查看与下图类似的结果：

![image](https://img.learnblockchain.cn/2026/02/28/aa3ad2a3657723f1-image1.png)

在我们的验证结果中，我们可以看到不变量检查在两个地方都失败了：在构造函数调用之后和方法执行期间。

![image](https://img.learnblockchain.cn/2026/02/28/9302b29201f0f634-image2.png)

当我们点击“**归纳基础：构造函数之后**”违规时，Prover 建议在你的配置中添加 `optimistic_loop` 键并将其值设置为 `true`，或者将 `loop_iter` 增加到大于 1 的值。

![image](https://img.learnblockchain.cn/2026/02/28/3e26fc8b7761eb25-image3.png)

现在，让我们按照 Prover 的建议，将 `optimistic_loop` 键设置为 `true` 来更新配置文件。我们将在后续名为“**字符串如何导致循环？**”的章节中更深入地探讨这个问题。

```solidity
{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}
```

完成后，通过在终端中运行 `certoraRun confs/erc20.conf` 命令重新运行 Prover。在我们的新验证结果中，我们可以看到我们的不变量在构造函数执行期间成功通过，但**在方法执行期间失败**，特别是对于 `transfer()` 和 `transferFrom()` 函数。

![image](https://img.learnblockchain.cn/2026/02/28/b41fc0a562ec3574-image4.png)

要了解违规的原因，请单击 `transfer()` 或 `transferFrom()` 函数的调用跟踪。在我们的示例中，我们将分析 `transfer()` 函数的调用跟踪。

![image](https://img.learnblockchain.cn/2026/02/28/9609da3125aba0dd-image5.png)

要查看完整的调用跟踪，请单击“**调用跟踪**”面板右上角的“**展开**”按钮。

![image](https://img.learnblockchain.cn/2026/02/28/cf7dcb5e26000817-image6.png)

在调用跟踪中，我们可以看到单独账户 `0x7` 和 `0x8200` 的初始余额分别设置为 `2^256 − 4` 和 `0xf000000000000000000000000000000000000000000000000000000000000000`。以十进制形式，它们分别对应于 **`115792089237316195423570985008687907853269984665640564039457584007913129639932`** 和 **`108890810646419256008710686707116392212123736112785533035372916772359555072000`**。

![image](https://img.learnblockchain.cn/2026/02/28/75c41d6d1278a9fc-image7.png)

这两个值都是 Prover 通过 **havocing** 分配的，并且落在 0 到 `2^{256} - 1` 的数值范围内。然而，在任何**正确**实现的 ERC20 合约中，单个账户余额绝不应超过所有余额的总和。在这种情况下，两个账户的起始余额都远大于总供应量（`0xa`）和 `sumOfBalances`，这创建了一个不可能在实际部署中存在的初始状态。

Prover 之所以这样做，是因为它本质上不理解 ERC20 代币的业务逻辑；它只是将存储视为原始数据。除非明确约束，否则它假定任何 `uint256` 值都是一个有效的起点。

为了避免这种情况，我们特别需要告诉 Prover，初始的单个账户余额不应大于 `sumOfBalances`。为此，我们将使用 CVL 提供的 `require` 语句来约束 Prover 应考虑的值。

## 使用 `require` 语句约束初始余额

在我们的 `erc20.spec` 文件中，将下面所示的代码添加到我们的 store hook 中，以限制可以分配给任何账户余额的值的范围。完成后，重新运行 Prover 以查看验证结果。

```solidity
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    require oldAmount <= sumOfBalances;  //添加此行
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
```

在**新结果**中，你会注意到 **Prover 不再发现任何违规**。

![image](https://img.learnblockchain.cn/2026/02/28/1098a5e88b55e77f-image8.png)

我们的不变量 `totalSupplyEqSumOfBalances` 通过了验证，因为在 store hook 中添加了 `require oldAmount <= sumOfBalances;` 这行代码后，Prover 将只探索此条件为真的执行路径。这有效地排除了依赖于单个余额高于总和（**例如，`transfer` 中发送者或接收者的余额**）的反例，确保 Prover 专注于**单个余额保持在总供应量逻辑范围内**的场景。因此，验证成功，确认不变量在所有允许的转换下都得到保留。

## 另一种方法：Load Hook

虽然向 `Sstore` hook 添加约束有效，但还有另一种方法，我们可以在 **Load Hook** 中添加单个余额的约束。

要实现此方法，请按照以下步骤操作：

1.  在 `balanceOf` mapping 上**定义一个 load hook**，它会拦截对 `balanceOf` 的每次读取。

```solidity
hook Sload uint256 balance balanceOf[KEY address addr] {}
```

2.  使用 `require sumOfBalances >= to_mathint(balance);` 在此 hook 中**引入一个约束**。

```solidity
hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}
```

3.  **从 `Sstore` hook 中移除约束**，这样我们就完全依赖 load hook 逻辑。

```solidity
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    require oldAmount <= sumOfBalances;  //移除此行
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
```

以下是更新后的规范在进行上述更改后应有的样子：

```solidity
methods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    // 通过 axiom 约束构造函数前的 ghost 值
    init_state axiom sumOfBalances == 0;

}

// 在 balanceOf mapping 上添加了一个 load hook
hook Sload uint256 balance balanceOf[KEY address addr] {
    // 引入一个约束
    require sumOfBalances >= to_mathint(balance);

}

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    // 增量更新
    sumOfBalances = sumOfBalances - oldAmount + newAmount;

}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;
```

如果你使用此更改（从 `Sstore` hook 中移除 `require` 并在 `Sload` hook 中保留它）重新运行验证，不变量 `totalSupplyEqSumOfBalances` 仍将通过。

![image](https://img.learnblockchain.cn/2026/02/28/503556e4dcf0a3cf-image9.png)

这之所以有效，是因为 load hook 明确排除了**任何单个账户余额大于所有余额总和的状态**。如果 Prover 试图使用这种不可能的初始状态来构建反例，它最终会在评估合约逻辑时**读取**该余额。一旦发生此读取，load hook 中的 `require` 语句会检查该余额是否与我们的 ghost 变量一致。由于余额不切实际地大，条件失败，Prover 被迫丢弃整个执行路径。

## Sstore 与 Sload：在哪里放置约束？

这两个版本都“有效”，因为它们排除了会违反我们不变量的不可能状态，但 load hook 方法提供了更可靠和全面的保护。让我们深入探讨原因：

### Store Hook 实际保证了什么

当我们将约束放入 store hook 时：

```solidity
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
    require oldAmount <= sumOfBalances;
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
```

在上面的代码中，我们实际上是在告诉 Prover：“**无论何时你向 `balanceOf[account]` 写入，请确保**之前的**值（`oldAmount`）不大于 `sumOfBalances`。”

这造成了一个**盲点**：

1.  如果 Prover **从不写入**某个 `balanceOf[addr]` slot，那么此 hook **从不为该地址触发**。
2.  这意味着 Prover 仍然可以从一个奇怪的初始值（通过 havoc）开始，例如 `balanceOf[addr] = 2^{256} - 1`，即使 `sumOfBalances = 10`。
3.  只要合约不尝试写入该 slot，`Sstore` 中的 `require` 就永远不会被检查，并且在读取和逻辑推理期间，不可能的状态被允许持续存在。

简而言之，store hook 只说：“**如果你通过写入接触到这个 slot，那么之前的值必须是合理的。**”它**没有**说：“**无论何时你查看所有余额，它们始终是合理的。**”

### Load Hook 保证了什么

现在，看看 load hook 版本：

```solidity
hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}
```

这会在 Prover **每次**从 `balanceOf` 读取余额时运行。在这里，我们告诉 Prover：“**无论何时你读取余额，该余额必须小于或等于 `sumOfBalances`。**”

这有两个重要的影响：

1.  **Prover 不能在任何计算中使用不可能的余额。**如果它试图假设 `balanceOf[addr]` 大于 `sumOfBalances`，然后读取它，load hook 中的 `require` 就会失败，并且该执行路径会立即被丢弃。
2.  **即使从未写入该 slot，这也适用。**Prover 可能会在开始时将 `balanceOf[addr]` 通过 havoc 设置为某个任意值，但一旦它**读取**该值，load hook 就会检查它。如果该值不可能，那么整个路径就会被抛弃。

load hook 就像一个**全局健全性检查**：“你查看的任何余额都必须与 ghost `sumOfBalances` 保持一致。”

这就是为什么，当我们关心 `sumOfBalances` 与真实余额对齐并避免不可能的 ERC20 状态时，load hook 方法通常是更好的选择。

## 结论

在本章中，我们验证了基本的 ERC20 不变量：**总供应量 = 所有余额的总和**。

我们通过使用一个 **ghost 变量**来跟踪总和，并使用 **hook** 将该 ghost 与合约的存储同步来实现这一点。至关重要的是，我们展示了为什么将约束放在 `Sload` hook 中通常比放在 `Sstore` hook 中更安全。通过在值**读取**时对其进行监管，我们有效地关闭了 Prover 可能假设不可能初始状态的“盲点”。

这些技术允许你在底层存储之上证明高层业务规则，确保你的验证只关注有效、真实的合约行为。

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

>- 原文链接： [rareskills.io/post/certo...](https://rareskills.io/post/certora-verifying-invariant-using-ghost-hook)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

Certora 形式化验证

使用 Ghost 和 Hook 验证不变量

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

上次更新时间：2026 年 2 月 13 日

在任何正确的 ERC20 实现中，所有账户余额的总和必须始终等于代币总供应量。此属性应在任何状态变更过程中始终保持为真。如果某个调用（无论是直接调用还是一系列调用的一部分）违反了此不变量，则表明合约的逻辑和设计存在根本性缺陷。

在本章中，我们将利用之前章节中学到的关于 ghost 变量和 hook 的知识，来形式化验证这个关键不变量。

添加智能合约进行验证

在本教程中，我们将使用来自 Solmate 库的 ERC20 合约，该库由 Transmission11 开发。要将此合约包含在你的项目中，请在 Certora 项目目录的 contracts 子目录中创建一个名为 ERC20.sol 的新文件。然后，将 Solmate 的 ERC20 实现的代码复制并粘贴到该文件中。

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity 0.8.25;

/// @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 的情况下，请勿手动设置余额，因为所有用户余额的总和不得超过它。
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;

    /*//////////////////////////////////////////////////////////////
                            EIP-2612 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 internal immutable INITIAL_CHAIN_ID;

    bytes32 internal immutable INITIAL_DOMAIN_SEPARATOR;

    mapping(address => uint256) public nonces;

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

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

        INITIAL_CHAIN_ID = block.chainid;
        INITIAL_DOMAIN_SEPARATOR = computeDomainSeparator();
    }

    /*//////////////////////////////////////////////////////////////
                               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;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        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]; // Saves gas for limited approvals.

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

        balanceOf[from] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(from, to, amount);

        return true;
    }

    /*//////////////////////////////////////////////////////////////
                             EIP-2612 LOGIC
    //////////////////////////////////////////////////////////////*/

    function permit(
        address owner,
        address spender,
        uint256 value,
        uint256 deadline,
        uint8 v,
        bytes32 r,
        bytes32 s
    ) public virtual {
        require(deadline >= block.timestamp, "PERMIT_DEADLINE_EXPIRED");

        // Unchecked because the only math done is incrementing
        // the owner's nonce which cannot realistically overflow.
        unchecked {
            address recoveredAddress = ecrecover(
                keccak256(
                    abi.encodePacked(
                        "\x19\x01",
                        DOMAIN_SEPARATOR(),
                        keccak256(
                            abi.encode(
                                keccak256(
                                    "Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"
                                ),
                                owner,
                                spender,
                                value,
                                nonces[owner]++,
                                deadline
                            )
                        )
                    )
                ),
                v,
                r,
                s
            );

            require(recoveredAddress != address(0) && recoveredAddress == owner, "INVALID_SIGNER");

            allowance[recoveredAddress][spender] = value;
        }

        emit Approval(owner, spender, value);
    }

    function DOMAIN_SEPARATOR() public view virtual returns (bytes32) {
        return block.chainid == INITIAL_CHAIN_ID ? INITIAL_DOMAIN_SEPARATOR : computeDomainSeparator();
    }

    function computeDomainSeparator() internal view virtual returns (bytes32) {
        return
            keccak256(
                abi.encode(
                    keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"),
                    keccak256(bytes(name)),
                    keccak256("1"),
                    block.chainid,
                    address(this)
                )
            );
    }

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

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

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

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

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

        // Cannot underflow because a user's balance
        // will never be larger than the total supply.
        unchecked {
            totalSupply -= amount;
        }

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

理解挑战

要将我们的不变量表达为 CVL 表达式，我们需要两个值：

代币总供应量
所有账户余额的总和

我们的合约有一个名为 totalSupply 的公共状态变量，它跟踪任何状态下的代币总供应量，并且可以使用 totalSupply() getter 函数读取其值。然而，核心挑战是合约没有提供任何内置方法来获取所有余额的总和。

“解决方案”

为了获取所有账户余额的总和，我们将创建一个名为 sumOfBalances 的 ghost 变量，其初始值将使用 init_state axiom 设置为 0。ghost sumOfBalances 将通过一个 store hook 在每次对 balanceOf mapping 进行写入操作时更新。

我们知道，store hook 可以让我们访问正在更新的余额的旧值和新值。我们使用这些值来计算变更并相应地更新我们的 ghost：

sumOfBalances = sumOfBalances - oldValue + newValue;

例如，如果用户的余额从 100 增加到 150，我们的 hook 会从 sumOfBalances 中减去 100 并加上 150，从而正确地将总额增加 50。通过对每次余额更新应用此增量计算，我们的 ghost sumOfBalances 将跟踪合约状态的变化，反映所有余额的总和。

一旦 Prover 可以访问这两个值（合约中的实际 totalSupply 和我们精确维护的 sumOfBalances ghost），我们就可以使用 CVL 中的 invariant 块正式声明不变量，以断言总供应量始终等于所有账户余额的总和。

逐步编写完整规范

现在，让我们将所有讨论付诸实践，编写一个完整的规范来验证所有余额的总和是否与代币总供应量匹配，具体步骤如下：

在你的 Certora 项目目录中，导航到 specs 子目录并创建一个名为 erc20.spec 的新文件。
在 erc20.spec 中，定义一个名为 sumOfBalances 的 ghost 变量。

ghost mathint sumOfBalances;

接下来，我们使用 init_state axiom 将 sumOfBalances 的初始值在不变量基本情况中设置为 0。

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

定义一个 store hook，它跟踪对 balanceOf mapping 的更改并相应地更新我们的 ghost 变量 sumOfBalances。

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

现在我们有了这两个值——合约的 totalSupply() 和我们的 ghost sumOfBalances——我们可以定义核心不变量，如下所示：

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

最后，添加一个 methods 块，其中将包含 totalSupply() 的函数签名。

methods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

导航到 confs 子目录并创建一个名为 erc20.conf 的新文件。

{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "msg": "Testing erc20 functionality"
}

运行验证

完成以上所有步骤后，通过在终端中运行 certoraRun confs/erc20.conf 命令提交代码进行验证。

在你选择的任何 Web 浏览器中打开 Prover 提供的验证结果，以查看与下图类似的结果：

在我们的验证结果中，我们可以看到不变量检查在两个地方都失败了：在构造函数调用之后和方法执行期间。

当我们点击“归纳基础：构造函数之后”违规时，Prover 建议在你的配置中添加 optimistic_loop 键并将其值设置为 true，或者将 loop_iter 增加到大于 1 的值。

现在，让我们按照 Prover 的建议，将 optimistic_loop 键设置为 true 来更新配置文件。我们将在后续名为“字符串如何导致循环？”的章节中更深入地探讨这个问题。

{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}

完成后，通过在终端中运行 certoraRun confs/erc20.conf 命令重新运行 Prover。在我们的新验证结果中，我们可以看到我们的不变量在构造函数执行期间成功通过，但在方法执行期间失败，特别是对于 transfer() 和 transferFrom() 函数。

要了解违规的原因，请单击 transfer() 或 transferFrom() 函数的调用跟踪。在我们的示例中，我们将分析 transfer() 函数的调用跟踪。

要查看完整的调用跟踪，请单击“调用跟踪”面板右上角的“展开”按钮。

在调用跟踪中，我们可以看到单独账户 0x7 和 0x8200 的初始余额分别设置为 2^256 − 4 和 0xf000000000000000000000000000000000000000000000000000000000000000。以十进制形式，它们分别对应于 115792089237316195423570985008687907853269984665640564039457584007913129639932 和 108890810646419256008710686707116392212123736112785533035372916772359555072000。

这两个值都是 Prover 通过 havocing 分配的，并且落在 0 到 2^{256} - 1 的数值范围内。然而，在任何正确实现的 ERC20 合约中，单个账户余额绝不应超过所有余额的总和。在这种情况下，两个账户的起始余额都远大于总供应量（0xa）和 sumOfBalances，这创建了一个不可能在实际部署中存在的初始状态。

Prover 之所以这样做，是因为它本质上不理解 ERC20 代币的业务逻辑；它只是将存储视为原始数据。除非明确约束，否则它假定任何 uint256 值都是一个有效的起点。

为了避免这种情况，我们特别需要告诉 Prover，初始的单个账户余额不应大于 sumOfBalances。为此，我们将使用 CVL 提供的 require 语句来约束 Prover 应考虑的值。

使用 `require` 语句约束初始余额

在我们的 erc20.spec 文件中，将下面所示的代码添加到我们的 store hook 中，以限制可以分配给任何账户余额的值的范围。完成后，重新运行 Prover 以查看验证结果。

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    require oldAmount &lt;= sumOfBalances;  //添加此行
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

在新结果中，你会注意到 Prover 不再发现任何违规。

我们的不变量 totalSupplyEqSumOfBalances 通过了验证，因为在 store hook 中添加了 require oldAmount <= sumOfBalances; 这行代码后，Prover 将只探索此条件为真的执行路径。这有效地排除了依赖于单个余额高于总和（例如，transfer 中发送者或接收者的余额）的反例，确保 Prover 专注于单个余额保持在总供应量逻辑范围内的场景。因此，验证成功，确认不变量在所有允许的转换下都得到保留。

另一种方法：Load Hook

虽然向 Sstore hook 添加约束有效，但还有另一种方法，我们可以在 Load Hook 中添加单个余额的约束。

要实现此方法，请按照以下步骤操作：

在 balanceOf mapping 上定义一个 load hook，它会拦截对 balanceOf 的每次读取。

hook Sload uint256 balance balanceOf[KEY address addr] {}

使用 require sumOfBalances >= to_mathint(balance); 在此 hook 中引入一个约束。

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

从 Sstore hook 中移除约束，这样我们就完全依赖 load hook 逻辑。

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    require oldAmount &lt;= sumOfBalances;  //移除此行
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

以下是更新后的规范在进行上述更改后应有的样子：

methods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    // 通过 axiom 约束构造函数前的 ghost 值
    init_state axiom sumOfBalances == 0;

}

// 在 balanceOf mapping 上添加了一个 load hook
hook Sload uint256 balance balanceOf[KEY address addr] {
    // 引入一个约束
    require sumOfBalances >= to_mathint(balance);

}

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    // 增量更新
    sumOfBalances = sumOfBalances - oldAmount + newAmount;

}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

如果你使用此更改（从 Sstore hook 中移除 require 并在 Sload hook 中保留它）重新运行验证，不变量 totalSupplyEqSumOfBalances 仍将通过。

这之所以有效，是因为 load hook 明确排除了任何单个账户余额大于所有余额总和的状态。如果 Prover 试图使用这种不可能的初始状态来构建反例，它最终会在评估合约逻辑时读取该余额。一旦发生此读取，load hook 中的 require 语句会检查该余额是否与我们的 ghost 变量一致。由于余额不切实际地大，条件失败，Prover 被迫丢弃整个执行路径。

Sstore 与 Sload：在哪里放置约束？

这两个版本都“有效”，因为它们排除了会违反我们不变量的不可能状态，但 load hook 方法提供了更可靠和全面的保护。让我们深入探讨原因：

Store Hook 实际保证了什么

当我们将约束放入 store hook 时：

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
    require oldAmount &lt;= sumOfBalances;
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

在上面的代码中，我们实际上是在告诉 Prover：“无论何时你向 balanceOf[account] 写入，请确保之前的**值（oldAmount）不大于 sumOfBalances。”

这造成了一个盲点：

如果 Prover 从不写入某个 balanceOf[addr] slot，那么此 hook 从不为该地址触发。
这意味着 Prover 仍然可以从一个奇怪的初始值（通过 havoc）开始，例如 balanceOf[addr] = 2^{256} - 1，即使 sumOfBalances = 10。
只要合约不尝试写入该 slot，Sstore 中的 require 就永远不会被检查，并且在读取和逻辑推理期间，不可能的状态被允许持续存在。

简而言之，store hook 只说：“如果你通过写入接触到这个 slot，那么之前的值必须是合理的。”它没有说：“无论何时你查看所有余额，它们始终是合理的。”

Load Hook 保证了什么

现在，看看 load hook 版本：

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

这会在 Prover 每次从 balanceOf 读取余额时运行。在这里，我们告诉 Prover：“无论何时你读取余额，该余额必须小于或等于 sumOfBalances。”

这有两个重要的影响：

Prover 不能在任何计算中使用不可能的余额。如果它试图假设 balanceOf[addr] 大于 sumOfBalances，然后读取它，load hook 中的 require 就会失败，并且该执行路径会立即被丢弃。
即使从未写入该 slot，这也适用。Prover 可能会在开始时将 balanceOf[addr] 通过 havoc 设置为某个任意值，但一旦它读取该值，load hook 就会检查它。如果该值不可能，那么整个路径就会被抛弃。

load hook 就像一个全局健全性检查：“你查看的任何余额都必须与 ghost sumOfBalances 保持一致。”

这就是为什么，当我们关心 sumOfBalances 与真实余额对齐并避免不可能的 ERC20 状态时，load hook 方法通常是更好的选择。

结论

在本章中，我们验证了基本的 ERC20 不变量：总供应量 = 所有余额的总和。

我们通过使用一个 ghost 变量来跟踪总和，并使用 hook 将该 ghost 与合约的存储同步来实现这一点。至关重要的是，我们展示了为什么将约束放在 Sload hook 中通常比放在 Sstore hook 中更安全。通过在值读取时对其进行监管，我们有效地关闭了 Prover 可能假设不可能初始状态的“盲点”。

这些技术允许你在底层存储之上证明高层业务规则，确保你的验证只关注有效、真实的合约行为。

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

原文链接： rareskills.io/post/certo...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

使用幽灵变量和Hook验证不变性

使用 Ghost 和 Hook 验证不变量

添加智能合约进行验证

理解挑战

“解决方案”

逐步编写完整规范

运行验证

使用 `require` 语句约束初始余额

另一种方法：Load Hook

Sstore 与 Sload：在哪里放置约束？

Store Hook 实际保证了什么

Load Hook 保证了什么

结论

0 条评论

文章目录

使用幽灵变量和Hook验证不变性

使用 Ghost 和 Hook 验证不变量

添加智能合约进行验证

理解挑战

“解决方案”

逐步编写完整规范

运行验证

使用 require 语句约束初始余额

另一种方法：Load Hook

Sstore 与 Sload：在哪里放置约束？

Store Hook 实际保证了什么

Load Hook 保证了什么

结论

0 条评论

文章目录

使用 `require` 语句约束初始余额