Move Prover(形式化验证)入门 + 安全最佳实践

日期: 2026-06-16 方向: Move / Sui 阶段: 第三阶段：安全审计 标签: #move-prover #formal-verification #specification #invariants #sui-security

---

今日目标

---

核心概念

1. 什么是形式化验证（Formal Verification）

形式化验证是用数学方法证明程序满足其规范（specification）。与传统测试不同，它不是检查有限个输入的输出是否正确，而是证明对所有可能的输入，程序都满足规范。

打个比方：

2. Move Prover 简介

Move Prover 是 Move 语言生态中的形式化验证工具。它基于 SMT求解器（Satisfiability Modulo Theories），可以自动证明 Move 模块满足用户编写的规范。

Move Prover 的工作流程：

Move 源代码 + Spec 规范
        ↓
   Move Prover 编译器
        ↓
   生成验证条件 (Verification Conditions)
        ↓
   SMT 求解器 (如 Z3/CVC5)
        ↓
   验证通过 ✓ / 发现违反 ✗ (给出反例)

重要说明：Move Prover 最初是为 Aptos Move（原 Diem/Libra）设计的。Sui Move 和 Aptos Move 有一些差异。Sui 生态目前更多依赖运行时安全（ownership/borrowing）和测试。下面的spec语法主要基于 Move 规范语言标准，部分语法在 Sui Move Prover 工具链中的支持程度可能有所不同，但概念是通用的。

3. 规范语言核心语法

Move 的规范语言嵌入在 spec 块中，主要有以下构造：

3.1 函数规范（Function Specification）

/// 函数规范写在 spec 块中
spec module {
    /// 前置条件：调用函数前必须满足的条件
    spec function_name {
        requires <condition>;    // 前置条件
        ensures <condition>;     // 后置条件
        aborts_if <condition>;   // 中止条件（什么情况下abort）
    }
}

requires（前置条件）

表示调用者必须保证的条件。如果前置条件不满足，验证器不会考虑这种情况。

spec transfer {
    // 调用者余额必须足够
    requires balance[sender] >= amount;
    // amount 必须为正数
    requires amount > 0;
}

ensures（后置条件）

表示函数执行完毕后必须满足的条件。old(expr) 引用函数执行前的值。

spec transfer {
    // 执行后，发送者余额减少了 amount
    ensures balance[sender] == old(balance[sender]) - amount;
    // 接收者余额增加了 amount
    ensures balance[receiver] == old(balance[receiver]) + amount;
}

aborts_if（中止条件）

表示函数在什么条件下会abort。Move Prover 可以验证函数是否恰好在这些条件下abort，不多也不少。

spec withdraw {
    // 当余额不足时会abort
    aborts_if balance[addr] < amount;
    // 隐含：当余额充足时，不会abort
}

3.2 数据不变量（Data Invariants）

不变量是在模块的整个生命周期中始终为真的属性。

spec module {
    // 全局不变量：totalSupply 始终等于所有余额之和
    invariant forall addr: address:
        sum(balances) == total_supply;

    // 结构体不变量：price 始终为正数
    invariant MyStruct.price > 0;
}

3.3 Schema（可复用的规范片段）

spec schema TransferSchema {
    sender: address;
    receiver: address;
    amount: u64;

    requires sender != receiver;
    requires amount > 0;
    ensures balance[sender] == old(balance[sender]) - amount;
}

spec transfer {
    include TransferSchema;
}

4. 形式化验证 vs 传统测试

最佳实践：三者结合使用。单元测试覆盖常见场景，fuzzing探索边界，形式化验证保证核心不变量。

---

代码实战

实战1：为Counter模块添加形式化规范

先回顾基础的Counter模块：

module counter::counter {
    use sui::object::{Self, UID};
    use sui::tx_context::TxContext;
    use sui::transfer;

    /// A simple counter object
    public struct Counter has key, store {
        id: UID,
        value: u64,
        owner: address,
    }

    /// Create a new counter with initial value 0
    public fun create(ctx: &mut TxContext): Counter {
        Counter {
            id: object::new(ctx),
            value: 0,
            owner: tx_context::sender(ctx),
        }
    }

    /// Increment the counter by 1
    public fun increment(counter: &mut Counter) {
        assert!(counter.value < 18446744073709551615, 0); // u64::MAX
        counter.value = counter.value + 1;
    }

    /// Decrement the counter by 1
    public fun decrement(counter: &mut Counter) {
        assert!(counter.value > 0, 1);
        counter.value = counter.value - 1;
    }

    /// Reset counter to 0
    public fun reset(counter: &mut Counter) {
        counter.value = 0;
    }

