存储Hook和幽灵变量介绍

RareSkills
发布于 2026-02-14 19:31
阅读 18

本文深入探讨了如何使用Certora的存储Hook（Storage Hooks）和幽灵变量（Ghost Variables）进行智能合约的形式化验证。文章通过具体案例，详细阐述了如何观察合约内部私有状态的变化，并克服了规则无法直接访问Hook局部变量的限制，最终实现了对合约关键属性的精确验证。

Certora 形式化验证

## 存储 Hooks 和 Ghosts 介绍

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

上次更新于 2026 年 2 月 13 日

通常需要检查特定存储位置的变化，以证明属性或不变量成立，特别是当存储无法从外部访问，或者感兴趣的值未被合约明确计算或暴露时。

例如，假设我们希望验证，在一个 ERC-20 实现中，`totalSupply` 的值**总是等于所有个人账户余额的总和**。乍一看，这似乎很简单：我们可以 `assert totalSupply() == sumOfBalances()`。

然而，困难在于合约实际上从不维护这个累计和；它只在映射中存储每个账户的余额。与 `totalSupply` 不同，`totalSupply` 被明确存储并可以直接查询，而“**余额总和**”在合约状态中并不存在。相反，这些信息分布在多个存储槽中，因此在不观察这些槽如何被访问和更新的情况下，不可能验证这种关系。当其中一些变量是 private 时，挑战变得更大。

为了应对这一挑战，CVL 提供了 hooks 和 ghost 变量。Hooks 允许我们观察低级事件，例如对存储的读取和写入，而 ghost 变量允许我们**捕获、聚合和共享**这些观察结果，以便它们可以在规范的其他地方被引用。它们共同弥合了内部合约行为与高级验证规则之间的鸿沟，使我们能够推理依赖于隐藏或隐式状态变化的属性。

在本章中，你将学习 hooks 的工作原理、可用的不同类型以及与它们相关的限制。我们还将向你介绍 ghost 变量，这是一个核心 CVL 功能，它使 hooks 和规则之间能够通信，从而使你能够验证那些隐藏在合约内部存储中的丰富正确性属性。

## 理解“需求”

为了更好地理解我们正在讨论的问题，请考虑下面的智能合约，它维护一个私有的 `count` 和一个在部署时设置的 `owner`。`increment()` 和 `resetCounter()` 都受 `onlyOwner` 修改器保护：`increment()` 将私有 `count` 增加 1，`resetCounter()` 将其重置为零，并且只有存储在合约中的 `owner` 地址才能调用这两个函数。

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

