形式化验证 Initializable.sol

使用 Certora 进行形式化验证

形式化验证 Initializable.sol

模块 1：规则和基本 CVL 语法

最后更新于 2026 年 2 月 17 日

本文描述了 Certora 如何形式化验证 OpenZeppelin 的 Initializable.sol 合约。我们假设读者已经熟悉该合约的使用方式。如果不是，请参阅我们关于 可初始化合约 的文章。

在可升级合约中，不使用构造函数。相反，在部署后，部署者调用 initialize(...)，这将状态变量设置为其初始条件。initialize(...) 函数只能被调用一次。

为了允许存储变量在以后设置为另一个值（例如，如果 ERC-20 代币更改其名称或 totalSupply），则这些更改必须通过 reinitialize 函数进行。外部函数不需要命名为“initializer”和“reinitializer”，但它们确实需要应用 OpenZeppelin 库中的 initializer() 和 reinitializer() 修饰符到这些函数上。

出于安全目的，可升级合约必须具有以下关于初始化的属性：

1. 一旦调用了 initializer，它就不应该再次被调用（所有调用都应该 revert）。
2. 不应该在实现合约中调用 initializer。只有代理合约中的 initializer 应该可被调用，因为所有状态都保存在代理合约中。这就是为什么代理模式的逻辑合约在构造函数中调用 _disableInitializers() 的原因。
3. 一旦 initializer 和 reinitializer 被禁用，它们应该永久保持禁用状态。
4. 如果我们调用 reinitializer 函数，我们必须将版本号从之前的版本递增。版本号存储为 uint64 变量。

请注意，对 initializer 和 reinitializer 的访问控制不在本合约的范围之内。合约甚至不强制规定这些函数的命名，它只确保修饰符的功能是正确的。

我们将涵盖 OpenZeppelin 的 Initializable.spec 文件的大部分内容，但不是全部，因为其中一些内容依赖于我们尚未涵盖的技术。但是，根据我们目前在课程中涵盖的内容，大部分内容应该是可以理解的。

这是我们检查的第一个规则：

Copyrule cannotInitializeTwice() {
    require isInitialized(); // 要求已初始化

    initialize@withrevert(); // 调用 initialize 并期望其 revert

    assert lastReverted, "contract must only be initialized once"; // 断言最后一次调用已 revert，合约只能初始化一次
}

这表示如果合约已初始化，则调用 initialize() 将会 revert。此规则没有说明如果合约未初始化，则调用 initialize() 不会 revert，换句话说，未初始化的合约可以被初始化。require 语句将规则的范围设置为仅涵盖 initializer 已被调用的情况。

以下规则涵盖了未初始化的合约可以被初始化的规范：

Copyrule initializeEffects() {
    requireInvariant notInitializing(); // 要求不在初始化状态

    bool isUninitializedBefore = isUninitialized(); // 记录初始化前是否未初始化

    initialize@withrevert(); // 调用 initialize 并期望其 revert
    bool success = !lastReverted; // 成功与否取决于是否 revert

    assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts"; // 断言成功当且仅当初始化前未初始化，只能初始化未初始化的合约
    assert success => version() == 1,         "initialize must set version() to 1"; // 断言如果成功，版本必须设置为 1

}

该规则表示 initialize 成功当且仅当合约之前未被初始化。如果初始化成功，则版本必须设置为 1。requireInvariant 语法是我们尚未涵盖的内容，我们将在后续教程中重新讨论。

reinitializer 不能覆盖禁用状态的规则很大程度上是不言自明的：

Copyrule cannotReinitializeOnceDisabled() {
    require isDisabled(); // 要求已禁用

    uint64 n; // 声明一个 uint64 变量 n
    reinitialize@withrevert(n); // 调用 reinitialize 并期望其 revert

    assert lastReverted, "contract is disabled"; // 断言最后一次调用已 revert，合约已禁用
}

换句话说，如果合约被禁用，则任何对 reinitialize 的调用都会导致 revert。

当调用 reinitializer 时，必须设置一个新版本，并且该版本必须大于旧版本。以下规则表示，如果新版本是参数中传递的版本，并且如果交易没有 revert，那么新版本会大于之前的版本。

Copyrule reinitializeEffects() {
    requireInvariant notInitializing(); // 要求不在初始化状态

    uint64 versionBefore = version(); // 记录初始化前的版本

    uint64 n; // 声明一个 uint64 变量 n
    reinitialize@withrevert(n); // 调用 reinitialize 并期望其 revert
    bool success = !lastReverted; // 成功与否取决于是否 revert

    assert success <=> versionBefore < n, "can only reinitialize to a later versions"; // 断言成功当且仅当旧版本小于新版本 n，只能重新初始化到更高版本
    assert success => version() == n,     "reinitialize must set version() to n"; // 断言如果成功，版本必须设置为 n
}

我们检查的最后一条规则指出，如果合约不在“初始化状态”（合约当前正在设置存储变量或重新初始化），那么调用 disable 总是成功的。

Copyrule disableEffect() {
    requireInvariant notInitializing(); // 要求不在初始化状态

    disable@withrevert(); // 调用 disable 并期望其 revert
    bool success = !lastReverted; // 成功与否取决于是否 revert

    assert success,      "call to _disableInitializers failed"; // 断言成功，调用 _disableInitializers 失败
    assert isDisabled(), "disable state not set"; // 断言已禁用，禁用状态未设置
}

总结

我们在此展示的规则非常容易理解，但我们对其进行回顾是为了证明形式化验证并不总是复杂的。我们在此展示的规则可以通过单元测试来完成，但形式化验证更加彻底且具有更高的保证。

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

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