使用 Move Prover 验证 Aptos Vault 的正确性

Adevar labs
发布于 1天前
阅读 23

本文介绍了如何使用 Move Prover 对 Aptos 上的一个简单 APT Vault 进行形式化验证。通过形式化验证，可以数学方式证明代码的正确性，确保 Vault 在所有可能的输入情况下都满足预期的属性，例如防止重复初始化、拒绝零存款/取款、保持资产会计的正确性以及保持 Vault 状态的一致性。

## 为什么需要形式化验证？

传统的测试是基于示例的。你可能会测试存入 100 APT（Aptos 的原生代币）并提取 50 APT，但 **边缘** 情况呢，比如 u64::MAX，单个 **八进制** 的余额，或者 1,000 笔同时进行的 **提取**？

形式化验证尝试证明所有可能输入的属性：

```shell
传统测试: "我测试了 100 个案例" → 100/∞ 的信心

形式化验证: "验证器检查了所有（有界）路径" → 数学上的确定性
```

考虑到这种区别，让我们看看我们将要验证的具体系统。

## 我们要构建什么

我们将在 Aptos 上构建和验证一个简单的 APT **金库**。该 **金库** 允许用户：

- **存入 APT** \- 发送资产并接收成比例的份额
- **提取 APT** \- 销毁份额并接收成比例的资产

我们将使用形式化验证来证明以下属性：

- **金库** 只能初始化一次
- 存款需要 **大于零** 的金额和有效的 **金库** 状态
- **提取** 需要 **大于零** 的份额和有效的 **金库** 状态
- 资产随着存款增加，随着 **提取** 减少
- **金库** 状态在所有操作后保持一致

```shell
形式化规范:
- initialize(): 没有重复初始化，零初始余额
- deposit(): 有效的先决条件，资产增加
- withdraw(): 有效的先决条件，资产减少
- View function: 总是返回非负值
```

‍

## 安装 & 设置

### 安装 Aptos CLI

使用 Move Prover 需要 Aptos CLI。选择以下安装方法之一：

**选项 1: Homebrew (Mac - 推荐)**

```javascript
brew update
brew install aptos
aptos help
```

**选项 2: 安装脚本 (Mac/Linux)** ‍

使用 curl:

```shell
curl -fsSL "https://aptos.dev/scripts/install_cli.sh" | sh
aptos help
```

或者使用 wget:

```shell
wget -qO- "https://aptos.dev/scripts/install_cli.sh" | sh
aptos help
```

‍

### 安装 Move Prover 依赖

安装 Aptos CLI 后，使用单个命令安装 prover 依赖项：

```shell
aptos update prover-dependencies
```

这会自动安装 Boogie, Z3 和所有其他必需的依赖项。

### 验证一切正常

```shell
aptos move prove --help
```

你应该能看到 prover 的选项和用法信息。

### 初始化你的 Aptos 项目

```javascript
mkdir aptos-vault-prover
cd aptos-vault-prover
aptos move init --name vault_project
```

这会创建：

```javascript
aptos-vault-prover/
├── Move.toml
├── sources/
│   └── (你的 .move 文件)
└── tests/
    └── (你的测试文件)
```

‍

## **金库** 架构

在深入研究形式化规范之前，值得让我们自己扎根于 **金库** 的设计和会计模型中。

### 高级设计