contract Counter {

// State variables
    address private owner;
    uint256 private count;

/// @notice Initializes the contract and sets the deployer as the owner
    constructor() {
        owner = msg.sender;
    }

/// @notice Restricts function calls to the contract owner only
    modifier onlyOwner() {
        require(msg.sender == owner, "Counter: caller is not the owner");
        _;
    }

// External functions

/// @notice Increments the counter by 1
    /// @dev Only callable by the owner
    function increment() external onlyOwner {
        count++;
    }

/// @notice Resets the counter to 0
    /// @dev Only callable by the owner
    function resetCounter() external onlyOwner {
        count = 0;
    }
}
```

现在假设我们想形式化验证以下属性：

1. `owner` 一旦在构造函数中设置，就绝不能改变。
2. 调用 `increment()` 应该使 `count` 恰好增加 1。

乍一看，这两个属性都显得很直接。然而，以 CVL 规则的形式表达它们带来了一些挑战。将第一个属性表达为 CVL 规则的问题在于 `owner` 变量被标记为 `private`，并且合约没有提供 getter 来暴露其值。如果无法从规则中访问它，我们就无法断言它在构造函数中设置后保持不变。

第二个属性引入了不同的挑战。尽管我们可以在规则内部调用 `increment()`，但变量 `count` 是 **private** 的，并且合约没有提供 getter 来读取其值。这意味着规则无法直接看到函数运行时 `count` 发生了什么。

由于规则只能观察函数的输入和输出，而不是内部存储的变化，因此它们无法捕获 `count` 更新时的旧值和新值。没有这种可见性，Prover 无法确认每次调用 `increment()` 实际上都将计数器增加了 1。

简而言之，问题不在于属性难以表述，而在于它们依赖于**低级存储行为**，并且需要直接观察执行期间存储如何更新。标准 CVL 规则仅限于通过其公共接口与合约交互，因此它们无法捕获这些内部变化。为了验证诸如 owner 的不变性或计数器的精确增量等属性，我们需要工具，使我们能够窥视合约内部，监控其存储操作，并将这些观察结果纳入我们的规范中。

这就是 **hooks** 发挥作用的地方。

## Hooks 是什么？

在 CVL 中，hooks 是代码块，当智能合约执行低级 EVM 操作时，例如从存储读取或写入、执行操作码或修改瞬态数据时，它们会在验证过程中自动运行。

一个 hook 使用 `hook` 关键字定义，每个 CVL hook 都指定了以下内容：

1. 它监听的**操作**（例如，SLOAD、SSTORE 或特定的 EVM 操作码）。
2. 当检测到该操作时执行的**CVL 代码块**，提供对该事件相关数据的访问。

## Hooks 的类型

CVL 提供了 3 种不同类型的 hooks，按它们监控的操作类型进行分类。这 3 种类型是：

1. **存储 Hooks**
2. **操作码 Hooks**
3. **瞬态存储 Hooks**

本章中，我们将重点关注**存储 Hooks**，因为它们应用最广泛，并且构成了理解 CVL 中 hooks 工作原理的基础。其他类型的 hooks 在特定上下文中同样有用，我们将在后续章节中介绍它们。

## 什么是存储 Hooks？

**存储 hooks** 是 CVL 中一种特定类型的 hook，当合约的存储变量被访问时，无论是读取还是写入，它们都会被触发。换句话说，当 EVM 对受监控的存储槽执行读取 (SLOAD) 或写入 (SSTORE) 操作时，它们会被激活，从而允许我们：

- 捕获正在读取或写入的值。
- 在变量被访问或修改时强制执行条件。
- 跟踪合约状态在不同执行中如何演变。

CVL 中主要有两种存储 hooks：

1. **Load Hooks**
2. **Store Hooks**

### 1. Load Hooks

**Load hook** 在受监控的存储变量上发生读取操作 (`SLOAD`) 时触发，并允许你捕获正在读取的值。

它使用 `hook Sload` 关键字定义，后跟 CVL 变量的类型和名称（用于保存加载的值），最后是被监控的合约存储变量的名称。

```solidity
Copyhook Sload address contractOwner owner { ... }
```

上面的 hook 将在验证中的合约访问其类型为 `address` 的 `owner` 存储变量进行读取操作时执行。该值随后将存储在 CVL 变量 `contractOwner` 中。

### 2. Store Hooks

**Store hooks** 在任何特定存储变量上发生任何写入操作之前执行。

Store hooks 也使用 `hook` 关键字定义，后跟 `Sstore` 关键字。之后，你指定被监控的合约存储变量的名称，以及 CVL 变量的类型和名称，该变量将保存即将写入该存储位置的值。

```solidity
Copyhook Sstore owner address newOwner{...}
```

可选地，该模式还可以包括一个变量的类型和名称，用于存储正在被覆盖的先前值。

```solidity
Copyhook Sstore owner address newOwner (address oldOwner) {...}
```

在我们应用 hooks 来验证 `Counter` 合约的属性之前，有一个重要的限制需要理解：**在 hooks 内部声明的变量是 hook 块的局部变量，并且不能被规则直接看到**。

## 理解 Hooks 的局限性

一个 hook 不仅允许我们监控特定的存储变量，还通过将其存储在 CVL 变量中以供使用来提供对其值的访问。**然而，一个限制是，在 hooks 内部定义的 CVL 变量的作用域仅限于该 hook，这意味着它们不能直接从规则中访问**。

为了理解这个限制，请考虑下面的规范，它旨在证明 `Counter` 合约的 `owner` 在构造函数中首次设置后永远不会改变：

```solidity
Copyhook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

address prevOwner = contractOwner;

//parametric call
     method f;
     calldataarg args;
     f(e,args);

address currentOwner = contractOwner;

assert prevOwner == currentOwner;

}
```

在上面的规范中，`Sload` hook 使私有 `owner` 变量在每次读取时都可观察，并将其值存储到 `contractOwner` 中。在规则中，规范将此观察到的值保存为 `prevOwner`，对具有任意输入的任何合约函数执行符号调用，然后再次将 owner 观察为 `currentOwner`。最后，它断言 `prevOwner == currentOwner`，这意味着在所有可能的调用中，owner 必须保持一致。

然而，当你运行 Certora Prover 时，你将遇到以下错误：

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

上面的错误简单地强调了规则 `checkOwnerConsistency()` 无法访问和使用在我们的 load hook 内部声明的 `contractOwner`。

这可能会引出一个问题：**如果 hooks 旨在捕获和存储数据，为什么我们不能直接在规则中使用这些数据呢？**

**答案在于 hooks 中定义的变量的作用域**。

### Hooks 的作用域限制

当你在 hook 内部定义变量时，其作用域**仅限于该 hook**。这就像在函数内部定义变量一样——它可以在该块内部使用，但在外部不可见。这就是为什么 `contractOwner` 在 hook 内部完全有效，但对于规则 `checkOwnerConsistency()` 来说却是完全未知的。

这意味着 **CVL 规则和 hooks 不共享变量**——它们在单独的作用域中操作。

那么我们如何使用从 hook 中提取的信息来编写有用的规则呢？

答案是 **ghost 变量**。

### 使用 Ghost 变量规避作用域限制

尽管我们无法直接在规则中访问 hook 变量，但我们可以定义特殊的变量，称为 **ghost 变量**（或简称 **ghosts**），以在 hooks 和规则之间传递信息。

ghost 使用 `ghost` 关键字声明，后跟其类型和名称，如下所示。

```solidity
Copyghost bool hasVoted;
ghost uint x;
ghost mathint numVoted;
ghost mapping(address => mathint) balances;
```

ghost 变量可以是任何 CVL 支持的类型或映射。在映射的情况下，其键必须是 CVL 支持的类型，其值可以是 CVL 类型或其他映射。

## 验证 `Counter` 合约中的 Owner 一致性

为了使 `checkOwnerConsistency()` 规则按预期工作，需要在规则的作用域中提供在 hook 内部观察到的值。我们可以通过将观察到的值存储在 ghost 变量中来实现这一点。实现此目的的步骤概述如下：

**1. 声明一个 ghost 来保存观察到的 `owner` 值：** 在我们的规范的顶层，引入一个名为 `ghostOwner` 的 ghost 变量。每当读取合约的 `owner` 槽时，这个 ghost 将作为该值的容器。

```solidity
/// Top-level ghost variable to mirror the contract's `owner` slot
ghost address ghostOwner;

hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

address prevOwner = contractOwner;

//parametric call
     method f;
     calldataarg args;
     f(e,args);

address currentOwner = contractOwner;

assert prevOwner == currentOwner;

}
```

声明 ghost 变量时，务必在它们前面加上 `ghost` 或 `ghost_`（例如，`ghostOwner`，`ghost_owner`），以明确将它们与 Solidity 存储变量和 hook 局部 CVL 变量区分开来。

在此阶段，ghost 变量 `ghostOwner` 已经声明但尚未与合约的存储同步。

**2. 在 hook 内部同步 ghost：** 接下来，修改 `Sload` hook，以便每当合约对 `owner` 存储槽执行读取操作时，hook 都会捕获该值并**将其写入 ghost**。

```solidity
Copyghost address ghostOwner;

hook Sload address contractOwner owner {
    //assign captured value to ghost
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

address prevOwner = contractOwner;

//parametric call
     method f;
     calldataarg args;
     f(e,args);

address currentOwner = contractOwner;

assert prevOwner == currentOwner;

}
```

这在合约的私有存储与 hook 之间，以及 hook 与超出 hook 局部作用域的 ghost 变量之间建立了一座桥梁。每当合约读取 `owner` 时，`ghostOwner` 就会与该存储值同步。

**3. 在规则内部使用 ghost：** 最后，更新 `checkOwnerConsistency()` 规则，使其引用 ghost `ghostOwner`，而不是使用 hook 局部的 `contractOwner`。

```solidity
Copyghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

//Take a snapshot of the ghost before the call
    address prevOwner = ghostOwner;

//parametric call
    method f;
    calldataarg args;
    f(e,args);

//Take another snapshot after the call
    address currentOwner = ghostOwner;

assert prevOwner == currentOwner;
}
```

按照上面提供的说明更新规范后，请使用 `certoraRun` 命令**重新运行 Certora Prover**。这次 Prover 将编译我们的规则而不会出现任何错误，并将在你的终端中打印验证结果。结果将类似于下图：

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

看到上面的结果后，你可能会感到惊讶，并想知道为什么我们的规则仍然失败，即使 `Counter` 合约从未明确更新其 owner。原因不在于 Solidity 代码，而在于 **Prover 如何解释 ghosts 以及 hooks 在验证运行期间如何执行**。

## 将 Ghosts 与存储同步

Ghost 变量不会自动与合约的存储绑定。在执行开始时，Prover 会为它们分配**任意值** (havoced values)——除非它们在规范中明确初始化，否则可以在不同跟踪中更改的任意占位符。在我们的例子中，ghost `ghostOwner` 仅在读取 `owner` 槽时（通过 Sload）更新。如果在规则比较 `prevOwner` 和 `currentOwner` 之前没有发生读取，则 ghost 保持未初始化状态，持有一个与实际存储无关的任意值。

这正是实际发生的情况：`owner` 的存储槽持有一个地址（例如，`0x2712` 或 `0x2711`），但 ghost `ghostOwner` 包含一个完全不同的值（例如，`0x401`）。

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

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

由于 ghost 从未与存储对齐，我们的规则最终比较了两个无意义的值，Prover 正确地报告了失败。

我们可以看到，主要问题是 ghost 变量不会自动镜像合约存储。为了解决这个问题，我们需要确保 ghost 在规则中使用**之前**通过 hook 明确更新。实际上，这意味着强制合约执行相关存储槽的读取，以便 `Sload` hook 可以触发并使 ghost 与存储中的实际值同步。

为了实现这一点，我们只需进行一次初始调用，导致合约读取 `owner` 槽，这反过来会触发 Sload hook 并更新我们的 ghost。在我们的例子中，我们将在规则开始时调用 `resetCounter(e)`。由于 `resetCounter(e)` 受 `onlyOwner` 修改器保护，EVM 必须读取 owner 存储槽以检查修改器的条件。此读取会自动触发 hook，确保 `ghostOwner` 在我们将其捕获到 `prevOwner` 中之前更新。

下面是**更新后的规范**，显示了完整的修改规则：

```solidity
Copyghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

