形式化验证 Ownable.sol

使用Certora进行形式化验证

形式化验证 Ownable.sol

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

最后更新于2026年2月17日

Ownable 是一个抽象合约，它提供基于所有者的访问控制。当被继承时，它使用 onlyOwner 修饰符限制特定函数只能由所有者调用。它有三个核心机制，每个机制都通过以下函数实现：

• onlyOwner()

  这个修饰符限制对特定函数的访问，只允许所有者调用它们。

• renounceOwnership()

  这个公共函数受 onlyOwner 修饰符保护，只允许所有者调用它。执行时，它将所有者设置为零地址（address(0)）。放弃所有权后，所有受 onlyOwner 限制的函数将永久不可访问。

• transferOwnership(address)

  这也是一个公共函数，与 renounceOwnership() 类似，受 onlyOwner 修饰符限制。当使用有效的参数地址（不是 address(0)）调用时，它将合约的所有权更新为该地址，即使该地址与当前所有者相同。

以下是 OpenZeppelin Ownable 合约，提供参考，同时解释其形式化验证方法：

// SPDX-License-Identifier: MIT
// OpenZeppelin Contracts (最后更新 v5.0.0) (access/Ownable.sol)

pragma solidity ^0.8.20;

import {Context} from "../utils/Context.sol";

/**
 * @dev 提供基本访问控制机制的合约模块，其中有一个账户（所有者）可以被授予对特定函数的独占访问权限。
 *
 * 初始所有者被设置为部署者提供的地址。这可以稍后通过 {transferOwnership} 更改。
 *
 * 此模块通过继承使用。它将提供 `onlyOwner` 修饰符，可应用于你的函数以限制其仅供所有者使用。
 */
abstract contract Ownable is Context {
    address private _owner;

    /**
     * @dev 调用者账户未被授权执行操作。
     */
    error OwnableUnauthorizedAccount(address account);

    /**
     * @dev 所有者不是有效的所有者账户。（例如，`address(0)`）
     */
    error OwnableInvalidOwner(address owner);

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    /**
     * @dev 初始化合约，将部署者提供的地址设置为初始所有者。
     */
    constructor(address initialOwner) {
        if (initialOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(initialOwner);
    }

    /**
     * @dev 如果由所有者以外的任何账户调用，则抛出异常。
     */
    modifier onlyOwner() {
        _checkOwner();
        _;
    }

    /**
     * @dev 返回当前所有者的地址。
     */
    function owner() public view virtual returns (address) {
        return _owner;
    }

    /**
     * @dev 如果发送者不是所有者，则抛出异常。
     */
    function _checkOwner() internal view virtual {
        if (owner() != _msgSender()) {
            revert OwnableUnauthorizedAccount(_msgSender());
        }
    }

    /**
     * @dev 使合约没有所有者。将无法调用 `onlyOwner` 函数。只能由当前所有者调用。
     *
     * 注意：放弃所有权将使合约没有所有者，从而禁用仅供所有者使用的任何功能。
     */
    function renounceOwnership() public virtual onlyOwner {
        _transferOwnership(address(0));
    }

    /**
     * @dev 将合约的所有权转移到一个新账户（`newOwner`）。只能由当前所有者调用。
     */
    function transferOwnership(address newOwner) public virtual onlyOwner {
        if (newOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(newOwner);
    }

    /**
     * @dev 将合约的所有权转移到一个新账户（`newOwner`）。内部函数，没有访问限制。
     */
    function _transferOwnership(address newOwner) internal virtual {
        address oldOwner = _owner;
        _owner = newOwner;
        emit OwnershipTransferred(oldOwner, newOwner);
    }
}

OpenZeppelin 的 Ownable CVL 规范

以下是 Ownable 合约的 CVL 规范链接：Ownable CVL Specification。

为了简化，我们进行了少量修改，将以下定义直接放入规范文件，而不是从 IOwnable.spec 和 helpers.spec 中导入：

• function owner() external returns (address) envfree (放置在 methods 块内)
• definition nonpayable(env e) returns bool = e.msg.value == 0

下面这个修改后的版本在功能上与原版等效，并将用于讨论：

methods {
    function restricted() external;
    function owner() external returns (address) envfree; // 取自 import IOwnable.spec
}

definition
 nonpayable(env e) returns bool = e.msg.value == 0; // 取自 helpers.spec

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 函数正确性：transferOwnership 更改所有权                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> (e.msg.sender == current && newOwner != 0), "未经授权的调用者或无效参数";
    assert success => owner() == newOwner, "当前所有者已更改";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 函数正确性：renounceOwnership 移除所有者                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "未经授权的调用者";
    assert success => owner() == 0, "所有者未清除";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 访问控制：只有当前所有者可以调用受限函数                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "访问控制失败";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 规则：所有权只能以特定方式更改                                                                                            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

    method f; calldataarg args;
    f(e, args);

    address newCurrent = owner();

    // 如果所有者更改，必须是 transferOwnership 或 renounceOwnership 之一
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
    );
}

注意 definition 关键词的使用。它声明了用于整个规范中常见表达式的可重用逻辑，并在大多数规则中被调用：

definition nonpayable(env e) returns bool = e.msg.value == 0;

nonpayable(env e) 在调用不发送以太币时（即 msg.value == 0）返回 true。

同样值得一提的是，该规范调用了一个名为 restricted() 的函数，它不是 Ownable 合约的一部分。相反，它是在继承自抽象合约 Ownable 的 测试辅助合约 中实现的。

当我们运行验证时，我们正在验证这个测试辅助合约。测试辅助合约通常做得更多，但这将是另一个章节的主题。目前，重要的是我们添加了一个 restricted() 函数并应用了 onlyOwner 修饰符。