![Screenshot 2026-01-02 at 11 05 36 AM](https://img.learnblockchain.cn/2026/01/16/696668157d0b0b469a2d0b8b_66e50909.png)

### 份额计算如何工作

**在存款时:**

```shell
IF first_deposit:
    shares_minted = amount (1:1 比例)
ELSE:
    shares_minted = (amount * total_shares) / total_assets
```

**在提取时:**

```javascript
amount_withdrawn = (shares * total_assets) / total_shares
```

这确保了比例保持不变：

```javascript
shares/assets before = shares/assets after
```

这种比例计算确保了 **金库** 资产在股东之间的公平分配。

‍

## **金库** 实现

让我们逐步构建 **金库**。创建 sources/vault.move:

```shell
module vault_project::vault {
    use std::signer;
    use std::option;
    use std::string;
    use aptos_framework::fungible_asset::{Self, Metadata, MintRef, TransferRef, BurnRef};
    use aptos_framework::object::{Self, Object};
    use aptos_framework::primary_fungible_store;
    use aptos_framework::coin::{Self, Coin};
    use aptos_framework::aptos_coin::AptosCoin;

/// 错误代码
    const E_NOT_INITIALIZED: u64 = 1;
    const E_ALREADY_INITIALIZED: u64 = 2;
    const E_INVALID_AMOUNT: u64 = 3;
    const E_INSUFFICIENT_SHARES: u64 = 4;
    const E_INSUFFICIENT_BALANCE: u64 = 5;

/// **金库** 配置 - 存储份额代币元数据和引用
    struct VaultConfig has key {
        mint_ref: MintRef,
        burn_ref: BurnRef,
        transfer_ref: TransferRef,
        metadata: Object<Metadata>,
    }

/// **金库** 金库 - 持有存入的 APT
    struct VaultTreasury has key {
        coins: Coin<AptosCoin>,
    }

/// 初始化 **金库** (一次性操作)
    public entry fun initialize(admin: &signer) {
        let admin_addr = signer::address_of(admin);
        assert!(!exists<VaultConfig>(admin_addr), E_ALREADY_INITIALIZED);

// 为 **金库** 份额创建同质化资产
        let constructor_ref = &object::create_named_object(admin, b"VAULT_SHARES");

primary_fungible_store::create_primary_store_enabled_fungible_asset(
            constructor_ref,
            option::none(),
            string::utf8(b"Vault Shares"),
            string::utf8(b"vAPT"),
            8,
            string::utf8(b"https://aptos.dev/icon.png"),
            string::utf8(b"https://aptos.dev"),
        );

// 生成用于铸造/销毁份额的引用
        let mint_ref = fungible_asset::generate_mint_ref(constructor_ref);
        let burn_ref = fungible_asset::generate_burn_ref(constructor_ref);
        let transfer_ref = fungible_asset::generate_transfer_ref(constructor_ref);
        let metadata = object::object_from_constructor_ref<Metadata>(constructor_ref);

// 存储 **金库** 配置
        move_to(admin, VaultConfig {
            mint_ref,
            burn_ref,
            transfer_ref,
            metadata,
        });

// 使用零余额 初始化金库
        move_to(admin, VaultTreasury {
            coins: coin::zero<AptosCoin>(),
        });
    }

/// 存入 APT，接收成比例的份额
    public entry fun deposit(user: &signer, amount: u64)
        acquires VaultConfig, VaultTreasury
    {
        assert!(amount > 0, E_INVALID_AMOUNT);

let vault_config = borrow_global_mut<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global_mut<VaultTreasury>(@vault_project);
        let user_addr = signer::address_of(user);

let total_assets = coin::value(&vault_treasury.coins);

// 计算要铸造的份额
        let shares_to_mint = if (total_assets == 0) {
            amount  // 首次存款：1:1 比例
        } else {
            let total_shares = fungible_asset::supply(vault_config.metadata);
            let total_shares_value = option::extract(&mut total_shares);
            (((amount as u128) * total_shares_value) / (total_assets as u128) as u64)
        };

// 将 APT 从用户转移到 **金库**
        let deposited_coins = coin::withdraw<AptosCoin>(user, amount);
        coin::merge(&mut vault_treasury.coins, deposited_coins);

// 将份额铸造给用户
        let shares = fungible_asset::mint(&vault_config.mint_ref, shares_to_mint);
        primary_fungible_store::deposit(user_addr, shares);
    }

/// 销毁份额， **提取** 成比例的 APT
    public entry fun withdraw(user: &signer, shares: u64)
        acquires VaultConfig, VaultTreasury
    {
        assert!(shares > 0, E_INVALID_AMOUNT);

let vault_config = borrow_global_mut<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global_mut<VaultTreasury>(@vault_project);
        let user_addr = signer::address_of(user);

// 验证用户是否有足够的份额
        let user_shares = primary_fungible_store::balance(user_addr, vault_config.metadata);
        assert!(user_shares >= shares, E_INSUFFICIENT_SHARES);

// 计算要 **提取** 的 APT
        let total_shares = fungible_asset::supply(vault_config.metadata);
        let total_shares_value = option::extract(&mut total_shares);
        let total_assets = coin::value(&vault_treasury.coins);
        let amount_to_withdraw = (((shares as u128) * (total_assets as u128)) / total_shares_value as u64);

assert!(total_assets >= amount_to_withdraw, E_INSUFFICIENT_BALANCE);

// 从用户那里销毁份额
        let shares_to_burn = primary_fungible_store::withdraw(user, vault_config.metadata, shares);
        fungible_asset::burn(&vault_config.burn_ref, shares_to_burn);

// 将 APT 转移给用户
        let withdrawn_coins = coin::extract(&mut vault_treasury.coins, amount_to_withdraw);
        coin::deposit(user_addr, withdrawn_coins);
    }

// View functions

#[view]
    public fun total_assets(): u64 acquires VaultTreasury {
        let vault_treasury = borrow_global<VaultTreasury>(@vault_project);
        coin::value(&vault_treasury.coins)
    }

#[view]
    public fun total_shares(): u128 acquires VaultConfig {
        let vault_config = borrow_global<VaultConfig>(@vault_project);
        let total_shares = fungible_asset::supply(vault_config.metadata);
        option::extract(&mut total_shares)
    }

#[view]
    public fun balance_of(user: address): u64 acquires VaultConfig {
        let vault_config = borrow_global<VaultConfig>(@vault_project);
        primary_fungible_store::balance(user, vault_config.metadata)
    }

#[view]
    public fun preview_deposit(amount: u64): u64 acquires VaultConfig, VaultTreasury {
        if (!exists<VaultConfig>(@vault_project)) {
            return amount
        };

let vault_config = borrow_global<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global<VaultTreasury>(@vault_project);
        let total_assets = coin::value(&vault_treasury.coins);

if (total_assets == 0) {
            amount
        } else {
            let total_shares = fungible_asset::supply(vault_config.metadata);
            let total_shares_value = option::extract(&mut total_shares);
            (((amount as u128) * total_shares_value) / (total_assets as u128) as u64)
        }
    }

#[view]
    public fun preview_withdraw(shares: u64): u64 acquires VaultConfig, VaultTreasury {
        if (!exists<VaultConfig>(@vault_project)) {
            return 0
        };

let vault_config = borrow_global<VaultConfig>(@vault_project);
        let vault_treasury = borrow_global<VaultTreasury>(@vault_project);
        let total_shares = fungible_asset::supply(vault_config.metadata);
        let total_shares_value = option::extract(&mut total_shares);
        let total_assets = coin::value(&vault_treasury.coins);

if (total_shares_value == 0) {
            0
        } else {
            (((shares as u128) * (total_assets as u128)) / total_shares_value as u64)
        }
    }
}
```

这是一个标准的 **金库** 实现。接下来重要的是不是它的外观，而是我们可以证明它的行为。

‍

## 编写形式化规范

Move 中的形式化规范使用 `spec` 关键字。可以将其视为验证器必须验证的 **合约**。

### 理解 pragma aborts_if_is_partial

在我们深入研究规范之前，你会在各处看到这个 **pragma**：

```javascript
spec function_name {
    pragma aborts_if_is_partial;
    // ... specifications
}
```

**它是什么意思？**

Aptos 框架很复杂。像 `coin::withdraw()` 或 `fungible_asset::mint()` 这样的函数在其调用堆栈深处有 **数十个** 可能的 **中断** 条件。指定每一个：

1.  **冗长** \- 每个函数数百行
2.  **脆弱** \- 在框架更新时中断
3.  **不必要** \- 大多数与框架内部结构有关，而不是你的业务逻辑

`pragma aborts_if_is_partial` 告诉验证器：“我正在指定 **我关心的** **中断** 条件（业务逻辑），信任框架的其余部分。”

‍

### 模块级别的 **不变量**

将其添加到你的 vault.move 文件的末尾：

```javascript
spec module {
    pragma aborts_if_is_partial;

/*
     * 这个模块使用形式化规范来证明:
     *
     * 1. 初始化安全性 - **金库** 只能初始化一次
     * 2. 状态一致性 - VaultConfig 和 VaultTreasury 一起存在
     * 3. 操作有效性 - 存款和 **提取** 需要有效的状态
     * 4. 资产核算 - 资产在存款时增加，在 **提取** 时减少
     * 5. 输入验证 - 拒绝零金额
     *
     * 这些规范验证这些属性适用于所有可能的输入和状态。
     */
}
```

这个 **注释** 记录了我们的形式化规范验证的属性。

### 函数级别的规范

现在让我们为每个函数添加规范。在模块级别规范之后添加这些：

#### **1\. 初始化规范**

```javascript
spec initialize {
    pragma aborts_if_is_partial;

let admin_addr = signer::address_of(admin);

// 先决条件：**金库** 必须尚未存在
    aborts_if exists<VaultConfig>(admin_addr);
    aborts_if exists<VaultTreasury>(admin_addr);

// 后置条件：使用零余额创建两个资源
    ensures exists<VaultConfig>(admin_addr);
    ensures exists<VaultTreasury>(admin_addr);
    ensures coin::value(global<VaultTreasury>(admin_addr).coins) == 0;
}
```

**这证明了：**

- 没有重复初始化（防止覆盖现有的 **金库**）
- VaultConfig 和 VaultTreasury 以原子方式创建
- **金库** 从零资产开始（对于首次存款逻辑很重要）

#### **2\. 存款规范**

```shell
spec deposit {
    pragma aborts_if_is_partial;

// 先决条件
    aborts_if !exists<VaultConfig>(@vault_project);
    aborts_if !exists<VaultTreasury>(@vault_project);
    aborts_if amount == 0;

// 后置条件
    ensures exists<VaultConfig>(@vault_project);
    ensures exists<VaultTreasury>(@vault_project);
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
            old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount;
}
```

**这证明了：**

- 无法存入未初始化的 **金库**
- 拒绝零存款
- 资产增加的金额与存款金额完全相同
- **金库** 状态保持有效

#### **3\. **提取** 规范**

```shell
spec withdraw {
    pragma aborts_if_is_partial;

let vault_treasury = global<VaultTreasury>(@vault_project);
    let total_assets_before = coin::value(vault_treasury.coins);

// 先决条件
    aborts_if !exists<VaultConfig>(@vault_project);
    aborts_if !exists<VaultTreasury>(@vault_project);
    aborts_if shares == 0;

// 后置条件：资产减少
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) <= total_assets_before;
    ensures exists<VaultConfig>(@vault_project);
    ensures exists<VaultTreasury>(@vault_project);
}
```

**这证明了：**

- 无法从未初始化的 **金库** 中 **提取**
- 拒绝零份额 **提取**
- 总资产减少（如果四舍五入，则保持不变）
- 维护 **金库** 的完整性

‍ **‍**

#### **4\. 查看函数规范**

```shell
spec balance_of {
    pragma aborts_if_is_partial;
    aborts_if !exists<VaultConfig>(@vault_project);
    ensures result >= 0;
}

spec preview_withdraw {
    pragma aborts_if_is_partial;
    aborts_if exists<VaultConfig>(@vault_project) && !exists<VaultTreasury>(@vault_project);
    ensures result >= 0;
}

spec total_assets {
    pragma aborts_if_is_partial;
    aborts_if !exists<VaultTreasury>(@vault_project);
    ensures result == coin::value(global<VaultTreasury>(@vault_project).coins);
}

spec total_shares {
    pragma aborts_if_is_partial;
    aborts_if !exists<VaultConfig>(@vault_project);
    ensures result >= 0;
}
```

有了规范，我们现在可以看到 Move Prover 实际上是如何验证它们的。

‍

### 验证流程

以下是运行 **验证器** 时发生的情况：

```javascript
vault.move → Move Compiler → Bytecode + Specs → Move Prover
                                                      ↓
                                                  Boogie IL
                                                      ↓
                                                  Z3 Solver
                                                 ↙     ↘            ↘
                                    [✓ SUCCESS]      [✗ FAILURE]    [TIMEOUT]
                               所有路径已验证  反例      未确定
```

**验证器**：

1.  将你的 Move 代码 **编译** 为字节码
2.  将规范 **转换** 为逻辑公式
3.  为所有执行路径 **生成** 验证条件
4.  **调用** Z3 以检查规范是否适用于所有可能的输入
5.  **报告** 成功或显示反例

**限制：** 在某些情况下，可能的输入和执行路径的搜索空间非常大。 发生这种情况时，**验证器** 可能需要运行很长时间，可能需要数天，数月甚至更长时间。

为了在实践中解决这个问题，我们设置了一个 **超时** 参数，该参数限制了允许 **验证器** 运行的时间。 这通常设置为几分钟或几小时，具体取决于复杂度。 如果在验证完成之前达到 **超时**，**验证器** 将停止，并且该属性标记为 **未确定**，这意味着它未被证明为真或假。

这是现实世界代码库中的常见情况。

‍

## 运行 Prover

#### 首先编译

```javascript
aptos move compile
```

这应该输出：

```shell
Compiling, may take a little while to download git dependencies...
正在编译，下载 git 依赖可能需要一段时间...
...
{
  "Result": "Success"
  "结果": "成功"
}
```

#### 运行验证

```javascript
aptos move prove
```

预期输出：

```shell
Proving vault_project::vault ...
正在验证 vault_project::vault ...
[INFO] preparing module 0x123::vault
[INFO] preparing module 0x123::vault
[信息] 准备模块 0x123::vault
[INFO] transforming bytecode
[信息] 转换字节码
[INFO] generating verification conditions
[信息] 生成验证条件
[INFO] 8 verification conditions
[信息] 8 个验证条件
[INFO] running solver (Z3)
[信息] 运行求解器 (Z3)
[INFO] 8 verification conditions proven
[信息] 8 个验证条件得到验证
SUCCESS
成功
```

**刚刚发生了什么？**

**验证器** 检查了你所有规范中的 **8 个验证条件**，并在数学上证明了它们。 这意味着对于 **每个可能的输入**，你的 **金库** 都会维护指定的属性。

只有当失败是可以理解的时，证明才有用，因此让我们看看规范错误时会发生什么：

### 如果验证失败

让我们故意破坏一些东西，看看失败是什么样的。 将 **存款** 规范更改为：

```shell
ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
        old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount + 1;
```

再次运行 aptos move prove：

```shell
error: post-condition does not hold
错误: 后置条件不成立
    ┌─ sources/vault.move:257:9
    ┌─ sources/vault.move:257:9
    │
257 │ ╭         ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
257 │ ╭         ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
258 │ │                 old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount + 1;
258 │ │                 old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount + 1;
    │ ╰───────────────────────────────────────────────────────────────────────────────────────────^
    │ ╰───────────────────────────────────────────────────────────────────────────────────────────^
    │
    =     at sources/vault.move:76: deposit
    =     at sources/vault.move:76: deposit
    =         user = signer{0x10000...}
    =         user = signer{0x10000...}
    =         amount = 2
    =         amount = 2
    =     at sources/vault.move:80: deposit
    =     at sources/vault.move:80: deposit
    =         vault_treasury = &vault::VaultTreasury{coins = coin::Coin{value = 0}}
    =         vault_treasury = &vault::VaultTreasury{coins = coin::Coin{value = 0}}
    ...
    ...
    =     Post-condition failed
    =     Post-condition failed
    =         amount = 2
    =         amount = 2
    =         old(total_assets) = 0
    =         old(total_assets) = 0
    =         new(total_assets) = 2  (not 3 as spec claims)
    =         new(total_assets) = 2  (not 3 as spec claims)
```

**验证器** 找到了一个反例，证明该规范是错误的 - 当将 2 APT 存入一个空的 **金库** 时，资产增加 2，而不是 3. 这证明了形式化验证的力量：它不仅仅说“测试失败”，它还显示了破坏你的声明的确切输入。

‍

## 经验证内容 vs 信任内容

### 显式验证 (你的规范)

1.  **资源存在** \- 函数需要已初始化的 **金库**
2.  **拒绝零值** \- 空存款/ **提取** 中止
3.  **状态一致性** \- 操作后资源一起存在
4.  **单调变化** \- 资产在存款时增加，在 **提取** 时减少
5.  **非负结果** \- 查看函数返回有效值

### 隐式信任 (框架)

1.  **算术安全** \- Move VM 防止溢出/下溢
2.  **代币有效性** \- 框架确保有足够的余额
3.  **份额核算** \- 同质化资产框架正确跟踪供应
4.  **所有权** \- 主要的存储操作尊重所有权

‍

**验证器** **假设框架是正确的**。 这是合理的，因为 Aptos 框架经过了大量 **审计** 并且本身经过了形式化验证。

‍

## 常见的规范模式

### 模式 1：状态先决条件

```shell
spec deposit {
    aborts_if !exists<VaultConfig>(@vault_project);
    aborts_if !exists<VaultTreasury>(@vault_project);
}
```

**用法：** 确保在操作之前存在所需的资源。

### 模式 2：输入验证

```shell
spec deposit {
    aborts_if amount == 0;
}
```

**用法：** 在规范级别拒绝无效输入。

### 模式 3：状态后置条件

```shell
spec initialize {
    ensures exists<VaultConfig>(admin_addr);
    ensures coin::value(global<VaultTreasury>(admin_addr).coins) == 0;
}
```

**用法：** 保证成功执行后的状态。

### 模式 4：单调属性

```shell
spec deposit {
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) >=
            old(coin::value(global<VaultTreasury>(@vault_project).coins));
}
```

‍ **用法：** 证明值仅以适当的方式增加/减少。

### 模式 5：精确更改

```shell
spec deposit {
    ensures coin::value(global<VaultTreasury>(@vault_project).coins) ==
            old(coin::value(global<VaultTreasury>(@vault_project).coins)) + amount;
}
```

**用法：** 证明精确的状态转换。

‍

## 调试失败的证明

当证明失败时，请按照以下过程操作：

### 步骤 1：读取错误

```shell
ERROR: post-condition does not hold
错误: 后置条件不成立
  ┌─ sources/vault.move:150:9
  ┌─ sources/vault.move:150:9
  │
150 │         ensures total_assets_after == total_assets_before + amount;
150 │         ensures total_assets_after == total_assets_before + amount;
  │         ^^^^^^ Post-condition failed
  │         ^^^^^^ Post-condition failed
```

告诉你哪个规范失败以及在哪里。

### 步骤 2：检查反例

```shell
Counterexample:
反例:
  amount = 0
  amount = 0
  total_assets_before = 100
  total_assets_before = 100
  total_assets_after = 100
  total_assets_after = 100
```

向你展示了破坏你的声明的确切输入。

‍

### 步骤 3：修复规范或代码

以下任一：

- 如果你的声明太强，则 **修复规范**
- 如果存在实际错误，则 **修复代码**

在这种情况下，我们忘记指定 `aborts_if amount == 0`，因此 **验证器** 找到了一个后置条件不成立的案例。

‍

### 步骤 4：重新验证

```javascript
aptos move prove
```

重复直到所有证明都通过。

‍

## 性能提示

### 1\. 使用 **pragma** **aborts_if_is_partial**

不要试图指定每个框架 **终止** 条件。

‍

### 2\. 保持规范重点突出

指定对你的业务逻辑有意义的内容：

```shell
// Good: Focused on business logic
// 好的: 专注于业务逻辑
spec deposit {
    aborts_if amount == 0;
    aborts_if amount == 0;
    ensures vault_balance_increases;
    ensures vault_balance_increases;
}

// Bad: Over-specifying framework details
// 坏: 过度指定框架细节
spec deposit {
    aborts_if !coin::is_account_registered<AptosCoin>(user);
    aborts_if !coin::is_account_registered<AptosCoin>(user);
    aborts_if coin::balance<AptosCoin>(user) < amount;
    aborts_if coin::balance<AptosCoin>(user) < amount;
    aborts_if !exists<CoinStore<AptosCoin>>(user);
    aborts_if !exists<CoinStore<AptosCoin>>(user);
    // ... 20 more framework conditions
    // ... 20 多个框架条件
}
```

‍

### 3\. 分离复杂逻辑

如果验证速度慢，请考虑将复杂逻辑提取到具有自己规范的 **辅助** 函数。

‍

### 4\. 对框架信任使用 assume

```shell
spec helper_function {
    // Trust framework guarantee
    // 信任框架保证
    assume fungible_asset::supply(metadata) >= 0;
    assume fungible_asset::supply(metadata) >= 0;

// Prove your logic
    // 证明你的逻辑
    ensures result == compute_shares(amount);
    ensures result == compute_shares(amount);
}
```

## 结论

形式化验证将 “我认为这有效” 转化为 “我可以证明这有效”。 Move Prover 为你提供编译时数学保证，你的 **金库**：

1.  只能初始化一次
2.  拒绝零存款/ **提取**
3.  维护正确的资产核算
4.  保持 **金库** 状态一致性
5.  在操作前验证所有先决条件

这是之间的区别：

```shell
"我们测试了 1000 个场景" → 1000/∞ 的置信度
"我们测试了 1000 个场景" → 1000/∞ 的置信度
"验证器验证了所有路径" → ∞/∞ 的置信度
"验证器验证了所有路径" → ∞/∞ 的置信度
```

‍

对于处理数百万 TVL 的生产 DeFi 协议，这种级别的保证并非可选项，而是必不可少的。 形式化验证不会取代测试； 它通过证明测试只能抽样的属性来补充它。

与任何测试方法一样，形式化验证都有其局限性，我们上面简要地介绍了这些局限性（例如，使属性未确定的 **超时**）。 还有另一个重要的限制：形式化验证仅证明 **声明** 的特定属性列表是否成立。 开发人员或审计员可能会遗漏其他重要属性，而这些属性未经过验证。 这些遗漏的属性正是攻击者倾向于利用的属性。

我们已经看到一些跨越各种生态系统的 DeFi 协议，它们经过了“形式化验证” 并且仍然被黑客入侵。 在事后分析中，一旦确定并写下了缺少的属性，形式化验证器就会正确地标记出漏洞。

因此，在对形式化验证做出强烈声明时要小心。 它 **不能** 证明不存在错误 - 这需要验证关于给定程序的 **每个可能的** 属性，这对于大多数真实世界的系统来说是不切实际的。

如果你来自 EVM 或 Solana 背景，并且想从概念上了解基于 Move 的系统如何处理安全性和正确性，那么这篇相关文章可能会有所帮助：

**EVM 和 SVM 开发人员的 Sui Move：第 1 部分 - 思维模型** [https://www.adevarlabs.com/blog/sui-move-for-evm-and-svm-developers-part-1-mental-models](https://learnblockchain.cn/article/21403)

我们根据实际审计工作和实际协议分析发布了类似的实用、高信号深度剖析。 如果你正在构建接近底层的东西并关心其正确性，请在 X 和 LinkedIn 上关注 Adevar Labs，以获取有关 Move、Rust 和智能合约安全的文章。

‍

### **安全发布。**

‍

### 参考文献

- [Aptos Move Prover 指南](https://aptos.dev/en/build/smart-contracts/prover)
- [Move 规范语言](https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md)
- [Boogie 文档](https://boogie-docs.readthedocs.io/)
- [Z3 定理证明器](https://github.com/Z3Prover/z3)

>- 原文链接： [adevarlabs.com/blog/prov...](https://www.adevarlabs.com/blog/proving-an-aptos-vault-correct-with-the-move-prover)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

为什么需要形式化验证？

传统的测试是基于示例的。你可能会测试存入 100 APT（Aptos 的原生代币）并提取 50 APT，但边缘情况呢，比如 u64::MAX，单个 八进制 的余额，或者 1,000 笔同时进行的提取？

形式化验证尝试证明所有可能输入的属性：

传统测试: "我测试了 100 个案例" → 100/∞ 的信心

形式化验证: "验证器检查了所有（有界）路径" → 数学上的确定性

考虑到这种区别，让我们看看我们将要验证的具体系统。

我们要构建什么

我们将在 Aptos 上构建和验证一个简单的 APT 金库。该金库允许用户：

存入 APT - 发送资产并接收成比例的份额
提取 APT - 销毁份额并接收成比例的资产

我们将使用形式化验证来证明以下属性：

金库只能初始化一次
存款需要 大于零 的金额和有效的金库状态
提取需要 大于零 的份额和有效的金库状态
资产随着存款增加，随着提取减少
金库状态在所有操作后保持一致

形式化规范:
- initialize(): 没有重复初始化，零初始余额
- deposit(): 有效的先决条件，资产增加
- withdraw(): 有效的先决条件，资产减少
- View function: 总是返回非负值

‍

安装 & 设置

安装 Aptos CLI

使用 Move Prover 需要 Aptos CLI。选择以下安装方法之一：

选项 1: Homebrew (Mac - 推荐)

brew update
brew install aptos
aptos help

选项 2: 安装脚本 (Mac/Linux) ‍

使用 curl:

curl -fsSL "https://aptos.dev/scripts/install_cli.sh" | sh
aptos help

或者使用 wget:

wget -qO- "https://aptos.dev/scripts/install_cli.sh" | sh
aptos help

‍

安装 Move Prover 依赖

安装 Aptos CLI 后，使用单个命令安装 prover 依赖项：

aptos update prover-dependencies

这会自动安装 Boogie, Z3 和所有其他必需的依赖项。

验证一切正常

aptos move prove --help

你应该能看到 prover 的选项和用法信息。

初始化你的 Aptos 项目

mkdir aptos-vault-prover
cd aptos-vault-prover
aptos move init --name vault_project

这会创建：

aptos-vault-prover/
├── Move.toml
├── sources/
│   └── (你的 .move 文件)
└── tests/
    └── (你的测试文件)

‍

金库架构

在深入研究形式化规范之前，值得让我们自己扎根于金库的设计和会计模型中。

高级设计

份额计算如何工作

在存款时:

IF first_deposit:
    shares_minted = amount (1:1 比例)
ELSE:
    shares_minted = (amount * total_shares) / total_assets

在提取时:

amount_withdrawn = (shares * total_assets) / total_shares

这确保了比例保持不变：

shares/assets before = shares/assets after

这种比例计算确保了金库资产在股东之间的公平分配。

‍

金库实现

让我们逐步构建金库。创建 sources/vault.move:

module vault_project::vault {
    use std::signer;
    use std::option;
    use std::string;
    use aptos_framework::fungible_asset::{Self, Metadata, MintRef, TransferRef, BurnRef};
    use aptos_framework::object::{Self, Object};
    use aptos_framework::primary_fungible_store;
    use aptos_framework::coin::{Self, Coin};
    use aptos_framework::aptos_coin::AptosCoin;

    /// 错误代码
    const E_NOT_INITIALIZED: u64 = 1;
    const E_ALREADY_INITIALIZED: u64 = 2;
    const E_INVALID_AMOUNT: u64 = 3;
    const E_INSUFFICIENT_SHARES: u64 = 4;
    const E_INSUFFICIENT_BALANCE: u64 = 5;

    /// **金库** 配置 - 存储份额代币元数据和引用
    struct VaultConfig has key {
        mint_ref: MintRef,
        burn_ref: BurnRef,
        transfer_ref: TransferRef,
        metadata: Object&lt;Metadata>,
    }

    /// **金库** 金库 - 持有存入的 APT
    struct VaultTreasury has key {
        coins: Coin&lt;AptosCoin>,
    }

    /// 初始化 **金库** (一次性操作)
    public entry fun initialize(admin: &signer) {
        let admin_addr = signer::address_of(admin);
        assert!(!exists&lt;VaultConfig>(admin_addr), E_ALREADY_INITIALIZED);

        // 为 **金库** 份额创建同质化资产
        let constructor_ref = &object::create_named_object(admin, b"VAULT_SHARES");

        primary_fungible_store::create_primary_store_enabled_fungible_asset(
            constructor_ref,
            option::none(),
            string::utf8(b"Vault Shares"),
            string::utf8(b"vAPT"),
            8,
            string::utf8(b"https://aptos.dev/icon.png"),
            string::utf8(b"https://aptos.dev"),
        );

        // 生成用于铸造/销毁份额的引用
        let mint_ref = fungible_asset::generate_mint_ref(constructor_ref);
        let burn_ref = fungible_asset::generate_burn_ref(constructor_ref);
        let transfer_ref = fungible_asset::generate_transfer_ref(constructor_ref);
        let metadata = object::object_from_constructor_ref&lt;Metadata>(constructor_ref);

        // 存储 **金库** 配置
        move_to(admin, VaultConfig {
            mint_ref,
            burn_ref,
            transfer_ref,
            metadata,
        });

        // 使用零余额 初始化金库
        move_to(admin, VaultTreasury {
            coins: coin::zero&lt;AptosCoin>(),
        });
    }

    /// 存入 APT，接收成比例的份额
    public entry fun deposit(user: &signer, amount: u64)
        acquires VaultConfig, VaultTreasury
    {
        assert!(amount > 0, E_INVALID_AMOUNT);

        let vault_config = borrow_global_mut&lt;VaultConfig>(@vault_project);
        let vault_treasury = borrow_global_mut&lt;VaultTreasury>(@vault_project);
        let user_addr = signer::address_of(user);

        let total_assets = coin::value(&vault_treasury.coins);

        // 计算要铸造的份额
        let shares_to_mint = if (total_assets == 0) {
            amount  // 首次存款：1:1 比例
        } else {
            let total_shares = fungible_asset::supply(vault_config.metadata);
            let total_shares_value = option::extract(&mut total_shares);
            (((amount as u128) * total_shares_value) / (total_assets as u128) as u64)
        };

        // 将 APT 从用户转移到 **金库**
        let deposited_coins = coin::withdraw&lt;AptosCoin>(user, amount);
        coin::merge(&mut vault_treasury.coins, deposited_coins);

        // 将份额铸造给用户
        let shares = fungible_asset::mint(&vault_config.mint_ref, shares_to_mint);
        primary_fungible_store::deposit(user_addr, shares);
    }

    /// 销毁份额， **提取** 成比例的 APT
    public entry fun withdraw(user: &signer, shares: u64)
        acquires VaultConfig, VaultTreasury
    {
        assert!(shares > 0, E_INVALID_AMOUNT);

        let vault_config = borrow_global_mut&lt;VaultConfig>(@vault_project);
        let vault_treasury = borrow_global_mut&lt;VaultTreasury>(@vault_project);
        let user_addr = signer::address_of(user);

        // 验证用户是否有足够的份额
        let user_shares = primary_fungible_store::balance(user_addr, vault_config.metadata);
        assert!(user_shares >= shares, E_INSUFFICIENT_SHARES);

        // 计算要 **提取** 的 APT
        let total_shares = fungible_asset::supply(vault_config.metadata);
        let total_shares_value = option::extract(&mut total_shares);
        let total_assets = coin::value(&vault_treasury.coins);
        let amount_to_withdraw = (((shares as u128) * (total_assets as u128)) / total_shares_value as u64);

        assert!(total_assets >= amount_to_withdraw, E_INSUFFICIENT_BALANCE);

        // 从用户那里销毁份额
        let shares_to_burn = primary_fungible_store::withdraw(user, vault_config.metadata, shares);
        fungible_asset::burn(&vault_config.burn_ref, shares_to_burn);

        // 将 APT 转移给用户
        let withdrawn_coins = coin::extract(&mut vault_treasury.coins, amount_to_withdraw);
        coin::deposit(user_addr, withdrawn_coins);
    }

    // View functions

    #[view]
    public fun total_assets(): u64 acquires VaultTreasury {
        let vault_treasury = borrow_global&lt;VaultTreasury>(@vault_project);
        coin::value(&vault_treasury.coins)
    }

    #[view]
    public fun total_shares(): u128 acquires VaultConfig {
        let vault_config = borrow_global&lt;VaultConfig>(@vault_project);
        let total_shares = fungible_asset::supply(vault_config.metadata);
        option::extract(&mut total_shares)
    }

    #[view]
    public fun balance_of(user: address): u64 acquires VaultConfig {
        let vault_config = borrow_global&lt;VaultConfig>(@vault_project);
        primary_fungible_store::balance(user, vault_config.metadata)
    }

    #[view]
    public fun preview_deposit(amount: u64): u64 acquires VaultConfig, VaultTreasury {
        if (!exists&lt;VaultConfig>(@vault_project)) {
            return amount
        };

        let vault_config = borrow_global&lt;VaultConfig>(@vault_project);
        let vault_treasury = borrow_global&lt;VaultTreasury>(@vault_project);
        let total_assets = coin::value(&vault_treasury.coins);

        if (total_assets == 0) {
            amount
        } else {
            let total_shares = fungible_asset::supply(vault_config.metadata);
            let total_shares_value = option::extract(&mut total_shares);
            (((amount as u128) * total_shares_value) / (total_assets as u128) as u64)
        }
    }

    #[view]
    public fun preview_withdraw(shares: u64): u64 acquires VaultConfig, VaultTreasury {
        if (!exists&lt;VaultConfig>(@vault_project)) {
            return 0
        };

        let vault_config = borrow_global&lt;VaultConfig>(@vault_project);
        let vault_treasury = borrow_global&lt;VaultTreasury>(@vault_project);
        let total_shares = fungible_asset::supply(vault_config.metadata);
        let total_shares_value = option::extract(&mut total_shares);
        let total_assets = coin::value(&vault_treasury.coins);

        if (total_shares_value == 0) {
            0
        } else {
            (((shares as u128) * (total_assets as u128)) / total_shares_value as u64)
        }
    }
}

这是一个标准的金库实现。接下来重要的是不是它的外观，而是我们可以证明它的行为。

‍

编写形式化规范

Move 中的形式化规范使用 spec 关键字。可以将其视为验证器必须验证的合约。

理解 pragma aborts_if_is_partial

在我们深入研究规范之前，你会在各处看到这个 pragma：

spec function_name {
    pragma aborts_if_is_partial;
    // ... specifications
}

它是什么意思？

Aptos 框架很复杂。像 coin::withdraw() 或 fungible_asset::mint() 这样的函数在其调用堆栈深处有 数十个 可能的中断条件。指定每一个：

冗长 - 每个函数数百行
脆弱 - 在框架更新时中断
不必要 - 大多数与框架内部结构有关，而不是你的业务逻辑

pragma aborts_if_is_partial 告诉验证器：“我正在指定 我关心的 中断条件（业务逻辑），信任框架的其余部分。”

‍

模块级别的不变量

将其添加到你的 vault.move 文件的末尾：

spec module {
    pragma aborts_if_is_partial;

    /*
     * 这个模块使用形式化规范来证明:
     *
     * 1. 初始化安全性 - **金库** 只能初始化一次
     * 2. 状态一致性 - VaultConfig 和 VaultTreasury 一起存在
     * 3. 操作有效性 - 存款和 **提取** 需要有效的状态
     * 4. 资产核算 - 资产在存款时增加，在 **提取** 时减少
     * 5. 输入验证 - 拒绝零金额
     *
     * 这些规范验证这些属性适用于所有可能的输入和状态。
     */
}

这个注释记录了我们的形式化规范验证的属性。

函数级别的规范

现在让我们为每个函数添加规范。在模块级别规范之后添加这些：

1. 初始化规范

spec initialize {
    pragma aborts_if_is_partial;

    let admin_addr = signer::address_of(admin);

    // 先决条件：**金库** 必须尚未存在
    aborts_if exists&lt;VaultConfig>(admin_addr);
    aborts_if exists&lt;VaultTreasury>(admin_addr);

    // 后置条件：使用零余额创建两个资源
    ensures exists&lt;VaultConfig>(admin_addr);
    ensures exists&lt;VaultTreasury>(admin_addr);
    ensures coin::value(global&lt;VaultTreasury>(admin_addr).coins) == 0;
}

这证明了：

没有重复初始化（防止覆盖现有的金库）
VaultConfig 和 VaultTreasury 以原子方式创建
金库从零资产开始（对于首次存款逻辑很重要）

2. 存款规范

spec deposit {
    pragma aborts_if_is_partial;

    // 先决条件
    aborts_if !exists&lt;VaultConfig>(@vault_project);
    aborts_if !exists&lt;VaultTreasury>(@vault_project);
    aborts_if amount == 0;

    // 后置条件
    ensures exists&lt;VaultConfig>(@vault_project);
    ensures exists&lt;VaultTreasury>(@vault_project);
    ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) ==
            old(coin::value(global&lt;VaultTreasury>(@vault_project).coins)) + amount;
}

这证明了：

无法存入未初始化的金库
拒绝零存款
资产增加的金额与存款金额完全相同
金库状态保持有效

3. 提取规范

spec withdraw {
    pragma aborts_if_is_partial;

    let vault_treasury = global&lt;VaultTreasury>(@vault_project);
    let total_assets_before = coin::value(vault_treasury.coins);

    // 先决条件
    aborts_if !exists&lt;VaultConfig>(@vault_project);
    aborts_if !exists&lt;VaultTreasury>(@vault_project);
    aborts_if shares == 0;

    // 后置条件：资产减少
    ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) &lt;= total_assets_before;
    ensures exists&lt;VaultConfig>(@vault_project);
    ensures exists&lt;VaultTreasury>(@vault_project);
}

这证明了：

无法从未初始化的金库中提取
拒绝零份额提取
总资产减少（如果四舍五入，则保持不变）
维护金库的完整性

‍ ‍

4. 查看函数规范

spec balance_of {
    pragma aborts_if_is_partial;
    aborts_if !exists&lt;VaultConfig>(@vault_project);
    ensures result >= 0;
}

spec preview_withdraw {
    pragma aborts_if_is_partial;
    aborts_if exists&lt;VaultConfig>(@vault_project) && !exists&lt;VaultTreasury>(@vault_project);
    ensures result >= 0;
}

spec total_assets {
    pragma aborts_if_is_partial;
    aborts_if !exists&lt;VaultTreasury>(@vault_project);
    ensures result == coin::value(global&lt;VaultTreasury>(@vault_project).coins);
}

spec total_shares {
    pragma aborts_if_is_partial;
    aborts_if !exists&lt;VaultConfig>(@vault_project);
    ensures result >= 0;
}

有了规范，我们现在可以看到 Move Prover 实际上是如何验证它们的。

‍

验证流程

以下是运行 验证器 时发生的情况：

vault.move → Move Compiler → Bytecode + Specs → Move Prover
                                                      ↓
                                                  Boogie IL
                                                      ↓
                                                  Z3 Solver
                                                 ↙     ↘            ↘
                                    [✓ SUCCESS]      [✗ FAILURE]    [TIMEOUT]
                               所有路径已验证  反例      未确定

验证器：

将你的 Move 代码编译为字节码
将规范转换为逻辑公式
为所有执行路径生成验证条件
调用 Z3 以检查规范是否适用于所有可能的输入
报告成功或显示反例

限制： 在某些情况下，可能的输入和执行路径的搜索空间非常大。发生这种情况时，验证器 可能需要运行很长时间，可能需要数天，数月甚至更长时间。

为了在实践中解决这个问题，我们设置了一个超时参数，该参数限制了允许 验证器 运行的时间。这通常设置为几分钟或几小时，具体取决于复杂度。如果在验证完成之前达到超时，验证器 将停止，并且该属性标记为 未确定，这意味着它未被证明为真或假。

这是现实世界代码库中的常见情况。

‍

运行 Prover

首先编译

aptos move compile

这应该输出：

Compiling, may take a little while to download git dependencies...
正在编译，下载 git 依赖可能需要一段时间...
...
{
  "Result": "Success"
  "结果": "成功"
}

运行验证

aptos move prove

预期输出：

Proving vault_project::vault ...
正在验证 vault_project::vault ...
[INFO] preparing module 0x123::vault
[INFO] preparing module 0x123::vault
[信息] 准备模块 0x123::vault
[INFO] transforming bytecode
[信息] 转换字节码
[INFO] generating verification conditions
[信息] 生成验证条件
[INFO] 8 verification conditions
[信息] 8 个验证条件
[INFO] running solver (Z3)
[信息] 运行求解器 (Z3)
[INFO] 8 verification conditions proven
[信息] 8 个验证条件得到验证
SUCCESS
成功

刚刚发生了什么？

验证器 检查了你所有规范中的 8 个验证条件，并在数学上证明了它们。这意味着对于 每个可能的输入，你的金库都会维护指定的属性。

只有当失败是可以理解的时，证明才有用，因此让我们看看规范错误时会发生什么：

如果验证失败

让我们故意破坏一些东西，看看失败是什么样的。将存款规范更改为：

ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) ==
        old(coin::value(global&lt;VaultTreasury>(@vault_project).coins)) + amount + 1;

再次运行 aptos move prove：

error: post-condition does not hold
错误: 后置条件不成立
    ┌─ sources/vault.move:257:9
    ┌─ sources/vault.move:257:9
    │
257 │ ╭         ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) ==
257 │ ╭         ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) ==
258 │ │                 old(coin::value(global&lt;VaultTreasury>(@vault_project).coins)) + amount + 1;
258 │ │                 old(coin::value(global&lt;VaultTreasury>(@vault_project).coins)) + amount + 1;
    │ ╰───────────────────────────────────────────────────────────────────────────────────────────^
    │ ╰───────────────────────────────────────────────────────────────────────────────────────────^
    │
    =     at sources/vault.move:76: deposit
    =     at sources/vault.move:76: deposit
    =         user = signer{0x10000...}
    =         user = signer{0x10000...}
    =         amount = 2
    =         amount = 2
    =     at sources/vault.move:80: deposit
    =     at sources/vault.move:80: deposit
    =         vault_treasury = &vault::VaultTreasury{coins = coin::Coin{value = 0}}
    =         vault_treasury = &vault::VaultTreasury{coins = coin::Coin{value = 0}}
    ...
    ...
    =     Post-condition failed
    =     Post-condition failed
    =         amount = 2
    =         amount = 2
    =         old(total_assets) = 0
    =         old(total_assets) = 0
    =         new(total_assets) = 2  (not 3 as spec claims)
    =         new(total_assets) = 2  (not 3 as spec claims)

验证器 找到了一个反例，证明该规范是错误的 - 当将 2 APT 存入一个空的金库时，资产增加 2，而不是 3. 这证明了形式化验证的力量：它不仅仅说“测试失败”，它还显示了破坏你的声明的确切输入。

‍

经验证内容 vs 信任内容

显式验证 (你的规范)

资源存在 - 函数需要已初始化的金库
拒绝零值 - 空存款/ 提取中止
状态一致性 - 操作后资源一起存在
单调变化 - 资产在存款时增加，在提取时减少
非负结果 - 查看函数返回有效值

隐式信任 (框架)

算术安全 - Move VM 防止溢出/下溢
代币有效性 - 框架确保有足够的余额
份额核算 - 同质化资产框架正确跟踪供应
所有权 - 主要的存储操作尊重所有权

‍

验证器 假设框架是正确的。这是合理的，因为 Aptos 框架经过了大量审计并且本身经过了形式化验证。

‍

常见的规范模式

模式 1：状态先决条件

spec deposit {
    aborts_if !exists&lt;VaultConfig>(@vault_project);
    aborts_if !exists&lt;VaultTreasury>(@vault_project);
}

用法： 确保在操作之前存在所需的资源。

模式 2：输入验证

spec deposit {
    aborts_if amount == 0;
}

用法： 在规范级别拒绝无效输入。

模式 3：状态后置条件

spec initialize {
    ensures exists&lt;VaultConfig>(admin_addr);
    ensures coin::value(global&lt;VaultTreasury>(admin_addr).coins) == 0;
}

用法： 保证成功执行后的状态。

模式 4：单调属性

spec deposit {
    ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) >=
            old(coin::value(global&lt;VaultTreasury>(@vault_project).coins));
}

