参数化规则介绍

Formal Verification with Certora

参数化规则介绍

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

最后更新于 2026 年 2 月 13 日

到目前为止，在前面的章节中，我们编写了规则来验证特定方法的行为及其对合约状态的影响。例如：

• 在 第 2 章 中，我们编写了一个规则来验证调用 increment() 会使 $count$ 的值增加 1。
• 在 第 3 章 中，我们编写了一个规则来检查对 increment() 和 decrement() 的顺序调用应导致 $count$ 值不变。

但如果我们想推理应适用于无论哪个函数被调用的属性，该怎么办？例如，考虑以下属性：

• 在一个简单的投票合约中，总票数应始终等于赞成票和反对票的总和。
• 在一个 ERC-20 合约 中，用户的余额绝不能超过代币的总供应量。

在本章中，我们将学习如何编写所谓的参数化规则——这些规则允许我们形式化验证预期在无论哪个函数被调用的情况下都成立的属性。

参数化规则介绍

在 CVL 中，一个标准规则通常检查 特定 函数调用后的状态转换。你通常使用以下模式定义允许的状态转换：

Copyrule any_general_rule{

  require <setup conditions>;

  mySpecificFunction(arg1, arg2);

  assert <expected outcome>;
}

一个参数化规则 的工作方式类似，但它概括了这个概念。参数化规则不是专注于一个 function(args)，而是验证一个属性在 任何函数 被 任何有效 参数 调用后都成立。

CVL 如何处理“任何函数，任何参数”

为了表达“ 任何函数，任何有效参数”这个概念，CVL 提供了两种特殊类型：

1. method: 代表你正在验证的合约中的 任何公共或外部函数。声明一个 method 类型的变量意味着该规则可以动态引用和执行合约中的 任何函数。
2. calldataarg: 代表函数调用的 参数。由于不同的函数需要不同的输入，calldataarg 确保为正在测试的任何函数 (method) 自动提供有效的参数。

参数化调用语法

这两种特殊类型允许我们创建所谓的 参数化调用，它使得规则能够使用以下语法访问和调用被验证合约的每个公共或外部方法：

Copyrule someParametricRule() {

    env e;

    method f;
    calldataarg args;

    f(e,args)

    //Any assert statement should go here
    assert <property_1>;
    assert <property_2>;
 }

f(e, args) 这一行被称为参数化调用。它允许我们测试合约中的所有公共或外部函数，而不是手动选择一个。它的工作原理如下：

• $f$ 代表合约中的 任何函数。这个变量确保每个函数都被逐一测试，而不是指定一个特定函数。
• $args$ 代表 一组有效的输入值。由于不同的函数有不同的参数，$args$ 确保为每个函数提供正确类型和数量的输入。
• $e$: 为函数调用模拟提供必要的环境上下文（如发送者地址、区块号）。

本质上，f(e, args); 这一行告诉 Certora Prover：“ 对于该合约中的每个函数 $f$ ，在模拟环境 $e$ 中，用有效参数 $args$ 执行它。”

通过在 f(e, args); 行 之后 放置 assert 语句，我们定义了在 任何 函数调用完成后必须普遍成立的属性。这使得参数化规则成为验证智能合约核心不变式和一般安全属性的理想选择。

识别 ERC-20 中的不变式

让我们将所学应用于形式化验证以下所示的 ERC-20 实现的一个不变式：

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