    /// Get the current value
    public fun value(counter: &Counter): u64 {
        counter.value
    }

    /// Increment by a custom amount
    public fun increment_by(counter: &mut Counter, amount: u64) {
        assert!(counter.value + amount >= counter.value, 2); // overflow check
        counter.value = counter.value + amount;
    }
}

现在为其添加形式化规范：

spec counter::counter {

    // ===== 函数规范 =====

    /// create: 确保新Counter初始值为0
    spec create {
        // 后置条件：创建的Counter value为0
        ensures result.value == 0;
    }

    /// increment: 确保值恰好增加1
    spec increment {
        // 当value已经是最大值时abort
        aborts_if counter.value == 18446744073709551615;
        // 执行后value恰好增加1
        ensures counter.value == old(counter.value) + 1;
        // owner不变
        ensures counter.owner == old(counter.owner);
    }

    /// decrement: 确保值恰好减少1
    spec decrement {
        // 当value为0时abort
        aborts_if counter.value == 0;
        // 执行后value恰好减少1
        ensures counter.value == old(counter.value) - 1;
        // owner不变
        ensures counter.owner == old(counter.owner);
    }

    /// reset: 确保值被设为0
    spec reset {
        // 永远不会abort
        aborts_if false;
        // 执行后value为0
        ensures counter.value == 0;
        // owner不变
        ensures counter.owner == old(counter.owner);
    }

    /// value: 纯读取函数
    spec value {
        aborts_if false;
        ensures result == counter.value;
    }

    /// increment_by: 确保值恰好增加amount
    spec increment_by {
        // 溢出时abort
        aborts_if counter.value + amount > 18446744073709551615;
        // 执行后value恰好增加amount
        ensures counter.value == old(counter.value) + amount;
        // owner不变
        ensures counter.owner == old(counter.owner);
    }

    // ===== 数据不变量 =====

    /// Counter的owner字段在创建后不应该被修改
    /// （这个不变量确保没有函数意外修改owner）
    invariant update Counter {
        old(self).owner == self.owner;
    }
}

实战2：Token模块的规范验证

更复杂的示例——为一个简化的Token模块添加规范：

module token::simple_token {
    use sui::object::{Self, UID};
    use sui::tx_context::TxContext;
    use sui::transfer;

    /// Token treasury (shared object)
    public struct Treasury has key {
        id: UID,
        total_supply: u64,
        max_supply: u64,
    }

    /// Individual token balance (owned object)
    public struct TokenBalance has key, store {
        id: UID,
        value: u64,
        owner: address,
    }

    const E_EXCEEDS_MAX_SUPPLY: u64 = 1;
    const E_INSUFFICIENT_BALANCE: u64 = 2;
    const E_ZERO_AMOUNT: u64 = 3;

    /// Initialize treasury
    public fun create_treasury(max_supply: u64, ctx: &mut TxContext): Treasury {
        assert!(max_supply > 0, E_ZERO_AMOUNT);
        Treasury {
            id: object::new(ctx),
            total_supply: 0,
            max_supply,
        }
    }

    /// Mint new tokens
    public fun mint(
        treasury: &mut Treasury,
        amount: u64,
        ctx: &mut TxContext,
    ): TokenBalance {
        assert!(amount > 0, E_ZERO_AMOUNT);
        assert!(treasury.total_supply + amount <= treasury.max_supply, E_EXCEEDS_MAX_SUPPLY);

        treasury.total_supply = treasury.total_supply + amount;

        TokenBalance {
            id: object::new(ctx),
            value: amount,
            owner: tx_context::sender(ctx),
        }
    }

    /// Burn tokens
    public fun burn(
        treasury: &mut Treasury,
        token: TokenBalance,
    ) {
        let TokenBalance { id, value, owner: _ } = token;
        object::delete(id);
        treasury.total_supply = treasury.total_supply - value;
    }

    /// Split tokens: take `amount` from `token`, return new TokenBalance
    public fun split(
        token: &mut TokenBalance,
        amount: u64,
        ctx: &mut TxContext,
    ): TokenBalance {
        assert!(amount > 0, E_ZERO_AMOUNT);
        assert!(token.value >= amount, E_INSUFFICIENT_BALANCE);

        token.value = token.value - amount;

        TokenBalance {
            id: object::new(ctx),
            value: amount,
            owner: token.owner,
        }
    }

    /// Merge two token balances
    public fun merge(
        token: &mut TokenBalance,
        other: TokenBalance,
    ) {
        let TokenBalance { id, value, owner: _ } = other;
        object::delete(id);
        token.value = token.value + value;
    }
}