‍ 用法： 证明值仅以适当的方式增加/减少。

模式 5：精确更改

spec deposit {
    ensures coin::value(global&lt;VaultTreasury>(@vault_project).coins) ==
            old(coin::value(global&lt;VaultTreasury>(@vault_project).coins)) + amount;
}

用法： 证明精确的状态转换。

‍

调试失败的证明

当证明失败时，请按照以下过程操作：

步骤 1：读取错误

ERROR: post-condition does not hold
错误: 后置条件不成立
  ┌─ sources/vault.move:150:9
  ┌─ sources/vault.move:150:9
  │
150 │         ensures total_assets_after == total_assets_before + amount;
150 │         ensures total_assets_after == total_assets_before + amount;
  │         ^^^^^^ Post-condition failed
  │         ^^^^^^ Post-condition failed

告诉你哪个规范失败以及在哪里。

步骤 2：检查反例

Counterexample:
反例:
  amount = 0
  amount = 0
  total_assets_before = 100
  total_assets_before = 100
  total_assets_after = 100
  total_assets_after = 100

向你展示了破坏你的声明的确切输入。

‍

步骤 3：修复规范或代码

以下任一：

如果你的声明太强，则 修复规范
如果存在实际错误，则 修复代码

在这种情况下，我们忘记指定 aborts_if amount == 0，因此 验证器 找到了一个后置条件不成立的案例。