以下是测试辅助合约的实现：

/// OwnableHarness.sol

import {Ownable} from "src/Ownable/Ownable.sol"; // 导入路径：根据需要修改

contract OwnableHarness is Ownable {
    constructor(address initialOwner) Ownable(initialOwner) {}

    function restricted() external onlyOwner {}
}

访问控制

我们从最基本的规则开始：onlyCurrentOwnerCanCallOnlyOwner()。这条规则验证 onlyOwner 修饰符是否阻止非所有者调用受限函数：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 访问控制：只有当前所有者可以调用受限函数                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "访问控制失败";
}

require nonpayable(e) 这行意味着规则的其余部分将仅针对不发送以太币（e.msg.value == 0）的交易进行评估；所有其他输入都将从分析中排除。

address current = owner() 这行检索当前所有者地址，然后将其用于断言中。

现在考虑以下几行，它们需要更多解释：

calldataarg args;
restricted@withrevert(e, args);

calldataarg args 这行将任意参数传递给函数调用 restricted@withrevert(e, args)。但是，这可以简化为：

restricted@withrevert(e);

因为 Prover 默认自动为输入分配任意值，使得在这种情况下 calldataarg 不必要（而且 restricted() 没有参数）。两种形式都是有效的，并反映了规范编写者的偏好。

现在下一个问题是它是否应该包含在 methods 块中：

methods {
    function restricted() external;
    ...
}

OpenZeppelin 规范包含了它。然而，这样做会产生一个警告（即使此规则已验证）：

“方法声明 OwnableHarness.restricted() 既不是 envfree，也不是 optional，也没有被汇总，因此它没有效果。”

正如我们在前一章讨论的那样，如果一个函数是环境依赖的并如此处理，则无需将其包含在 methods 块中。在这种情况下，我们可以通过从 methods 块中移除 function restricted() external 行来简化。

现在，最后是断言：

assert !lastReverted <=> e.msg.sender == current, "access control failed";

这意味着当且仅当调用者是 current 地址时，调用才成功。在所有其他情况下，函数必须回滚。当然，如果函数与以太币一起发送，它可能会回滚，但我们在此规则中通过 require nonpayable(e) 语句明确排除了这种情况。

放弃所有权

这条规则验证只有所有者可以放弃所有权，如果成功，所有者地址将被设置为 address(0)。以下是规则：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 函数正确性：renounceOwnership 移除所有者                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "未经授权的调用者";
    assert success => owner() == 0, "所有者未清除";
}

乍一看，该规则将 !lastReverted 赋值给 success，它在两个断言中都使用了。

第一个断言：

assert success <=> e.msg.sender == current, "unauthorized caller";

确认了与上一条规则相同的逻辑：当且仅当调用者是当前所有者时，调用才成功。

第二个断言：

assert success => owner() == 0, "owner not cleared";

是一个蕴涵。它意味着如果调用成功，则所有者必须被清除（即，设置为 address(0)）。换句话说，所有权必须被放弃。

转移所有权

这条规则验证，如果调用成功，调用者必须是当前所有者，并且新地址必须是有效地址（即，不是 address(0)）。

现在我们来看 transferOwnership() 的规则：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 函数正确性：transferOwnership 更改所有权                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> (e.msg.sender == current && newOwner != 0), "未经授权的调用者或无效参数";
    assert success => owner() == newOwner, "当前所有者已更改";
}

与之前的规则一样，这个断言：

assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";

其前提是当且仅当调用者是当前所有者并且 newOwner 是一个有效（非零）地址时，调用才成功。条件 newOwner != 0 是必要的，因为如果移除它，将违反 Solidity 函数的内部检查并导致回滚（因此是违规）。

/// Ownable.sol

function transferOwnership(address newOwner) public virtual onlyOwner {
    if (newOwner == address(0)) { // 如果 newOwner 为零，此行将导致回滚
        revert OwnableInvalidOwner(address(0));
    }
    _transferOwnership(newOwner);
}

现在是这条规则的最后一个断言：

assert success => owner() == newOwner, "current owner changed";

这意味着如果调用成功，则所有者必须更新为 newOwner。

参数化规则

现在，Ownable 合约的三个核心功能已经过形式化验证，还剩最后一个规则：一个验证所有权变更的参数化规则。该规则断言，如果所有者变更，则必须通过以下方式之一发生：

• transferOwnership() 导致新所有者非零或
• renounceOwnership() 导致新所有者为零地址

以下是规则：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 规则：所有权只能以特定方式更改                                                                                            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

    method f; calldataarg args;
    f(e, args);

    address newCurrent = owner();

    // 如果所有者更改，必须是 transferOwnership 或 renounceOwnership 之一
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
    );
}

这是一个参数化规则，其存在 f(e, args) 调用就是证明。在方法 f(e, args) 调用之前和之后的行中，我们使用 owner() 检索 oldCurrent 和 newCurrent。很明显，我们正在跟踪所有权状态的更改。通过将 f(e, args) 放置在这两个调用之间，我们允许任意函数执行并检查它是否导致所有权更改。

现在是断言：

assert oldCurrent != newCurrent => (
    (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
    (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
);

如果所有者已更改（oldCurrent != newCurrent），则此更改必须通过以下两种有效方式之一发生：

• e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector)

  这意味着调用者必须是当前所有者，新所有者不是零地址，并且触发更改的函数是 transferOwnership()。

• e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)

  这意味着调用者仍然是当前所有者，但新所有者是零地址，并且使用的函数必须是 renounceOwnership()。

根据该规则，这些是更改所有权的唯一两种合法途径。

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

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