Certora竞赛报告：Blend v2

Certora 竞赛报告：Blend v2

目录

• 概述
  • 关于 Certora
  • 总结
• 突变
• 值得注意的属性
  • 合约中捕获的突变：deposit
  • 合约中捕获的突变：fund_management
  • 合约中捕获的突变：pool
  • 合约中捕获的突变：user
  • 合约中捕获的突变：withdraw
• 免责声明

概述

关于 Certora

Certora 是一家 Web3 安全公司，提供行业领先的形式化验证工具和智能合约审计。Certora 的旗舰安全产品 Certora Prover 是一款独特的 SaaS 产品，它可以在智能合约中定位难以发现的错误，或以数学方式证明它们不存在。

形式化验证竞赛是一种竞赛，社区成员以数学方式验证智能合约的准确性，以换取赞助商根据参与者的发现和属性覆盖率提供的奖励。

在此处详细描述的形式化验证竞赛中，竞争者形式化验证了 Blend v2 智能合约。本次形式化验证竞赛于 2025 年 2 月 24 日至 2025 年 3 月 17 日举行，是 Code4rena 托管的审计 的一部分。

总结

引入代码“突变(mutations)”是为了评估竞赛参与者编写的规范的质量。这些突变如下所述，并在竞赛结束时在 此处竞赛存储库中更新的 mutations 目录 中提供，以及每个突变的描述。

21 名参与者提交了 229 个成功捕获突变的属性。其中一些属性包含在下面的报告中，作为高质量属性的示例。此外，顶级规范已添加到 竞赛存储库。你可以在 此处 找到比赛的最终结果。

突变

Deposit 突变

deposit_0: 突变：跳过 execute_deposit() 中 pool_balance 的更新，因此 pool 看起来比实际拥有的流动性和份额更少。

deposit_1: 突变：跳过 execute_deposit() 中 user_balance 的更新。

deposit_2: 突变：删除 execute_deposit() 中用于铸造零或负份额的错误检查。

deposit_3: 突变：删除 execute_deposit() 中对负存款的输入验证。

Fund Management 突变

fund_management_0: 突变：无法减少 execute_draw() 中的 pool 余额。

fund_management_1: 突变：删除 execute_draw() 中对负提款的输入验证。

fund_management_2: 突变：删除 execute_donate() 中对负捐赠的输入验证。

fund_management_3: 突变：无法增加 execute_donate() 中的 pool 余额。

fund_management_4: 突变：在 execute_donate() 中按减少的金额增加 pool 余额。

Pool 突变

pool_0: 突变：跳过 withdraw() 中 token 余额的减少。

pool_1: 突变：跳过 withdraw() 中 share 余额的减少。

pool_2: 突变：跳过 withdraw() 中 queued shares（排队份额）的减少。

pool_3: 突变：跳过 deposit() 中 token 余额的增加。

pool_4: 突变：在 queue_for_withdraw() 中减少（而不是增加）queued shares。

User 突变

user_0: 突变：无法增加 add_shares() 中用户的余额。

user_1: 突变：在 queue_shares_for_withdrawal() 中递增（而不是递减）用户的余额。

user_2: 突变：在 dequeue_shares() 中，当排队金额大于提款时，无法计算排队的份额，从而导致无限循环（拒绝服务）。

user_3: 突变：如果第一个排队金额小于提款，则无法在 withdraw_shares() 中取消排队份额。

Withdraw 突变

withdraw_0: 突变：无法更新 execute_dequeue_withdrawal() 中存储的用户余额。

withdraw_1: 突变：无法在 execute_queue_withdrawal() 中将用户份额排队以进行提款。

withdraw_2: 突变：无法在 execute_dequeue_withdrawal 中增加用户的份额余额。

withdraw_3: 突变：删除 execute_withdraw() 中阻止提取 0 个 token 金额的验证。

值得注意的属性

合约中捕获的突变：deposit

确保负存款失败

作者： PositiveSecurity

捕获的突变：deposit_2、deposit_3

pub fn execute_deposit_negative_amount_fails(e: &Env, from: Address, pool_address: Address, amount: i128) {
    cvlr_assume!(amount <= 0);
    execute_deposit(&e, &from, &pool_address, amount);
    cvlr_assert!(false);
}

存款正确影响份额和 Token 余额

作者： X0rD3v1L

捕获的突变：deposit_0、deposit_1