contract RareToken {
    uint8 public immutable decimals = 18;
    uint256 public immutable totalSupply;

    mapping(address => uint256) private balances;
    mapping(address => mapping(address => uint256)) private allowances;

    event Transfer(address indexed from, address indexed to, uint256 value);
    event Approval(address indexed owner, address indexed spender, uint256 value);

    constructor(uint256 _initialSupply) {
        require(_initialSupply > 0, "Invalid initial supply");

        totalSupply = _initialSupply * 10 ** uint256(decimals);
        balances[msg.sender] = totalSupply;

        emit Transfer(address(0), msg.sender, totalSupply);
    }

    function balanceOf(address account) public view returns (uint256) {
        return balances[account];
    }

    function transfer(address recipient, uint256 amount) public returns (bool) {
        require(recipient != address(0), "ERC20: transfer to zero address");
        require(balances[msg.sender] >= amount, "Insufficient balance");

        balances[msg.sender] -= amount;
        balances[recipient] += amount;
        emit Transfer(msg.sender, recipient, amount);
        return true;
    }

    function approve(address spender, uint256 amount) public returns (bool) {
        require(spender != address(0), "ERC20: approve to zero address");

        allowances[msg.sender][spender] = amount;
        emit Approval(msg.sender, spender, amount);
        return true;
    }

    function allowance(address owner_, address spender) public view returns (uint256) {
        return allowances[owner_][spender];
    }

    function transferFrom(
        address sender,
        address recipient,
        uint256 amount
    ) public returns (bool) {
        require(recipient != address(0), "ERC20: transfer to zero address");
        require(balances[sender] >= amount, "Insufficient balance");

        uint256 currentAllowance = allowances[sender][msg.sender];
        require(currentAllowance >= amount, "ERC20: insufficient allowance");

        if (currentAllowance != type(uint256).max) {
            allowances[sender][msg.sender] = currentAllowance - amount;
        }

        balances[sender] -= amount;
        balances[recipient] += amount;
        emit Transfer(sender, recipient, amount);
        return true;
    }
}

正如我们所学，编写参数化规则的目的是验证智能合约属性，这些属性应在不同的函数调用中始终成立。在我们的 RareToken 合约中，一个关键的不变式是：总供应量稳定性。

由于合约不包括 铸币或销毁 功能，总供应量在部署时初始化一次，并且在合约的整个生命周期内必须保持不变。换句话说，任何函数都不应修改 totalSupply() 返回的值。

让我们看看如何编写一个参数化规则来验证总供应量完整性。

形式化验证总供应量一致性

一旦我们确定了要验证的合约的关键不变式，请按照以下步骤编写 参数化规则：

1. 定义规则

使用 rule 关键字，后跟规则的描述性名称：

Copyrule totalSupplyIsConstant() { }

2. 声明执行环境

定义一个 env 变量来表示函数的执行环境：

Copyrule totalSupplyIsConstant() {
    env e;
}

3. 捕获调用前状态

由于我们需要比较函数执行前后 $totalSupply$ 的值，我们存储其初始状态：

Copyrule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);
}

4. 模拟函数执行

声明一个 method 变量来表示任何函数调用，并定义可能传入的 arguments：

Copyrule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args); // Execute the function call with the given arguments
}

5. 捕获调用后状态

执行函数后，我们将存储 $totalSupply$ 的更新值：

Copyrule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args);

    mathint afterSupply = totalSupply(e);
}

6. 强制执行总供应量一致性

在我们的 RareToken 合约中，我们希望确保 $totalSupply$ 变量在任何函数执行后都不应改变。我们使用 assert 语句 (assert beforeSupply == afterSupply) 来明确强制执行此条件：

Copyrule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args);

    mathint afterSupply = totalSupply(e);

    assert beforeSupply == afterSupply;
}

运行验证

要查看参数化规则的结果，请应用你在前面章节中学到的知识：将 RareToken 合约和相应的规范放入 Certora Prover 环境中。

设置完成后，启动验证过程。如果合约满足规则定义的所有条件，Certora Prover 将确认验证运行成功，没有检测到任何违规，如下图所示：

验证结果确认 RareToken 合约中的所有函数都已根据 totalSupplyIsConstant() 规则进行测试。每个函数旁边的绿色勾号 (✅) 表示该规则适用于所有可能的执行，确保 $totalSupply$ 变量在任何函数调用下保持不变。

理解参数化规则的范围

关于 参数化规则，一个重要的理解是它旨在一次只分析 一个函数调用 的影响。这意味着 Prover 不会检查一系列调用后发生的情况——它只关注对一个函数的 单个 调用以及该调用后合约状态的样子。

以下是 Prover 评估参数化规则时发生的情况：

1. 它从一个 初始合约状态 开始——这是任何函数被调用之前的状态。
2. 它从合约中选择 一个函数，并检查——在 给定前置条件 下——是否存在 任何有效输入 可能导致规则断言被违反。
3. 这个过程对合约中的 每个函数 重复。
4. 规则 仅当没有一个函数，在任何有效输入下，导致断言失败时 才通过验证 (✅)。