‍

步骤 4：重新验证

aptos move prove

重复直到所有证明都通过。

‍

性能提示

1. 使用 pragma aborts_if_is_partial

不要试图指定每个框架终止条件。

‍

2. 保持规范重点突出

指定对你的业务逻辑有意义的内容：

// Good: Focused on business logic
// 好的: 专注于业务逻辑
spec deposit {
    aborts_if amount == 0;
    aborts_if amount == 0;
    ensures vault_balance_increases;
    ensures vault_balance_increases;
}

// Bad: Over-specifying framework details
// 坏: 过度指定框架细节
spec deposit {
    aborts_if !coin::is_account_registered&lt;AptosCoin>(user);
    aborts_if !coin::is_account_registered&lt;AptosCoin>(user);
    aborts_if coin::balance&lt;AptosCoin>(user) &lt; amount;
    aborts_if coin::balance&lt;AptosCoin>(user) &lt; amount;
    aborts_if !exists&lt;CoinStore&lt;AptosCoin>>(user);
    aborts_if !exists&lt;CoinStore&lt;AptosCoin>>(user);
    // ... 20 more framework conditions
    // ... 20 多个框架条件
}

‍

3. 分离复杂逻辑

如果验证速度慢，请考虑将复杂逻辑提取到具有自己规范的辅助函数。