pub fn execute_deposit_correctness(e: &Env, from: &Address, pool_address: &Address, amount: i128) {
    cvlr_assume!(amount > 0);
    cvlr_assume!(from != pool_address);
    cvlr_assume!(from != &e.current_contract_address());

    let pool_balance_before = storage::get_pool_balance(e, pool_address);
    let user_balance_before = storage::get_user_balance(e, pool_address, from);

    let user_shares_before = user_balance_before.shares;
    let pool_shares_before = pool_balance_before.shares;
    let pool_tokens_before = pool_balance_before.tokens; // 假设 pool 存储 token 余额

    let minted_shares = execute_deposit(e, from, pool_address, amount);

    let pool_balance_after = storage::get_pool_balance(e, pool_address);
    let user_balance_after = storage::get_user_balance(e, pool_address, from);

    let user_shares_after = user_balance_after.shares;
    let pool_shares_after = pool_balance_after.shares;
    let pool_tokens_after = pool_balance_after.tokens;

    cvlr_assert!(minted_shares > 0);
    cvlr_assert!(user_shares_after == user_shares_before + minted_shares);
    cvlr_assert!(pool_shares_after == pool_shares_before + minted_shares);
    cvlr_assert!(pool_tokens_after == pool_tokens_before + amount);
}

合约中捕获的突变：fund_management

等额捐赠后的 Draw 产生原始 Pool Token 余额

作者： kind0Dev

捕获的突变：fund_management_0、fund_management_3、fund_management_4

pub fn draw_after_donation_neutral(e: Env, from: Address, pool_address: Address, donate_amount: i128, to: &Address) {
    cvlr_assume!(donate_amount > 0, "Donation amount must be positive");
    let pool_balance = storage::get_pool_balance(&e, &pool_address);

    let initial_pool_tokens = pool_balance.tokens;

    execute_donate(&e, &from, &pool_address, donate_amount);
    execute_draw(&e, &pool_address, donate_amount, &to);
    let pool_balance_after = storage::get_pool_balance(&e, &pool_address);

    cvlr_assert!(
        pool_balance_after.tokens == initial_pool_tokens,
        "Donation followed by immediate draw should leave pool token balance unchanged"
    );
}

捐赠正确增加 Pool Token 余额

作者： Zac369

捕获的突变：fund_management_3、fund_management_4

pub fn fund_deposit(e: &Env, from: &Address, pool_address: &Address, amount: i128) {
    let pool_balance_before = storage::get_pool_balance(e, pool_address);
    let pool_tokens_before = pool_balance_before.tokens;
    execute_donate(e, from, pool_address, amount);
    let pool_balance_after = storage::get_pool_balance(e, pool_address);
    let pool_tokens_after = pool_balance_after.tokens;
    cvlr_assert!(
        pool_tokens_after == pool_tokens_before + amount
    );
}

合约中捕获的突变：pool

等额存款和入队后的 Withdraw 产生原始 Pool 余额

作者： LSHFGJ

捕获的突变：pool_0、pool_1、pool_2、pool_3、pool_4

pub fn deposit_withdraw_no_change(e: &Env, pool_balance: &mut PoolBalance, tokens: i128, shares: i128) {
    let pool_balance_before = pool_balance.clone();
    pool_balance.deposit(tokens, shares);
    pool_balance.queue_for_withdraw(shares);
    pool_balance.withdraw(e, tokens, shares);
    let pool_balance_after = pool_balance.clone();
    cvlr_assert!(
        pool_balance_before.tokens == pool_balance_after.tokens &&
        pool_balance_before.shares == pool_balance_after.shares &&
        pool_balance_before.q4w == pool_balance_after.q4w
    );
}

Withdraw 需要非空队列和正余额

作者： jraynaldi3

捕获的突变：pool_0、pool_1、pool_2

pub fn withdraw_positive_value(e:&Env, tokens:i128, shares:i128){
    let mut pool_balance: PoolBalance = cvlr::nondet();

    pool_balance.withdraw(e, tokens, shares);

    cvlr_assert!(
        pool_balance.q4w >= 0
        && pool_balance.shares >= 0
        && pool_balance.tokens >= 0
    );
}

等额存款后的 Withdraw 产生原始 Pool 余额

作者： Zac369

捕获的突变：pool_0、pool_1、pool_3

pub fn deposit_withdraw_equal(e: &Env, pool_balance: &mut PoolBalance, tokens: i128, shares: i128) {
    let pool_tokens_before = pool_balance.tokens;
    let pool_shares_before = pool_balance.shares;

    pool_balance.deposit(tokens, shares);
    pool_balance.withdraw(e, tokens, shares);

    let pool_tokens_after = pool_balance.tokens;
    let pool_shares_after = pool_balance.shares;

    cvlr_assert!(pool_tokens_after == pool_tokens_before);
    cvlr_assert!(pool_shares_after == pool_shares_before);
}