为了更清楚地理解参数化规则的评估过程，考虑 Counter 合约。它包含两个外部函数：increment()，它增加 $count$；以及 transferOwnership()，它更新 $owner$ 地址。所有权相关的功能仅仅是为了引入额外的函数，以便我们能够观察参数化规则在应用于各种函数类型时的行为。

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

contract Counter {
    uint256 public count;
    address public owner;

    // Define custom errors
    // 定义自定义错误
    error Unauthorized();
    error InvalidAddress();

    // Emit events for important state changes
    // 发出事件以记录重要的状态变化
    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);
    event CountUpdated(uint256 newCount);

    constructor() {
        owner = msg.sender;
        emit OwnershipTransferred(address(0), msg.sender);
    }

  modifier onlyOwner() {

        if (msg.sender != owner) revert Unauthorized();
        _;
    }

    function increment() external {
        count += 1;
        emit CountUpdated(count);
    }

    function transferOwnership(address _newOwner) external onlyOwner {
        if (_newOwner == address(0)) revert InvalidAddress();
        emit OwnershipTransferred(owner, _newOwner);
        owner = _newOwner;
    }
}

现在考虑下面定义了一个名为 counterParametricCall() 的参数化规则的规范。

Copyrule counterParametricCall() {
    env e;

    require count(e) == 0;

    method f;
    calldataarg args;

    f(e,args);

    satisfy count(e) == 2 ;
}

由于我们的规则 counterParametricCall() 包含 satisfy count(e) == 2; 语句，我们正在询问 Prover 是否存在 至少一种可能的方法可以达到 $count$ 为 $2$ 的状态，从 $count$ 为 $0$ 的初始状态开始。

但还有更多——规则还在 require 和 satisfy 语句之间包含一个 参数化函数调用 (f(e, args))。这使得问题从一个通用的可达性检查转向一个更集中的查询：

“是否存在 合约中的任何单个函数 f ，当它与一些有效参数 args__ 一起执行一次时，它能将状态直接从 count == 0 转换到 count == 2？”

在我们的 Counter 合约中，唯一可用的函数是 increment()，它每次调用将计数器增加 $1$。由于没有函数可以在单次执行中将计数器增加 $2$，Prover 无法找到满足条件 count(e) == 2 的任何函数。

因此，该规则将 验证失败，这是预期且正确的结果——如下图所示：

需要非常重要的是，参数化规则只分析 单个外部函数调用 的影响。它不检查一系列调用或单个交易中的复杂交互。例如，虽然上述规则证明没有单个调用能使 count == 2，但如果在同一交易中另一个智能合约 连续两次 调用 increment() 函数，则有可能达到 count == 2。这种情况涉及在单个交易中启动的 多个函数调用，这超出了本章的范围。

然而，即使我们将规则放宽为检查 satisfy count(e) == 1 而不是 satisfy count(e) == 2 ，该规则仍然不会通过，如下图所示：

发生这种情况是因为，在底层，当评估参数化规则时，Prover 会为合约中的每个函数创建一个规则实例。它会单独测试这些规则实例，对照断言进行检查。当且仅当每个函数实例都满足 assert 和 satisfy 语句指定的所有条件时，规则才通过验证。如果即使一个函数未能满足条件，整个规则也会失败。

在 Counter 合约中，只有 increment() 函数修改了 $count$ 变量，使其成为唯一可能满足 satisfy 条件（例如 count == 1）的候选者。相反，transferOwnership() 和 getter 函数 count() 和 owner() 完全不影响 $count$。当 Prover 为这些函数评估规则时，它发现它们都无法产生所需的状态变化。因此，它们的规则实例失败，并且由于所有实例都必须通过规则才能成功，所以整个规则验证失败。

总结

这就是我们如何使用 参数化规则 来验证预期在所有函数执行中都成立的智能合约属性。然而，在某些情况下，我们可能希望 将某些函数从规则中排除 或以不同的方式处理它们。在下一章中，我们将学习如何 微调参数化规则 以根据特定函数调用选择性地强制执行约束。

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

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