// Updated rule: now includes an initial sync call
rule checkOwnerConsistency(env e) {

// NEW: Force an SLOAD of `owner` so the hook fires and syncs `ghostOwner`
    resetCounter(e);

/// Take the first snapshot after synchronization
    address prevOwner = ghostOwner;

//parametric call
    method f;
    calldataarg args;
    f(e, args);

// Take another snapshot after the call
    address currentOwner = ghostOwner;

// The owner must not change across any call
    assert prevOwner == currentOwner;
}
```

规则内部的**第一行** (`resetCounter(e);`) 是关键的补充。

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

现在 ghost 已正确同步，`prevOwner` 和 `currentOwner` 之间的比较变得有意义，从而允许 Prover 正确验证 `owner` 变量的一致性。

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

让我们逐步分解这里**发生**了什么：

1. **初始同步调用 (`resetCounter(e)`)**
   - 规则通过调用 `resetCounter(e)` 开始。
   - 为了检查 `onlyOwner` 修改器，合约**必须读取** `owner` 槽 (SLOAD)。
   - 该读取**触发了 `Sload` hook**，它将观察到的值写入 ghost `ghostOwner`。
   - 因此，在我们进行任何快照之前，`ghostOwner` 现在已与实际存储值同步。
2. **第一次快照 (`prevOwner`)**
   - 同步后，规则立即执行 `address prevOwner = ghostOwner;`。
   - 由于步骤 1，`prevOwner` 是合约中存储的**真实 owner**。
3. **任意调用 (`method f; calldataarg args; f(e, args);`)**
   - Prover 现在探索一个**带有符号输入的任意外部调用**。
   - 在此合约中，这意味着 `increment(...)` 或 `resetCounter(...)` 带有任意参数。
   - 这两个函数都受 `onlyOwner` 保护，并且**不写入** owner。
   - 在此调用期间，任何对 `owner` 的额外读取（因为 `onlyOwner`）都将**重新触发 `Sload` hook**，但它只会将**相同的值**写入 ghost。
4. **第二次快照 (`currentOwner`)**
   - 任意调用返回后，规则执行 `address currentOwner = ghostOwner;`。
   - 由于合约在部署后从未修改 `owner`，并且 hook 仅镜像读取，因此 `currentOwner` 等于先前捕获的相同存储支持的值。
5. **断言**
   - 规则检查 `assert prevOwner == currentOwner;`。
   - 由于合约在部署后从未修改 `owner`，因此没有代码路径可以使这两个快照不同。
   - 因此，在所有探索的执行中，`prevOwner` 和 `currentOwner` 始终保持相等。
   - 结果，Prover 未发现反例并报告规则**已验证**。

在 owner 属性验证后，现在让我们转向我们之前确定的第二个属性。

## 验证 `Counter` 合约中的 `Increment()` 调用

我们要证明的第二个属性是，**对 `increment()` 的调用应该使 `count` 恰好增加 1**。由于 `count` 是私有的，规则本身无法观察到 `count++` 执行的实际存储写入。为了证明此属性，我们将一个 **store hook** 附加到 `count` 槽，捕获写入前后的值，将它们持久化到 ghosts 中，最后在规则中断言算术关系。

以下是完整的规范：

```solidity
Copymethods {
    function increment() external;
}

ghost mathint ghost_prevCount;

ghost mathint ghost_currentCount;

hook Sstore count uint256 postcallValue (uint256 precallValue) {
    ghost_prevCount = precallValue;
    ghost_currentCount = postcallValue;
}

