ERC-721 的转移与授权规则

本文详细介绍了如何使用Certora Prover对ERC-721代币的transferFrom()、approve()、setApprovalForAll()以及balanceOf(0)等核心功能进行形式化验证。文章通过具体的Certora验证语言（CVL）代码示例，深入解析了每个规则的前置条件、状态记录、方法调用以及活性、效果和无副作用断言，旨在确保代币操作的正确性和安全性。

Formal Verification with Certora

ERC-721 的转账与批准规则

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

最后更新日期：2026 年 2 月 13 日

引言

本章继续作为 OpenZeppelin 的 ERC-721 CVL 规范代码演练的第三部分 (3/5)，重点关注代币转账和批准规则，具体包括：

  • transferFrom()
  • approve()
  • setApprovalForAll()
  • zeroAddressBalanceRevert()

这些规则验证所有权转移、按代币批准、所有代币的操作者批准，以及查询 balanceOf(0) 会回滚。

形式化验证 transferFrom()

transferFrom() 函数将 NFT 的所有权更改为另一个地址。它假定 NFT 已经铸造，并且只能由所有者、经批准用于该代币 ID 的地址，或者经批准用于所有者所有代币的操作者调用。

以下是 transferFrom 规则，我们将在代码块后逐节解释：

rule transferFrom(env e, address from, address to, uint256 tokenId) {
    // preconditions
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    // pre-call state
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    // method call
    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

前置条件

这些前置条件指定了 Prover 执行 transferFrom() 之前必须为真的情况。我们将在代码块后解释每一行：

require nonpayable(e);
require authSanity(e);
...
requireInvariant ownerHasBalance(tokenId);
require balanceLimited(to);

require nonpayable(e)

这要求 transferFrom() 在不发送 ETH 的情况下被调用，因为该函数是 non-payable。它被表达为一个定义：

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

它将条件 $e.msg.value == 0$ 定义为一个名为 $nonpayable(e)$ 的可重用表达式，该表达式检查调用是否未附带 ETH。

尽管 ERC-721 标准将 transferFrom() 指定为 payable，但 OpenZeppelin 将其实现为 non-payable。实际上，NFT 转账不期望附带 ETH，因此这已成为一种实际惯例。CVL 规则强制执行 $e.msg.value == 0$。

require authSanity(e)

这要求调用者不是零地址。它也被表达为一个 definition：

definition authSanity(env e) returns bool = e.msg.sender != 0

如果没有此要求，Prover 会将 address(0) 视为有效的调用者，即使实际调用不可能源自 address(0)。合约的授权逻辑绝不允许 address(0) 作为所有者、批准地址或操作者，因此任何来自 address(0) 作为调用者而引起的违规都是误报。

requireInvariant ownerHasBalance(tokenId)

此先决条件要求在规则开始时 ownerHasBalance($tokenId$) 不变量（它保证如果代币存在，其所有者拥有正余额）成立。它强制 Prover 在一个状态下开始，其中任何现有代币都拥有有效的（非零）所有者：

rule transferFrom(env e, address from, address to, uint256 tokenId) {
    // preconditions
    require nonpayable(e);
    require authSanity(e);
    ...
    requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
    require balanceLimited(to);
    ...
}
// invariant as a precondition

invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    ...

ownerHasBalance 不变量通过保留块依赖于另一个不变量 balanceOfConsistency，它验证 balanceOf、_ownedByUser 和 ghost _balances 是否相等：

invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    {
        preserved { // invariant as a preserved condition
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
    }
// invariant as a preserved condition

invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

通过使用不变量 ownerHasBalance($tokenId$) 作为前置条件，transferFrom 规则继承了 balanceOfConsistency 保证：

rule transferFrom(env e, address from, address to, uint256 tokenId) {
    // preconditions
    require nonpayable(e);
    require authSanity(e);
    ...
    requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
    require balanceLimited(to);
    ...
}

如果删除此先决条件，Prover 可能会在不可能的状态下开始规则，其中所有权和余额不匹配——例如，一个地址可能被记录为代币的所有者，而其余额为零，因为 ghost 值与存储不一致。这会导致误报违规。

require balanceLimited(to)

balanceLimited($to$) 将接收方 ($to$) 地址的余额限制在 $max\_uint256$ 以下，如定义所示：

definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

合约在 unchecked 块中增加余额以提高 gas 效率。尽管溢出实际上不可能发生，但 Prover 仍然会探索溢出情况，因为 transferFrom() 调用 _update()，而余额增加发生在 unchecked 块内：

// ERC721.sol

function transferFrom(address from, address to, uint256 tokenId) public virtual {
    ...
    address previousOwner = _update(to, tokenId, _msgSender());
    ..
}
/// ERC721.sol

function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
    ...

    if (to != address(0)) {
        unchecked {
            _balances[to] += 1;
        }
    }
      ...
}

使用 require balanceLimited($to$) 排除了实际上无法达到的溢出状态，这些状态会导致规则在不切实际的场景中失败。

调用前状态

在调用 transferFrom() 方法之前，我们记录状态变量，以便与调用后的值进行比较：

  • $balanceOfFromBefore$ 是转账前发送方 ($from$) 的余额。
  • $balanceOfToBefore$ 是转账前接收方 ($to$) 的余额。
  • $balanceOfOtherBefore$ 是转账前一个不相关账户 ($otherAccount$) 的余额。
  • $ownerBefore$ 是待转账代币的所有者。
  • $otherOwnerBefore$ 是一个不相关代币的所有者。
  • $approvalBefore$ 是待转账代币的批准。
  • $otherApprovalBefore$ 是一个不相关代币的批准。
uint252 balanceOfFromBefore  = balanceOf(from);
uint256 balanceOfToBefore    = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore          = unsafeOwnerOf(tokenId);
address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
address approvalBefore       = unsafeGetApproved(tokenId);
address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

请注意，我们使用 unsafeGetApproved()（一个辅助函数）读取批准，而不是合约的 getApproved()。辅助版本会暴露批准值，即使代币未铸造或已销毁（$owner == address(0)$），因为它返回 $_getApproved(tokenId)$，而不检查代币是否存在或是否有所有者。相比之下，实际合约中的 getApproved() 会执行所有权检查，如果代币未铸造或已销毁，则会回滚：

// ERC721Harness.sol -- returns approval without checking token existence or ownership

function unsafeGetApproved(uint256 tokenId) external view returns (address) {
    return _getApproved(tokenId);
}
// ERC721.sol -- performs an ownership check and reverts if the token is unminted or burned

function getApproved(uint256 tokenId) public view virtual returns (address) {
    _requireOwned(tokenId); // reverts if `owner == address(0)`

    return _getApproved(tokenId);
}

这阻止了查询未铸造或已销毁代币的批准状态，因为 getApproved() 在这些情况下会回滚。然而，规则需要在通过零地址状态的状态转换中比较批准值：

  • 代币创建（未铸造到已铸造）——所有者从 address(0) 转换为非零地址
  • 代币销毁（已铸造到未铸造/已销毁）——所有者从非零地址转换回 address(0)

因此，需要 unsafeGetApproved()，以便规则即使在代币处于零地址所有者状态时也能读取批准值。

现在已记录调用前状态，我们将执行 transferFrom() 并推断后续断言中的调用后值。

转账调用

transferFrom() 调用与 @withrevert 指示 Prover 探索回滚和非回滚路径。!$lastReverted$ 条件捕获调用是否未回滚，并将其存储为 $success$：

transferFrom@withrevert(e, from, to, tokenId);
bool success = !lastReverted;

断言——活性、效果和无副作用

活性：

当且仅当 ($\Leftrightarrow$) 以下所有条件都成立时，转账不会回滚：

  • $from == ownerBefore$

发送方 ($from$) 地址（代币从中转出）必须是代币的前所有者。

  • $from \neq 0$

发送方 ($from$) 地址不能是零地址。

  • $to \neq 0$

接收方 ($to$) 地址不能是零地址。

  • ($operator == from$ || $operator == approvalBefore$ || $isApprovedForAll(ownerBefore, operator)$)

操作者（调用者）必须通过以下至少一种方式获得授权：

  • $operator == from$ —— 所有者转移自己的代币
  • $operator == approvalBefore$ —— 操作者对该代币有特定的批准（通过 approve()）
  • $isApprovedForAll(ownerBefore, operator)$ —— 操作者对所有者所有代币有全局批准（通过 setApprovalForAll()）
// liveness
assert success <=> (
    from == ownerBefore &&
    from != 0 &&
    to   != 0 &&
    (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
);

效果：

如果转账没有回滚，则应用以下状态更改：

  • $to\_mathint(balanceOf(from)) == balanceOfFromBefore - assert\_uint256(from \neq to ? 1 : 0)$

发送方的余额减少 1，除了自转账 ($from == to$) 情况下，余额保持不变。

  • $to\_mathint(balanceOf(to)) == balanceOfToBefore + assert\_uint256(from \neq to ? 1 : 0)$

接收方的余额增加 1，除了自转账 ($from == to$) 情况下，余额保持不变。

  • $unsafeOwnerOf(tokenId) == to$

接收方 ($to$) 地址成为 $tokenId$ 的新所有者。

  • $unsafeGetApproved(tokenId) == 0$

$tokenId$ 的批准被清除。

// effect
assert success => (
    to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
    to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
    unsafeOwnerOf(tokenId)                 == to &&
    unsafeGetApproved(tokenId)             == 0
);

无副作用：

在断言预期状态更改（效果）之后，我们还检查余额、所有权或批准上没有发生意外副作用：

  • 关于余额

$balanceOf(otherAccount) \neq balanceOfOtherBefore \Rightarrow (otherAccount == from || otherAccount == to)$

如果任何账户的余额发生变化，则意味着 ($\Rightarrow$) 该账户是发送方或接收方。没有其他不相关账户的余额被修改。

  • 关于所有权

$unsafeOwnerOf(otherTokenId) \neq otherOwnerBefore \Rightarrow otherTokenId == tokenId$

如果任何代币的所有权发生变化，则意味着 ($\Rightarrow$) 该代币是被转移的代币。没有其他不相关代币的所有权被更改。

  • 关于批准

$unsafeGetApproved(otherTokenId) \neq otherApprovalBefore \Rightarrow otherTokenId == tokenId$

如果任何代币的批准发生变化，则意味着 ($\Rightarrow$) 该代币是被转移的代币。没有其他不相关代币的批准被修改。

// no side effect
assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

以下是规则 transferFrom 的完整规范：

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool)    envfree;

    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

以下是 Prover 运行结果。

既然我们已经验证了 transferFrom()，我们就可以转向授权这些转账的批准机制。

回想一下，transferFrom() 仅在调用者拥有适当授权时才能成功：作为代币所有者、作为经批准用于该代币的地址，或作为经批准用于所有者所有代币的操作者。接下来的两条规则验证授予这些权限的函数：approve() 用于按代币授权，setApprovalForAll() 用于操作者级别的授权。

形式化验证 approve()

approve() 合约函数授予一个地址转移特定代币的权限。它仅在代币存在且调用者是所有者或操作者（拥有全局批准）时才能成功。

以下是验证此行为的规则：

rule approve(env e, address spender, uint256 tokenId) {
    // preconditions
    require nonpayable(e);
    require authSanity(e);

    // pre-call state
    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    // method call
    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

前置条件

到目前为止，我们已经知道 $nonpayable(e)$ 要求调用不附带 Ether，而 $authSanity(e)$ 要求 $msg.sender$ 不是零地址：

require nonpayable(e);
require authSanity(e);

批准调用

作为 OpenZeppelin 的 ERC-721 规则规范中的一个常见模式，approve 方法使用 @withrevert 调用，!$lastReverted$ 的结果存储在 $success$ 变量中，以便推断调用成功的情况：

approve@withrevert(e, spender, tokenId);
bool success = !lastReverted;

断言——活性、效果和无副作用

活性：

这意味着函数调用不会回滚当且仅当以下条件得到满足：

  • $owner \neq 0$

代币所有者不能是零地址。这可以防止批准不存在或已销毁的代币。

  • ($owner == caller$ || $isApprovedForAll(owner, caller)$)

这是一个授权检查，其中 $caller$ 必须：

  • 是代币的 $owner$，或者
  • 是通过 $isApprovedForAll(owner, caller)$（返回 true）批准的操作者
// liveness
assert success <=> (
    owner != 0 &&
    (owner == caller || isApprovedForAll(owner, caller))
);

效果：

  • $success \Rightarrow unsafeGetApproved(tokenId) == spender$

如果调用成功 ($success == true$)，那么 $tokenId$ 的批准地址现在必须等于 $spender$。

// effect
assert success => unsafeGetApproved(tokenId) == spender;

无副作用：

  • $unsafeGetApproved(otherTokenId) \neq otherApprovalBefore \Rightarrow otherTokenId == tokenId$

如果 $otherTokenId$ 的批准地址发生变化，那么 $otherTokenId$ 必须与 $tokenId$ 相同。这意味着只有 $tokenId$（预期目标）的批准被更新，而没有其他代币 ($otherTokenId$) 被意外影响。

// no side effect
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

以下是 approve 规则的完整规范：

methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

以下是 Prover 运行结果。

形式化验证setApprovalForAll()

setApprovalForAll() 函数授权一个地址管理调用者拥有的所有代币。以下是该规则：

rule setApprovalForAll(env e, address operator, bool approved) {
    // preconditions
    require nonpayable(e);

    // pre-call state
    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

至此，我们已经熟悉了前置条件、调用前和调用后状态以及方法调用的模式，因此我们将跳过这些，直接进入断言。

断言——活性、效果和无副作用

活性：

  • $assert success \Leftrightarrow operator \neq 0$

当且仅当操作者不是零地址时，调用成功。ERC-721 禁止将零地址批准为操作者，因此此断言要求当 $operator == 0$ 时调用失败：

// liveness
assert success <=> operator != 0;

效果：

  • $assert success \Rightarrow isApprovedForAll(owner, operator) == approved$

如果调用成功，($owner$, $operator$) 对的批准状态必须与 $approved$ 布尔值匹配。这意味着批准值（真或假）已正确设置。

// effect
assert success => isApprovedForAll(owner, operator) == approved;

无副作用：

  • 如果任何 ($otherOwner$, $otherOperator$) 的批准状态发生变化，则这些地址必须与调用者 ($owner$) 和指定的操作者 ($operator$) 匹配。任何对不同批准条目的更改都会导致此断言失败。
// no side effect
assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
    otherOwner    == owner &&
    otherOperator == operator
);

以下是 setApprovalForAll 规则的完整 CVL 规范：

methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

以下是 Prover 运行结果。

形式化验证 balanceOf(0) 回滚

以下规则验证 balanceOf 函数在查询零地址时总是回滚。

下面是 balanceOf 的合约实现。如果 $owner == address(0)$，它将回滚：

function balanceOf(address owner) public view virtual returns (uint256) {
    if (owner == address(0)) {
        revert ERC721InvalidOwner(address(0));

    }
    return _balances[owner];
}

以下是验证此行为的规则：

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

以下是 Prover 运行结果：

转账和批准的完整规范

以下是完整的规范和 Prover 运行结果。

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool)    envfree;

    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

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

  • 原文链接： rareskills.io/post/certo...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
RareSkills
RareSkills
https://www.rareskills.io/

RareSkills

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！