持久化幽灵变量

Certora 形式化验证

持久型幽灵变量 (Persistent Ghosts)

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

上次更新于 2026 年 2 月 13 日

介绍

在前面的章节中，我们使用幽灵变量（通过 Sstore Hook）来记录智能合约中未明确跟踪的存储值和数量——例如，所有余额的总和。它们允许在验证期间观察和推断状态变化或状态变量之间的关系。

然而，在调用合约方法后执行规则期间，幽灵变量可能会出现以下情况：

• 当 Prover 遇到未解析的外部调用时被 havoc’ed，或
• 当调用回滚时，回滚到其先前的状态（重置）。

幽灵变量在未解析的外部调用期间被 havoc’ed，因为 Prover 无法看到被调用合约的实现。由于外部合约可能会回调到调用者并修改存储，Prover 无法排除幽灵变量可能通过其Hook更新的情况。为了处理这种不确定性，Prover 会为幽灵变量分配非确定性值。

当调用回滚时，幽灵变量不会变得非确定性。相反，它们会回滚（重置）到调用开始前它们所持有的值。根据 Certora 的 文档，“幽灵变量可以被视为所验证合约状态的扩展。这意味着如果一个调用回滚，幽灵变量的值将回滚到其前置状态。”

这些是幽灵变量的默认行为：它们在未解析的调用中被 havoc’ed，并在方法调用回滚时重置。然而，有一种特殊类型的幽灵变量称为 持久型幽灵变量 (persistent ghost)，它在未解析的外部调用和回滚中都保持其值（不会被 havoc）。

在本章中，我们将演示持久型幽灵变量如何工作，它们与常规幽灵变量有何不同，何时使用它们，以及何时不使用它们。

声明持久型幽灵变量

持久型幽灵变量使用 persistent 关键字声明，如下所示：

Copypersistent ghost bool g_flag;
persistent ghost uint256 g_count;

为了可读性，在本文中我们对所有幽灵变量使用 g_ 前缀，尽管它们可以自由命名。

要使用特定值初始化持久型幽灵变量，请在幽灵变量声明中添加 init_state axiom：

Copypersistent ghost bool g_flag {
    init_state axiom g_flag == false;
}

persistent ghost uint256 g_count {
    init_state axiom g_count == 0;
}

注意：虽然持久型幽灵变量在未解析的方法调用期间不会被 havoc’ed，但它们在规则的预调用状态和不变量的基例中会被 havoc’ed；常规幽灵变量也是如此。因此，它们仍然必须在规则中作为前置条件（通过 require 语句）进行适当约束，并使用 init_state axiom 对不变量的基例进行初始化。

持久型幽灵变量与常规幽灵变量的行为

下图显示了持久型幽灵变量如何在回滚调用和未解析的外部调用中保留其值。在规则执行期间，当Hook为 ghostVar 赋值时，该值永远不会被回滚（重置）或 havoc’ed，因此其最终状态始终反映Hook分配的最后一个值：

与持久型幽灵变量相反，常规幽灵变量在未解析的外部调用时被 havoc’ed，并在回滚时重置：

注意：持久型幽灵变量和常规幽灵变量都只在单次规则执行中保持其值，而不会在规则之间传递。区别在于持久型幽灵变量在该执行中可以存活未解析或回滚的调用，而常规幽灵变量则不能。

使用持久型幽灵变量跟踪回滚

本节演示了持久型幽灵变量如何以常规幽灵变量无法做到的方式实现回滚跟踪。它解释了为什么常规幽灵变量在这种用例中会失败，并展示了持久型幽灵变量如何解决这个问题。

当方法调用回滚时，常规幽灵变量会重置

当方法回滚时，常规幽灵变量的状态也会回滚。这种行为与存储变量在失败调用期间回滚到其先前值的方式一致。

为了说明这种行为，考虑以下合约 SimpleVault，用户可以在其中存入和取出 ETH：

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

contract SimpleVault {
    mapping(address => uint256) public balanceOf;

    /// deposit ETH into the vault
    function deposit() external payable {
        balanceOf[msg.sender] += msg.value;
    }

    /// withdraw ETH from the vault
    function withdraw(uint256 amount) external {
        require(balanceOf[msg.sender] >= amount, "Insufficient balance");
        balanceOf[msg.sender] -= amount;

        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "ETH transfer failed");
    }
}

目标是验证 withdraw() 在以下情况下会精确回滚：

