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

• onlyOwner()

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

• renounceOwnership()

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

• transferOwnership(address)

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

以下是 OpenZeppelin Ownable contract，供在解释其形式化验证方法时作为参考：

Copy
// SPDX-License-Identifier: MIT
// OpenZeppelin Contracts (last updated v5.0.0) (access/Ownable.sol)

pragma solidity ^0.8.20;

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

/**
 * @dev Contract module which provides a basic access control mechanism, where
 * there is an account (an owner) that can be granted exclusive access to
 * specific functions.
 *
 * The initial owner is set to the address provided by the deployer. This can
 * later be changed with {transferOwnership}.
 *
 * This module is used through inheritance. It will make available the modifier
 * `onlyOwner`, which can be applied to your functions to restrict their use to
 * the owner.
 */
abstract contract Ownable is Context {
    address private _owner;

    /**
     * @dev The caller account is not authorized to perform an operation.
     */
    error OwnableUnauthorizedAccount(address account);

    /**
     * @dev The owner is not a valid owner account. (eg. `address(0)`)
     */
    error OwnableInvalidOwner(address owner);

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

    /**
     * @dev Initializes the contract setting the address provided by the deployer as the initial owner.
     */
    constructor(address initialOwner) {
        if (initialOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(initialOwner);
    }

    /**
     * @dev Throws if called by any account other than the owner.
     */
    modifier onlyOwner() {
        _checkOwner();
        _;
    }

    /**
     * @dev Returns the address of the current owner.
     */
    function owner() public view virtual returns (address) {
        return _owner;
    }

    /**
     * @dev Throws if the sender is not the owner.
     */
    function _checkOwner() internal view virtual {
        if (owner() != _msgSender()) {
            revert OwnableUnauthorizedAccount(_msgSender());
        }
    }

    /**
     * @dev Leaves the contract without owner. It will not be possible to call
     * `onlyOwner` functions. Can only be called by the current owner.
     *
     * NOTE: Renouncing ownership will leave the contract without an owner,
     * thereby disabling any functionality that is only available to the owner.
     */
    function renounceOwnership() public virtual onlyOwner {
        _transferOwnership(address(0));
    }

    /**
     * @dev Transfers ownership of the contract to a new account (`newOwner`).
     * Can only be called by the current owner.
     */
    function transferOwnership(address newOwner) public virtual onlyOwner {
        if (newOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(newOwner);
    }

    /**
     * @dev Transfers ownership of the contract to a new account (`newOwner`).
     * Internal function without access restriction.
     */
    function _transferOwnership(address newOwner) internal virtual {
        address oldOwner = _owner;
        _owner = newOwner;
        emit OwnershipTransferred(oldOwner, newOwner);
    }
}

OZ 的 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

下面的修改版本在功能上等同于原始版本，并将用于接下来的讨论：

Copy
methods {
    function restricted() external;
    function owner() external returns (address) envfree; // taken from the import IOwnable.spec
}


definition
 nonpayable(env e) returns bool = e.msg.value == 0; // taken from the helpers.spec

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership changes ownership                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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), "unauthorized caller or invalid arg";
    assert success => owner() == newOwner, "current owner changed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

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

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => owner() == 0, "owner not cleared";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership can only change in specific ways                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

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

    address newCurrent = owner();

    // If owner changes, must be either transferOwnership or 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 关键字的使用。它为规范中常用的表达式声明了可重用的逻辑，并在大多数规则中被调用：

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

当调用未发送以太币时，即当 msg.value == 0 时，nonpayable(env e) 返回 true。

还需要提到的是，规范调用了一个名为 restricted() 的函数，该函数不是 Ownable 合约的一部分。相反，它是在继承自抽象合约 Ownable 的 harness contract 中实现的。

当我们运行验证时，我们验证的是 harness contract。harness contract 通常会做更多的事情，但这属于另一章的主题。目前，重要的是我们添加了一个 restricted() 函数并应用了 onlyOwner 修饰符。

以下是 harness contract 的实现：

Copy
/// OwnableHarness.sol

import {Ownable} from "src/Ownable/Ownable.sol"; // import path: modify as necessary

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

    function restricted() external onlyOwner {}
}

访问控制

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

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

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

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

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

代码行 address current = owner() 获取当前的所有者地址，随后该地址将被用于断言中。

现在考虑以下几行代码，它们需要多一点解释：

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

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

Copy
restricted@withrevert(e);

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

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

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

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

“Method declaration for OwnableHarness.restricted() is neither envfree, optional, nor summarized, so it has no effect.”_

正如我们上一章所讨论的，如果一个函数依赖于环境并按此处理，则不需要将其包含在 methods 块中。在这种情况下，我们可以通过从 methods 块中删除 function restricted() e``xternal 这一行来简化。

最后，断言部分：

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

这意味着_“当且仅当调用者是_ current 地址时，调用才会成功”。在所有其他情况下，函数必须回退。当然，如果发送了以太币，函数也可能回退，但我们在本规则中使用 require nonpayable(e) 语句明确排除了那种情况。

放弃所有权

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

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

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

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => owner() == 0, "owner not cleared";
}

乍看之下，规则将 !lastReverted 赋值给 success，这在两个断言中都被用到了。

第一个断言：

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

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

第二个断言：

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

是一个蕴含关系。这意味着_“如果调用成功，那么所有者必须被清除（即设置为_ address(0)）”。换句话说，所有权必须被放弃。

转移所有权

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

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

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership changes ownership                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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), "unauthorized caller or invalid arg";
    assert success => owner() == newOwner, "current owner changed";
}

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

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

它基于这样的前提：当且仅当调用者是当前所有者且 newOwner 是有效（非零）地址时，调用才会成功。条件 newOwner != 0 是必要的，因为如果移除它，将会违反 Solidity 函数的内部检查并导致回退（从而产生验证违规）。

Copy
/// Ownable.sol

function transferOwnership(address newOwner) public virtual onlyOwner {
    if (newOwner == address(0)) { // this line will cause a revert if newOwner is zero
        revert OwnableInvalidOwner(address(0));
    }
    _transferOwnership(newOwner);
}

现在看这条规则的最后一个断言，

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

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

参数化规则

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

• transferOwnership()，产生一个非零的新所有者；或者
• renounceOwnership()，产生一个零地址作为新所有者

规则如下：

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership can only change in specific ways                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

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

    address newCurrent = owner();

    // If owner changes, must be either transferOwnership or 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) 置于这两个调用之间，我们允许执行任意函数，并检查其是否导致所有权的改变。

现在来看断言：

Copy
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()`。

根据该规则，这是仅有的两条合法的改变所有权的途径。

本文是有关 formal verification using the Certora Prover 系列文章的一部分