‍

4. 对框架信任使用 assume

spec helper_function {
    // Trust framework guarantee
    // 信任框架保证
    assume fungible_asset::supply(metadata) >= 0;
    assume fungible_asset::supply(metadata) >= 0;

    // Prove your logic
    // 证明你的逻辑
    ensures result == compute_shares(amount);
    ensures result == compute_shares(amount);
}

结论

形式化验证将 “我认为这有效” 转化为 “我可以证明这有效”。 Move Prover 为你提供编译时数学保证，你的金库：

只能初始化一次
拒绝零存款/ 提取
维护正确的资产核算
保持金库状态一致性
在操作前验证所有先决条件

这是之间的区别：

"我们测试了 1000 个场景" → 1000/∞ 的置信度
"我们测试了 1000 个场景" → 1000/∞ 的置信度
"验证器验证了所有路径" → ∞/∞ 的置信度
"验证器验证了所有路径" → ∞/∞ 的置信度

‍

对于处理数百万 TVL 的生产 DeFi 协议，这种级别的保证并非可选项，而是必不可少的。形式化验证不会取代测试；它通过证明测试只能抽样的属性来补充它。

与任何测试方法一样，形式化验证都有其局限性，我们上面简要地介绍了这些局限性（例如，使属性未确定的超时）。还有另一个重要的限制：形式化验证仅证明声明的特定属性列表是否成立。开发人员或审计员可能会遗漏其他重要属性，而这些属性未经过验证。这些遗漏的属性正是攻击者倾向于利用的属性。