• 提款金额超过存入余额 (amount > balanceBefore)
• 向此不可支付函数发送了非零 msg.value (e.msg.value != 0)
• ETH 转移失败，或低级调用返回 false

本节专门关注第三种情况：跟踪 ETH 转移失败。

以下规则实现了“账户余额”章节中的断言模式。它使用双条件运算符 (<=>) 并以析取方式 (||) 列出所有预期的回滚条件。这解释了所有可能的方法回滚，当且仅当其中一个条件发生时：

Copyghost bool g_lowLevelCallSuccess; // regular ghost

rule withdraw_revert(env e) {
    uint256 amount;

    require g_lowLevelCallSuccess; // by requiring it to be true initially, you can detect when it becomes false during execution

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

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

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

为了跟踪 ETH 转移结果，我们使用 CALL Hook；这是一个 CVL 功能，用于监视低级 EVM CALL 指令并捕获其返回码。我们将此返回码分配给 g_lowLevelCallSuccess（0 表示失败，1 表示成功）：

Copyhook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

这是完整的规范：

Copymethods {
    function balanceOf(address) external returns uint256 envfree;
}

ghost bool g_lowLevelCallSuccess;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

rule withdraw_revert(env e) {
    uint256 amount;
    require g_lowLevelCallSuccess;

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

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

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

使用常规幽灵变量，验证失败：

查看失败的 Prover 运行：链接

让我们检查一下失败的原因。

常规幽灵变量值重置 — 调用跟踪

验证失败是因为 g_lowLevelCallSuccess 是一个在回滚时重置的常规幽灵变量。CALL Hook捕获了失败 (returnCode == 0)，但当 withdraw 回滚时，幽灵变量重置并丢失了此值。

如下图所示，在调用 withdraw() 方法之前（预调用状态），g_lowLevelCallSuccess 为 true：

当低级 ETH 转移调用失败时，CALL Hook捕获失败的调用（返回值为 0），这将 g_lowLevelCallSuccess 设置为 false：

当 CALL 操作码（由 CVL CALL Hook捕获）返回零时，表示 ETH 转移失败。在规则内部，当 withdraw@withrevert(e, amount) 调用回滚时，幽灵变量会重置为其预调用状态。下图显示幽灵变量在转移失败的情况下回到了 true：

使用持久型幽灵变量修复规范

回顾我们在常规幽灵变量的调用跟踪中观察到的情况，执行过程如下：

1. 幽灵变量 g_lowLevelCallSuccess 被初始化为 true（通过 require 语句）。
2. withdraw 函数执行并触发一个失败的低级 CALL。
3. CALL Hook检测到失败 (returnCode == 0) 并将 g_lowLevelCallSuccess 设置为 false。
4. withdraw 函数回滚，因为 require(success) 在 success 为 false 时失败。
5. 回滚导致幽灵变量重置为其预调用状态 true。

根本问题很明显：步骤 5 中的回滚将幽灵变量重置为 true，抹去了步骤 3 中记录转移失败的 false 值。

为了解决这个问题，将幽灵变量声明为 persistent，以便 CALL Hook分配的布尔值可以在回滚中存活并可在规则中访问：

Copymethods {
    function balanceOf(address) external returns uint256 envfree;
}

persistent ghost bool g_lowLevelCallSuccess;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

rule withdraw_revert(env e) {
    uint256 amount;
    require g_lowLevelCallSuccess;

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

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

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

正如预期，规则验证通过：

Prover 运行：链接

有了持久型幽灵变量，我们成功地跟踪了回滚期间低级调用 ETH 转移失败，这是常规幽灵变量无法做到的。这个例子展示了持久型幽灵变量的一个恰当用例：捕获在回滚中会丢失的状态信息。

何时不使用持久型幽灵变量

了解持久型幽灵变量的正确用例后，同样重要的是要了解何时不应使用它们。

轻松地为常规幽灵变量添加 persistent 关键字使其容易被滥用。只有当你需要观察回滚或未解析的执行中发生的情况时，才应有意使用持久型幽灵变量——而不是将其作为规则或不变量无法验证时的权宜之计。

为了演示滥用的问题，让我们考虑一个接受 ERC-20 代币而不是 ETH 的类似金库。它的余额映射是私有的，因此需要一个幽灵变量来镜像内部余额，因为没有 getter 函数可以读取：

Copy/// minimal ERC20 interface
interface IERC20 {
    function transfer(address to, uint256 amount) external returns (bool);
    ...
}

contract SimpleVault20 {
    IERC20 public immutable token;
    mapping(address => uint256) private balanceOf;

    constructor(address _token) {
        token = IERC20(_token);
    }

    function deposit(uint256 amount) external {
        require(amount > 0, "Zero deposit");

        balanceOf[msg.sender] += amount;
        require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
    }

    ...
}

我们来编写 deposit() 函数的规范。对于幽灵变量和Hook：

• 将幽灵变量声明为常规幽灵变量
• 实现 Sstore Hook以跟踪每个账户存款人余额的变化
• 实现 Sload Hook以同步存储和幽灵变量的读取

Copyghost mapping(address => mathint) g_balanceOf;

hook Sstore balanceOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_balanceOf[account] = g_balanceOf[account] + newVal - oldVal;
}

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

至于规则，我们验证存入的金额 (depositAmount) 是否正确地记入了发送者在金库中的余额：

Copyrule deposit(env e) {
    uint256 depositAmount;

    require currentContract != e.msg.sender;
    require g_balanceOf[e.msg.sender] == 0;

    deposit(e, depositAmount);
    assert g_balanceOf[e.msg.sender] == depositAmount;
}

我们运行验证。由于 deposit 函数调用了一个未知的 ERC-20 实现（这将导致 havoc），我们预计它会失败：

Prover 运行：链接

为什么验证失败

根本原因在于 SimpleVault20 合约的以下一行，它调用了一个未知的 ERC-20 实现：

Copycontract SimpleVault20 {
    ...
    function deposit(uint256 amount) external {
        require(amount > 0, "Zero deposit");

        balanceOf[msg.sender] += amount;

        // `token` is an unknown ERC-20 implementation
        require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
    }
    ...
}

在下图中，我们看到 Prover 将值 0xa（或 10）分配给 depositAmount，然后通过 Sstore Hook传递给幽灵映射变量 g_balanceOf[address]：

然后，在调用外部合约期间，幽灵变量被 havoc’ed，因为它的实现是未知的：

看到 havoc 错误后，人们可能会试图添加 persistent 关键字来抑制它。虽然这会使验证通过，但它隐藏了真正的问题：我们不知道外部 ERC-20 合约是如何实现的：

Prover 运行：链接

Prover 在错误假设下验证

Prover 显示规则已验证，但这基于一个错误的假设。通过使用 持久型 幽灵变量，规范假设 ERC-20 实现永远不会回滚或修改调用合约的存储。因此，它将金额 0xa（或 10）记入 msg.sender，即使转移实际上可能失败：

这说明了为什么在这种情况下使用 持久型 幽灵变量具有误导性：它绕过了外部合约行为的不确定性，掩盖了潜在的错误而不是揭示它们。

实际代币实现应与金库关联

正确的解决方案不是使用持久型幽灵变量。相反，我们必须将一个已知的 ERC-20 实现“链接”到 场景 中——无论是协议自己的 ERC20、WETH、DAI，还是任何代码可用的 ERC-20 代币。

链接指令 Prover 使用验证场景中包含的实际合约实现进行外部调用，而不是将这些调用视为 havoc 行为。

对于 SimpleVault20，代币地址是不可变的，这意味着要使用的 ERC-20 在部署时是已知的，并且在合约的整个生命周期中都不会改变。因此，我们可以通过将 ERC-20 合约添加到场景并在规范中配置它来使用 link 将其“绑定”到 ERC-20 实现。这允许 Prover 针对实际的代币实现验证 SimpleVault20 合约。否则，如果没有链接，Prover 将无法准确验证金库与代币的交互，从而导致如上所示的假阳性。

有关 link 的更多详细信息，请参阅 Certora 文档：1，2

总结

• 持久型幽灵变量在 havoc 和回滚中存活，而常规幽灵变量在对未知合约的外部调用期间被 havoc’ed，并在回滚期间重置。
• 对未知合约的外部调用导致 havoc，因为 Prover 无法看到被调用方的实现，因此它会模拟所有可能的返回值和存储效果。
• 持久型幽灵变量的一个恰当用例是捕获来自 CVL Hook（例如 CALL 返回码）的信息，这些信息必须在失败的执行路径中存活，例如跟踪失败的低级 ETH 转移。
• 将 persistent 关键字作为快速修复方案来通过失败的规则，会通过忽略未知合约实现或未解析调用的影响，从而产生虚假的验证成功感。

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

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