/// 形式化规范
spec token::simple_token {

    // ===== 核心不变量 =====

    /// Treasury的total_supply永远不超过max_supply
    spec Treasury {
        invariant total_supply <= max_supply;
        invariant max_supply > 0;
    }

    // ===== 函数规范 =====

    spec create_treasury {
        aborts_if max_supply == 0;
        ensures result.total_supply == 0;
        ensures result.max_supply == max_supply;
    }

    spec mint {
        // 前置条件（隐含在aborts_if中）
        aborts_if amount == 0;
        aborts_if treasury.total_supply + amount > treasury.max_supply;

        // 后置条件
        ensures treasury.total_supply == old(treasury.total_supply) + amount;
        ensures result.value == amount;

        // max_supply 不被修改
        ensures treasury.max_supply == old(treasury.max_supply);
    }

    spec burn {
        // burn不应该abort（前提是token是有效的）
        // total_supply >= token.value 由不变量保证
        ensures treasury.total_supply == old(treasury.total_supply) - token.value;
        ensures treasury.max_supply == old(treasury.max_supply);
    }

    spec split {
        aborts_if amount == 0;
        aborts_if token.value < amount;

        // token的value减少了amount
        ensures token.value == old(token.value) - amount;
        // 返回的新token value正好是amount
        ensures result.value == amount;
        // 总量守恒
        ensures token.value + result.value == old(token.value);
    }

    spec merge {
        // merge后，token的value是两者之和
        ensures token.value == old(token.value) + other.value;
    }
}

这些规范可以验证几个重要属性：

1. Supply上限保证：total_supply <= max_supply 永远为真
2. Mint正确性：mint后total_supply恰好增加了amount
3. Burn正确性：burn后total_supply恰好减少了token.value
4. Split守恒：split后两个token的value之和等于原来的value
5. Merge守恒：merge后token的value等于两者之和

实战3：发现规范违反的例子

如果我们在 Counter 模块中故意引入一个bug：

/// 错误的increment实现
public fun increment(counter: &mut Counter) {
    counter.value = counter.value + 2; // bug: 加了2而不是1
}

spec increment {
    ensures counter.value == old(counter.value) + 1; // spec期望加1
}

Move Prover 会报告：

error: post-condition does not hold
   ┌─ counter.move:XX:9
   │
XX │         ensures counter.value == old(counter.value) + 1;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   = counter.value = 3, old(counter.value) = 1
   = (counterexample: counter.value was 1, after increment it became 3)

Prover 不仅告诉你规范被违反了，还给出了反例（counterexample），帮助定位bug。

---

Sui 安全最佳实践清单

对象安全

[x] Ownership 正确设置
    - 只有owner才能修改的object使用 `transfer::transfer`（私有传输）
    - 需要共享访问的object使用 `transfer::share_object`
    - 不可变数据使用 `transfer::freeze_object`

[x] 避免对象泄露
    - 确保所有创建的object都被转移(transfer)或销毁(delete)
    - 不要在函数中创建object但忘记处理（编译器会报错，但要理解原因）

[x] Shared Object 并发安全
    - Shared object的每次修改都通过Sui的共识机制排序
    - 但要注意read-then-write模式可能导致逻辑错误
    - 考虑使用 `&mut` 独占引用来保证操作的原子性

数值安全

[x] 整数溢出
    - Move的u64/u128/u256运算在溢出时自动abort
    - 但要注意乘法中间结果溢出：
      (a * b) / c 中如果 a * b 溢出，整个表达式abort
    - 使用 u128 或 u256 作为中间计算结果

[x] 除法截断
    - Move整数除法向下截断：7 / 2 = 3
    - 在费率计算中可能导致精度丢失
    - 考虑使用fixed-point math库
    - 先乘后除：(amount * rate) / PRECISION

[x] 零除检查
    - Move在除以零时自动abort
    - 但要给用户友好的错误信息，最好显式检查

权限控制

[x] Admin权限管理
    - 使用 AdminCap 模式（capability pattern）
    - AdminCap 只在 init 函数中创建一次
    - 考虑支持AdminCap转移（换管理员）

[x] 避免特权提升
    - 检查 public fun 是否暴露了不应该暴露的内部操作
    - struct 的 has key/store/copy/drop 能力要谨慎授予
    - store 能力意味着object可以被包装到其他object中

[x] Capability模式
    - 使用 Capability Objects（如 TreasuryCap、AdminCap）
    - 函数要求传入capability对象作为授权凭证
    - 这比address-based access control更安全

模块设计

[x] 最小暴露原则
    - 只 public 必要的函数
    - 内部辅助函数用 fun（不加public）
    - public(package) 用于同package内的跨模块调用