我们已经看到一些跨越各种生态系统的 DeFi 协议，它们经过了“形式化验证” 并且仍然被黑客入侵。在事后分析中，一旦确定并写下了缺少的属性，形式化验证器就会正确地标记出漏洞。

因此，在对形式化验证做出强烈声明时要小心。它不能证明不存在错误 - 这需要验证关于给定程序的 每个可能的 属性，这对于大多数真实世界的系统来说是不切实际的。

如果你来自 EVM 或 Solana 背景，并且想从概念上了解基于 Move 的系统如何处理安全性和正确性，那么这篇相关文章可能会有所帮助：

EVM 和 SVM 开发人员的 Sui Move：第 1 部分 - 思维模型 https://www.adevarlabs.com/blog/sui-move-for-evm-and-svm-developers-part-1-mental-models

我们根据实际审计工作和实际协议分析发布了类似的实用、高信号深度剖析。如果你正在构建接近底层的东西并关心其正确性，请在 X 和 LinkedIn 上关注 Adevar Labs，以获取有关 Move、Rust 和智能合约安全的文章。

‍

安全发布。

‍

参考文献

原文链接： adevarlabs.com/blog/prov...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

翻译
学分: 0
分类: 安全
标签: 形式化验证 Move Prover Aptos Vault 智能合约安全

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

使用 Move Prover 验证 Aptos Vault 的正确性

为什么需要形式化验证？

我们要构建什么

安装 & 设置

安装 Aptos CLI

安装 Move Prover 依赖

验证一切正常

初始化你的 Aptos 项目

金库 架构

高级设计

份额计算如何工作

金库 实现

编写形式化规范

理解 pragma aborts_if_is_partial

模块级别的 不变量

函数级别的规范

1. 初始化规范

2. 存款规范

3. 提取 规范

4. 查看函数规范

验证流程

运行 Prover

首先编译

运行验证

如果验证失败

经验证内容 vs 信任内容

显式验证 (你的规范)

隐式信任 (框架)

常见的规范模式

模式 1：状态先决条件

模式 2：输入验证

模式 3：状态后置条件

模式 4：单调属性

模式 5：精确更改

调试失败的证明

步骤 1：读取错误

步骤 2：检查反例

步骤 3：修复规范或代码

步骤 4：重新验证

性能提示

1. 使用 pragma aborts_if_is_partial

2. 保持规范重点突出

3. 分离复杂逻辑

4. 对框架信任使用 assume

结论

安全发布。

参考文献

0 条评论

文章目录

金库架构

金库实现

模块级别的不变量

3. 提取规范