rule checkCounter() {

env e;

//call to increment
    increment(e);

assert ghost_currentCount == ghost_prevCount + 1;
}
```

在上面的规范中，每当调用 `increment()` 函数时，hook 都会观察对 `count` 存储槽的更新。旧值 (`precallValue`) 存储在一个 ghost 变量 (`ghost_prevCount`) 中，而新值 (`postcallValue`) 存储在另一个 (`ghost_currentCount`) 中。这允许规则检查在调用 `increment()` 函数后，计数器是否恰好增加了 1，正如预期的那样。

当我们在上面的规范上运行 Prover 时，我们将看到规则已通过验证，如下图所示：

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

让我们逐步分解这里发生的一切：

1. **调用之前**：合约的私有变量 `count` 有一些初始值（假设为 X）。
2. **`increment()` 调用期间**：

- EVM 执行 `count++` 语句，这会转换为对 `count` 存储槽的读取和随后的写入。
   - 就在写入发生之前，`Sstore` hook 被触发。
   - hook 捕获即将被覆盖的值 (`precallValue`) 和正在写入的新值 (`postcallValue`)。
   - 这些值存储在 ghost 变量 `ghost_prevCount` 和 `ghost_currentCount` 中。
3. **规则检查**：

- 函数调用完成后，规则断言 `ghost_currentCount == ghost_prevCount + 1`。
   - 鉴于 `ghost_currentCount = X + 1` 且 `ghost_prevCount = X`，断言成立。

因此，我们从 Prover 获得了验证结果。换句话说，任何对 `increment()` 的调用都会使计数器恰好增加 1，并且 Prover 能够形式化验证此属性而没有找到任何反例。

## **Ghost 变量作为存储的扩展**

我们可以看到，hooks 用于通过检测合约存储上的特定读取或写入操作来观察和收集数据。然而，由于在 hooks 内部声明的变量是 hooks 的局部变量，一旦 hook 执行完成，它们的值就会消失。为了在整个规范中保留和重用这些信息，CVL 引入了 **ghost 变量**——持久的、规范级别的存储，它镜像或扩展了合约的实际状态。因此，ghost 变量可以被视为合约存储的扩展。

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

**事实上，Certora Prover 对 ghost 变量的处理与常规存储非常相似：**

- 任何对 ghost 的更新都会在正在进行的事务稍后回滚时自动回滚，就像存储一样。
- 在验证运行开始时，ghosts（**与其他 CVL 变量一样**）代表任意（_havoced_）值，除非它们在规范中明确设置，这反映了 Prover 对存储的符号视图。

我们将在后面的章节中更详细地探讨这些行为，届时我们还将学习如何显式初始化 ghost 变量，以避免意外的任意化，并确保更可预测的验证结果。

## 结论

Certora hooks 提供了对存储和 EVM 操作的强大可观察性。然而，它们的变量仅限于每个 hook 的局部作用域。Ghost 变量通过从 hooks 捕获数据并使其可供规则访问来解决这个问题，从而能够有效而全面地推理合约在验证期间的内部状态。

_本文是关于 [使用 Certora Prover 进行形式化验证](https://rareskills.io/tutorials/certora-book) 系列文章的一部分_

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

Certora 形式化验证

存储 Hooks 和 Ghosts 介绍

模块 2：不变量、存储 Hooks、Ghosts 和代币的形式化验证不变量、存储 Hooks、Ghosts 和代币的形式化验证

上次更新于 2026 年 2 月 13 日

通常需要检查特定存储位置的变化，以证明属性或不变量成立，特别是当存储无法从外部访问，或者感兴趣的值未被合约明确计算或暴露时。

例如，假设我们希望验证，在一个 ERC-20 实现中，totalSupply 的值总是等于所有个人账户余额的总和。乍一看，这似乎很简单：我们可以 assert totalSupply() == sumOfBalances()。

然而，困难在于合约实际上从不维护这个累计和；它只在映射中存储每个账户的余额。与 totalSupply 不同，totalSupply 被明确存储并可以直接查询，而“余额总和”在合约状态中并不存在。相反，这些信息分布在多个存储槽中，因此在不观察这些槽如何被访问和更新的情况下，不可能验证这种关系。当其中一些变量是 private 时，挑战变得更大。

为了应对这一挑战，CVL 提供了 hooks 和 ghost 变量。Hooks 允许我们观察低级事件，例如对存储的读取和写入，而 ghost 变量允许我们捕获、聚合和共享这些观察结果，以便它们可以在规范的其他地方被引用。它们共同弥合了内部合约行为与高级验证规则之间的鸿沟，使我们能够推理依赖于隐藏或隐式状态变化的属性。

理解“需求”

为了更好地理解我们正在讨论的问题，请考虑下面的智能合约，它维护一个私有的 count 和一个在部署时设置的 owner。increment() 和 resetCounter() 都受 onlyOwner 修改器保护：increment() 将私有 count 增加 1，resetCounter() 将其重置为零，并且只有存储在合约中的 owner 地址才能调用这两个函数。

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

contract Counter {

    // State variables
    address private owner;
    uint256 private count;

    /// @notice Initializes the contract and sets the deployer as the owner
    constructor() {
        owner = msg.sender;
    }

    /// @notice Restricts function calls to the contract owner only
    modifier onlyOwner() {
        require(msg.sender == owner, "Counter: caller is not the owner");
        _;
    }

    // External functions

    /// @notice Increments the counter by 1
    /// @dev Only callable by the owner
    function increment() external onlyOwner {
        count++;
    }

    /// @notice Resets the counter to 0
    /// @dev Only callable by the owner
    function resetCounter() external onlyOwner {
        count = 0;
    }
}

现在假设我们想形式化验证以下属性：

owner 一旦在构造函数中设置，就绝不能改变。
调用 increment() 应该使 count 恰好增加 1。

乍一看，这两个属性都显得很直接。然而，以 CVL 规则的形式表达它们带来了一些挑战。将第一个属性表达为 CVL 规则的问题在于 owner 变量被标记为 private，并且合约没有提供 getter 来暴露其值。如果无法从规则中访问它，我们就无法断言它在构造函数中设置后保持不变。

第二个属性引入了不同的挑战。尽管我们可以在规则内部调用 increment()，但变量 count 是 private 的，并且合约没有提供 getter 来读取其值。这意味着规则无法直接看到函数运行时 count 发生了什么。

由于规则只能观察函数的输入和输出，而不是内部存储的变化，因此它们无法捕获 count 更新时的旧值和新值。没有这种可见性，Prover 无法确认每次调用 increment() 实际上都将计数器增加了 1。

简而言之，问题不在于属性难以表述，而在于它们依赖于低级存储行为，并且需要直接观察执行期间存储如何更新。标准 CVL 规则仅限于通过其公共接口与合约交互，因此它们无法捕获这些内部变化。为了验证诸如 owner 的不变性或计数器的精确增量等属性，我们需要工具，使我们能够窥视合约内部，监控其存储操作，并将这些观察结果纳入我们的规范中。

这就是 hooks 发挥作用的地方。

Hooks 是什么？

在 CVL 中，hooks 是代码块，当智能合约执行低级 EVM 操作时，例如从存储读取或写入、执行操作码或修改瞬态数据时，它们会在验证过程中自动运行。

一个 hook 使用 hook 关键字定义，每个 CVL hook 都指定了以下内容：

它监听的操作（例如，SLOAD、SSTORE 或特定的 EVM 操作码）。
当检测到该操作时执行的CVL 代码块，提供对该事件相关数据的访问。

Hooks 的类型

CVL 提供了 3 种不同类型的 hooks，按它们监控的操作类型进行分类。这 3 种类型是：

存储 Hooks
操作码 Hooks
瞬态存储 Hooks

本章中，我们将重点关注存储 Hooks，因为它们应用最广泛，并且构成了理解 CVL 中 hooks 工作原理的基础。其他类型的 hooks 在特定上下文中同样有用，我们将在后续章节中介绍它们。

什么是存储 Hooks？

存储 hooks 是 CVL 中一种特定类型的 hook，当合约的存储变量被访问时，无论是读取还是写入，它们都会被触发。换句话说，当 EVM 对受监控的存储槽执行读取 (SLOAD) 或写入 (SSTORE) 操作时，它们会被激活，从而允许我们：

捕获正在读取或写入的值。
在变量被访问或修改时强制执行条件。
跟踪合约状态在不同执行中如何演变。

CVL 中主要有两种存储 hooks：

Load Hooks
Store Hooks

1. Load Hooks

Load hook 在受监控的存储变量上发生读取操作 (SLOAD) 时触发，并允许你捕获正在读取的值。

它使用 hook Sload 关键字定义，后跟 CVL 变量的类型和名称（用于保存加载的值），最后是被监控的合约存储变量的名称。

Copyhook Sload address contractOwner owner { ... }

上面的 hook 将在验证中的合约访问其类型为 address 的 owner 存储变量进行读取操作时执行。该值随后将存储在 CVL 变量 contractOwner 中。

2. Store Hooks

Store hooks 在任何特定存储变量上发生任何写入操作之前执行。

Store hooks 也使用 hook 关键字定义，后跟 Sstore 关键字。之后，你指定被监控的合约存储变量的名称，以及 CVL 变量的类型和名称，该变量将保存即将写入该存储位置的值。

Copyhook Sstore owner address newOwner{...}

可选地，该模式还可以包括一个变量的类型和名称，用于存储正在被覆盖的先前值。

Copyhook Sstore owner address newOwner (address oldOwner) {...}

在我们应用 hooks 来验证 Counter 合约的属性之前，有一个重要的限制需要理解：在 hooks 内部声明的变量是 hook 块的局部变量，并且不能被规则直接看到。

理解 Hooks 的局限性

一个 hook 不仅允许我们监控特定的存储变量，还通过将其存储在 CVL 变量中以供使用来提供对其值的访问。然而，一个限制是，在 hooks 内部定义的 CVL 变量的作用域仅限于该 hook，这意味着它们不能直接从规则中访问。

为了理解这个限制，请考虑下面的规范，它旨在证明 Counter 合约的 owner 在构造函数中首次设置后永远不会改变：

Copyhook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;

}

在上面的规范中，Sload hook 使私有 owner 变量在每次读取时都可观察，并将其值存储到 contractOwner 中。在规则中，规范将此观察到的值保存为 prevOwner，对具有任意输入的任何合约函数执行符号调用，然后再次将 owner 观察为 currentOwner。最后，它断言 prevOwner == currentOwner，这意味着在所有可能的调用中，owner 必须保持一致。

然而，当你运行 Certora Prover 时，你将遇到以下错误：

上面的错误简单地强调了规则 checkOwnerConsistency() 无法访问和使用在我们的 load hook 内部声明的 contractOwner。

这可能会引出一个问题：如果 hooks 旨在捕获和存储数据，为什么我们不能直接在规则中使用这些数据呢？

答案在于 hooks 中定义的变量的作用域。

Hooks 的作用域限制

当你在 hook 内部定义变量时，其作用域仅限于该 hook。这就像在函数内部定义变量一样——它可以在该块内部使用，但在外部不可见。这就是为什么 contractOwner 在 hook 内部完全有效，但对于规则 checkOwnerConsistency() 来说却是完全未知的。

这意味着 CVL 规则和 hooks 不共享变量——它们在单独的作用域中操作。

那么我们如何使用从 hook 中提取的信息来编写有用的规则呢？

答案是 ghost 变量。

使用 Ghost 变量规避作用域限制

尽管我们无法直接在规则中访问 hook 变量，但我们可以定义特殊的变量，称为 ghost 变量（或简称 ghosts），以在 hooks 和规则之间传递信息。

ghost 使用 ghost 关键字声明，后跟其类型和名称，如下所示。

Copyghost bool hasVoted;
ghost uint x;
ghost mathint numVoted;
ghost mapping(address => mathint) balances;

ghost 变量可以是任何 CVL 支持的类型或映射。在映射的情况下，其键必须是 CVL 支持的类型，其值可以是 CVL 类型或其他映射。

验证 `Counter` 合约中的 Owner 一致性

为了使 checkOwnerConsistency() 规则按预期工作，需要在规则的作用域中提供在 hook 内部观察到的值。我们可以通过将观察到的值存储在 ghost 变量中来实现这一点。实现此目的的步骤概述如下：

1. 声明一个 ghost 来保存观察到的 owner 值： 在我们的规范的顶层，引入一个名为 ghostOwner 的 ghost 变量。每当读取合约的 owner 槽时，这个 ghost 将作为该值的容器。

/// Top-level ghost variable to mirror the contract's `owner` slot
ghost address ghostOwner;

hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;

}

声明 ghost 变量时，务必在它们前面加上 ghost 或 ghost_（例如，ghostOwner，ghost_owner），以明确将它们与 Solidity 存储变量和 hook 局部 CVL 变量区分开来。

在此阶段，ghost 变量 ghostOwner 已经声明但尚未与合约的存储同步。

2. 在 hook 内部同步 ghost： 接下来，修改 Sload hook，以便每当合约对 owner 存储槽执行读取操作时，hook 都会捕获该值并将其写入 ghost。

Copyghost address ghostOwner;

hook Sload address contractOwner owner {
    //assign captured value to ghost
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;

}

这在合约的私有存储与 hook 之间，以及 hook 与超出 hook 局部作用域的 ghost 变量之间建立了一座桥梁。每当合约读取 owner 时，ghostOwner 就会与该存储值同步。

3. 在规则内部使用 ghost： 最后，更新 checkOwnerConsistency() 规则，使其引用 ghost ghostOwner，而不是使用 hook 局部的 contractOwner。

Copyghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

    //Take a snapshot of the ghost before the call
    address prevOwner = ghostOwner;

    //parametric call
    method f;
    calldataarg args;
    f(e,args);

    //Take another snapshot after the call
    address currentOwner = ghostOwner;

    assert prevOwner == currentOwner;
}

按照上面提供的说明更新规范后，请使用 certoraRun 命令重新运行 Certora Prover。这次 Prover 将编译我们的规则而不会出现任何错误，并将在你的终端中打印验证结果。结果将类似于下图：

看到上面的结果后，你可能会感到惊讶，并想知道为什么我们的规则仍然失败，即使 Counter 合约从未明确更新其 owner。原因不在于 Solidity 代码，而在于 Prover 如何解释 ghosts 以及 hooks 在验证运行期间如何执行。

将 Ghosts 与存储同步

Ghost 变量不会自动与合约的存储绑定。在执行开始时，Prover 会为它们分配任意值 (havoced values)——除非它们在规范中明确初始化，否则可以在不同跟踪中更改的任意占位符。在我们的例子中，ghost ghostOwner 仅在读取 owner 槽时（通过 Sload）更新。如果在规则比较 prevOwner 和 currentOwner 之前没有发生读取，则 ghost 保持未初始化状态，持有一个与实际存储无关的任意值。

这正是实际发生的情况：owner 的存储槽持有一个地址（例如，0x2712 或 0x2711），但 ghost ghostOwner 包含一个完全不同的值（例如，0x401）。

由于 ghost 从未与存储对齐，我们的规则最终比较了两个无意义的值，Prover 正确地报告了失败。

我们可以看到，主要问题是 ghost 变量不会自动镜像合约存储。为了解决这个问题，我们需要确保 ghost 在规则中使用之前通过 hook 明确更新。实际上，这意味着强制合约执行相关存储槽的读取，以便 Sload hook 可以触发并使 ghost 与存储中的实际值同步。

为了实现这一点，我们只需进行一次初始调用，导致合约读取 owner 槽，这反过来会触发 Sload hook 并更新我们的 ghost。在我们的例子中，我们将在规则开始时调用 resetCounter(e)。由于 resetCounter(e) 受 onlyOwner 修改器保护，EVM 必须读取 owner 存储槽以检查修改器的条件。此读取会自动触发 hook，确保 ghostOwner 在我们将其捕获到 prevOwner 中之前更新。

下面是更新后的规范，显示了完整的修改规则：

Copyghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

// Updated rule: now includes an initial sync call
rule checkOwnerConsistency(env e) {

    // NEW: Force an SLOAD of `owner` so the hook fires and syncs `ghostOwner`
    resetCounter(e);

    /// Take the first snapshot after synchronization
    address prevOwner = ghostOwner;

    //parametric call
    method f;
    calldataarg args;
    f(e, args);

    // Take another snapshot after the call
    address currentOwner = ghostOwner;

    // The owner must not change across any call
    assert prevOwner == currentOwner;
}

规则内部的第一行 (resetCounter(e);) 是关键的补充。

现在 ghost 已正确同步，prevOwner 和 currentOwner 之间的比较变得有意义，从而允许 Prover 正确验证 owner 变量的一致性。

让我们逐步分解这里发生了什么：

初始同步调用 (resetCounter(e))
- 规则通过调用 resetCounter(e) 开始。
- 为了检查 onlyOwner 修改器，合约必须读取 owner 槽 (SLOAD)。
- 该读取触发了 Sload hook，它将观察到的值写入 ghost ghostOwner。
- 因此，在我们进行任何快照之前，ghostOwner 现在已与实际存储值同步。
第一次快照 (prevOwner)
- 同步后，规则立即执行 address prevOwner = ghostOwner;。
- 由于步骤 1，prevOwner 是合约中存储的真实 owner。
任意调用 (method f; calldataarg args; f(e, args);)
- Prover 现在探索一个带有符号输入的任意外部调用。
- 在此合约中，这意味着 increment(...) 或 resetCounter(...) 带有任意参数。
- 这两个函数都受 onlyOwner 保护，并且不写入 owner。
- 在此调用期间，任何对 owner 的额外读取（因为 onlyOwner）都将重新触发 Sload hook，但它只会将相同的值写入 ghost。
第二次快照 (currentOwner)
- 任意调用返回后，规则执行 address currentOwner = ghostOwner;。
- 由于合约在部署后从未修改 owner，并且 hook 仅镜像读取，因此 currentOwner 等于先前捕获的相同存储支持的值。
断言
- 规则检查 assert prevOwner == currentOwner;。
- 由于合约在部署后从未修改 owner，因此没有代码路径可以使这两个快照不同。
- 因此，在所有探索的执行中，prevOwner 和 currentOwner 始终保持相等。
- 结果，Prover 未发现反例并报告规则已验证。

在 owner 属性验证后，现在让我们转向我们之前确定的第二个属性。

验证 `Counter` 合约中的 `Increment()` 调用

我们要证明的第二个属性是，对 increment() 的调用应该使 count 恰好增加 1。由于 count 是私有的，规则本身无法观察到 count++ 执行的实际存储写入。为了证明此属性，我们将一个 store hook 附加到 count 槽，捕获写入前后的值，将它们持久化到 ghosts 中，最后在规则中断言算术关系。

以下是完整的规范：

Copymethods {
    function increment() external;
}

ghost mathint ghost_prevCount;

ghost mathint ghost_currentCount;

hook Sstore count uint256 postcallValue (uint256 precallValue) {
    ghost_prevCount = precallValue;
    ghost_currentCount = postcallValue;
}

rule checkCounter() {

    env e;

    //call to increment
    increment(e);

    assert ghost_currentCount == ghost_prevCount + 1;
}

在上面的规范中，每当调用 increment() 函数时，hook 都会观察对 count 存储槽的更新。旧值 (precallValue) 存储在一个 ghost 变量 (ghost_prevCount) 中，而新值 (postcallValue) 存储在另一个 (ghost_currentCount) 中。这允许规则检查在调用 increment() 函数后，计数器是否恰好增加了 1，正如预期的那样。

当我们在上面的规范上运行 Prover 时，我们将看到规则已通过验证，如下图所示：

让我们逐步分解这里发生的一切：

调用之前：合约的私有变量 count 有一些初始值（假设为 X）。
increment() 调用期间：
- EVM 执行 count++ 语句，这会转换为对 count 存储槽的读取和随后的写入。
- 就在写入发生之前，Sstore hook 被触发。
- hook 捕获即将被覆盖的值 (precallValue) 和正在写入的新值 (postcallValue)。
- 这些值存储在 ghost 变量 ghost_prevCount 和 ghost_currentCount 中。
规则检查：
- 函数调用完成后，规则断言 ghost_currentCount == ghost_prevCount + 1。
- 鉴于 ghost_currentCount = X + 1 且 ghost_prevCount = X，断言成立。

因此，我们从 Prover 获得了验证结果。换句话说，任何对 increment() 的调用都会使计数器恰好增加 1，并且 Prover 能够形式化验证此属性而没有找到任何反例。

Ghost 变量作为存储的扩展

我们可以看到，hooks 用于通过检测合约存储上的特定读取或写入操作来观察和收集数据。然而，由于在 hooks 内部声明的变量是 hooks 的局部变量，一旦 hook 执行完成，它们的值就会消失。为了在整个规范中保留和重用这些信息，CVL 引入了 ghost 变量——持久的、规范级别的存储，它镜像或扩展了合约的实际状态。因此，ghost 变量可以被视为合约存储的扩展。

事实上，Certora Prover 对 ghost 变量的处理与常规存储非常相似：

任何对 ghost 的更新都会在正在进行的事务稍后回滚时自动回滚，就像存储一样。
在验证运行开始时，ghosts（与其他 CVL 变量一样）代表任意（havoced）值，除非它们在规范中明确设置，这反映了 Prover 对存储的符号视图。

我们将在后面的章节中更详细地探讨这些行为，届时我们还将学习如何显式初始化 ghost 变量，以避免意外的任意化，并确保更可预测的验证结果。

结论

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

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

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

翻译
学分: 2
分类: 安全
标签: 形式化验证 Certora 存储钩子幽灵变量 Solidity 智能合约

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

存储Hook和幽灵变量介绍

存储 Hooks 和 Ghosts 介绍

理解“需求”

Hooks 是什么？

Hooks 的类型

什么是存储 Hooks？

1. Load Hooks

2. Store Hooks

理解 Hooks 的局限性

Hooks 的作用域限制

使用 Ghost 变量规避作用域限制

验证 `Counter` 合约中的 Owner 一致性

将 Ghosts 与存储同步

验证 `Counter` 合约中的 `Increment()` 调用

Ghost 变量作为存储的扩展

结论

0 条评论

文章目录

存储Hook和幽灵变量介绍

存储 Hooks 和 Ghosts 介绍

理解“需求”

Hooks 是什么？

Hooks 的类型

什么是存储 Hooks？

1. Load Hooks

2. Store Hooks

理解 Hooks 的局限性

Hooks 的作用域限制

使用 Ghost 变量规避作用域限制

验证 Counter 合约中的 Owner 一致性

将 Ghosts 与存储同步

验证 Counter 合约中的 Increment() 调用

Ghost 变量作为存储的扩展

结论

0 条评论

文章目录

验证 `Counter` 合约中的 Owner 一致性

验证 `Counter` 合约中的 `Increment()` 调用