[x] 类型安全
    - 使用 Witness Pattern 确保模块唯一性
    - 使用 Hot Potato Pattern 强制调用顺序
    - 使用 phantom type 做编译期类型区分

[x] 升级安全
    - Move模块发布后可以升级（在Sui中）
    - 但要注意升级兼容性（不能删除/修改已有的public函数签名）
    - 使用 UpgradeCap 控制谁能升级

与外部交互

[x] Dynamic Fields 安全
    - 使用 dynamic_field 和 dynamic_object_field 时注意类型一致性
    - 从dynamic field取出的值类型要与存入时一致
    - 注意 dynamic field 的存在性检查

[x] Clock 和时间
    - 使用 sui::clock::Clock 获取链上时间
    - 注意时间精度（毫秒级）
    - 不要依赖精确的时间间隔

[x] 随机性
    - 链上没有真正的随机性
    - 不要用 tx_context 的 epoch/digest 作为随机源（可预测）
    - 使用 Sui 的 Random 模块（如果可用）或 VRF

---

关键要点总结

形式化验证的价值

1. 数学级别的保证：形式化验证可以证明"对所有输入"程序都满足规范，这是测试无法做到的
2. 发现隐蔽bug：通过spec和代码的对比，Prover可以发现人眼难以察觉的逻辑错误
3. 活文档：spec本身就是最精确的文档，描述了函数的完整行为契约

Move安全模型的独特优势

1. 资源线性性：Move的资源（object）不能被复制或隐式丢弃，从根本上消除了一类重要漏洞
2. 引用安全：借用检查器确保不会有悬垂引用或数据竞争
3. 类型安全：强类型系统 + 泛型约束，编译期就能捕获大量错误
4. Capability模式：权限控制通过对象传递而非address检查，更安全且可组合

Spec编写建议

---

常见误区

误区1："形式化验证能证明合约完全安全"

形式化验证只能证明代码满足规范（spec）。如果spec本身有误（比如spec漏掉了一个关键属性），Prover也检测不到。所以spec的编写质量至关重要。

正确说法是："形式化验证证明了代码和规范的一致性"。

误区2："Move不需要安全审计因为语言本身就安全"

Move消除了一些特定类型的漏洞（如重入、资源复制），但业务逻辑漏洞和经济模型缺陷仍然可能存在。比如：

• 价格计算公式错误
• 权限设计不合理
• 激励机制可被博弈

误区3："Sui的owned object不需要担心并发问题"

Owned object确实不会被并发修改（因为只有owner才能使用），但如果多个owned object之间有逻辑依赖关系，仍然可能出现一致性问题。例如，一个swap操作需要同时修改两个用户的TokenBalance。

误区4："把所有数据都放在shared object中最安全"

恰恰相反，shared object的性能较低（需要共识排序），且暴露了更大的攻击面。应该只在真正需要共享访问时才使用shared object，其他数据保持为owned object。

---

面试关联

Q1: "Move Prover是什么？它能解决什么问题？"

简短回答: Move Prover是一个形式化验证工具，它通过SMT求解器数学证明Move代码满足用户编写的规范（specification）。它能发现传统测试覆盖不到的逻辑错误。

详细回答: Move Prover将开发者编写的spec（requires/ensures/aborts_if/invariants）和Move代码一起编译成验证条件，交给Z3/CVC5等SMT求解器求解。如果求解器找到了反例（spec被违反的情况），就报告错误并给出反例。核心价值在于：对于金融逻辑中的关键不变量（如总供应量守恒、余额非负），可以获得数学级别的正确性保证。

Q2: "Move语言相比Solidity有哪些安全优势？"

回答: 三个核心优势：

1. 资源线性性：Move的对象不能被复制或隐式丢弃，从语言层面消除了重入攻击和资产复制漏洞
2. Capability-based权限：权限通过对象传递而非address检查，更不容易被绕过
3. 内置形式化验证：Move Prover是语言生态原生工具，Solidity没有同等级别的原生形式化验证

但Move也有劣势：生态和工具链不如Solidity成熟，开发者数量少，审计资源有限。

Q3: "在什么场景下你会使用形式化验证？"

回答: 形式化验证成本较高，我会在以下场景使用：

1. 核心金融逻辑：Token供应量守恒、借贷协议的利率计算、LP份额计算
2. 权限控制关键路径：Admin操作的约束、升级机制的安全性
3. 已知高风险区域：审计中发现的薄弱环节，用spec加固
4. 不变量验证：系统的核心不变量（如"总存入 >= 总借出"）

对于UI辅助函数、简单getter等低风险代码，传统测试就足够了。

---

参考资源