合约中捕获的突变：user

为提款排队份额正确转移份额

作者： kind0Dev

捕获的突变：pool_4、user_1、withdraw_1

pub fn queue_withdraw_atomicity(from: Address, e: Env, pool_address: Address, queued_shares: i128,
) {
    cvlr_assume!(queued_shares > 0, "Rule relevant for positive queue amounts");
    let user_balance: UserBalance = storage::get_user_balance(&e, &pool_address, &from);
    let pool_balance: PoolBalance = storage::get_pool_balance(&e, &pool_address);

    let user_share_before = user_balance.shares;
    let pool_q4w_share_before = pool_balance.q4w;

    execute_queue_withdrawal(&e, &from, &pool_address, queued_shares);

    let user_balance_new: UserBalance = storage::get_user_balance(&e, &pool_address, &from);
    let pool_balance_new: PoolBalance = storage::get_pool_balance(&e, &pool_address);

    let user_shares_decrease = user_share_before - user_balance_new.shares;
    let pool_q4w_increase = pool_balance_new.q4w - pool_q4w_share_before;

    cvlr_assert!(user_shares_decrease == pool_q4w_increase, "Atomicity: Queuing should reduce user shares by the queued amount.");
}

提款正确更新排队的份额

作者： BenRai1

捕获的突变：user_3

pub fn user_withdraw_shares_rest_pushed_to_front(e: &Env) {
    let mut user_balance: UserBalance =cvlr::nondet();
    let shares: i128 = cvlr::nondet();
    cvlr_assume!(shares >= 0);
    let user_q4w_before = user_balance.q4w.clone();
    cvlr_assume!(user_q4w_before.len() == 3);

    let amount0 = user_q4w_before.get(0).unwrap().amount;
    let amount1 = user_q4w_before.get(1).unwrap().amount;
    let amount2 = user_q4w_before.get(2).unwrap().amount;

    cvlr_assume!(amount0 == amount1 && amount1 == amount2);
    cvlr_assume!(amount0 > 2); // prevent error becasue of rounding down
    cvlr_assume!(shares == amount0 + amount0 / 2); // make sure 1,5 q4w are removed

    //function call
    user_balance.withdraw_shares(&e, shares);

    let user_balance_after = user_balance.q4w.clone();
    let amount0_after = user_balance_after.get(0).unwrap().amount;
    let amount1_after = user_balance_after.get(1).unwrap().amount;

    cvlr_assert!(amount0_after == amount0 - (shares - amount0));
    cvlr_assert!(amount1_after == amount0);
}

合约中捕获的突变：withdraw

取消排队份额正确更新用户余额，其他用户不受影响

作者： BenRai1

捕获的突变：withdraw_0、withdraw_2

pub fn dequeue_increase_shares(e: &Env) {
    let from: Address = nondet_address();
    let pool_address: Address = nondet_address();
    let other_user: Address = nondet_address();
    let shares:i128 = cvlr::nondet();
    cvlr_assume!(from != other_user);

    //values before
    let user_shares_before = storage::get_user_balance(e, &pool_address, &from).shares;
    let other_user_shares_before = storage::get_user_balance(e, &pool_address, &other_user).shares;

    execute_dequeue_withdrawal(e, &from, &pool_address, shares);

    //values after
    let user_shares_after = storage::get_user_balance(e, &pool_address, &from).shares;
    let other_user_shares_after = storage::get_user_balance(e, &pool_address, &other_user).shares;

    cvlr_assert!(user_shares_after == user_shares_before + shares);
    cvlr_assert!(other_user_shares_after == other_user_shares_before);           
}

免责声明

Certora Prover 接受合约和规范作为输入，并正式证明合约在所有情况下都满足规范。值得注意的是，Certora Prover 的保证范围仅限于提供的规范，并且 Certora Prover 不检查规范未涵盖的任何情况。

Certora 不提供任何形式的明示或暗示的保证。本报告的内容不应被解释为完全保证合约在所有维度上都是安全的。在任何情况下，Certora 或其任何员工或社区参与者均不对因本文报告的结果引起或与之相关的合同、侵权或其他行为中的任何索赔、损害或其他责任负责。所有智能合约软件的使用均应由用户自行承担风险和责任。

• 原文链接： github.com/code-423n4/20...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～