Certora 竞赛报告：Aquarius

Certora 竞赛报告：Aquarius

目录

• 概述
  • 关于 Certora
  • 总结
• 突变
• 值得注意的属性
  • 捕获的实际 Bug
  • 在 AccessControl 合约中捕获的突变：management
  • 在 AccessControl 合约中捕获的突变：storage
  • 在 AccessControl 合约中捕获的突变：transfer
  • 在 FeesController 合约中捕获的突变：contract
  • 在 Upgrade 合约中捕获的突变：lib
• 免责声明

概述

关于 Certora

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

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

在本文详述的形式化验证竞赛中，参赛者形式化验证了 Aquarius 智能合约。本次形式化验证竞赛于 2025 年 5 月 7 日至 2025 年 6 月 18 日举行，是 由 Cantina 主办的审计 的一部分。

总结

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

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

突变

访问控制 Crate

emergency.rs 突变

emergency_0: 突变：跳过在 set_emergency_mode() 中设置/清除紧急模式。 漏洞：系统无法进入紧急模式，因此通过破坏缓解机制来延续系统面临的任何风险。

management.rs 突变

management_0: 突变：否定了 set_role_address() 中 is_transfer_delayed() 的测试。 漏洞：允许立即更改关键角色。

management_1: 突变：跳过在 set_role_address() 中设置角色。 漏洞：角色地址无法更改。

storage.rs 突变

storage_0: 突变：在 get_key() 中，为 RewardsAdmin 角色提供错误的 key（OperationsAdmin 而不是 Operator）。 漏洞：由于地址存储冲突，额外的权限授予 RewardsAdmin 和 OperationsAdmin。

storage_1: 突变：在 get_future_key() 中，为 EmergencyAdmin 角色提供错误的 key（FutureAdmin 而不是 FutureEmergencyAdmin）。 漏洞：由于地址存储冲突，完整的 Admin 权限可能会授予 EmergencyAdminRole。

storage_2: 突变：在 get_future_deadline_key() 中，为 Admin 角色提供错误的 key（FutureAdmin 而不是 TransferOwnershipDeadline）。 漏洞：无法启动 Admin 角色转移，在检查现有截止日期时将恢复并显示类型错误。

transfer.rs 突变

transfer_0: 突变：跳过 apply_transfer_ownership() 中的所有权转移。 漏洞：角色无法更改，违反了设计原则。

transfer_1: 突变：忽略 get_transfer_ownership_deadline() 中存储的截止日期并返回 0。 漏洞：apply_transfer_ownership() 始终恢复，因此角色无法更改，违反了设计原则。

transfer_2: 突变：忽略 put_transfer_ownership_deadline() 中请求的截止日期并存储 0。 漏洞：数字字面量 0 在放入存储时被视为默认类型 i32，但 get_transfer_ownership_deadline() 假定它是 u64，导致所有后续调用都恢复。因此，apply_transfer_ownership() 始终恢复，从而阻止了所有权更改，违反了设计原则。

transfer_3: 突变：无法在 revert_transfer_ownership() 中重置截止日期。 漏洞：Admin 和 EmergencyAdmin 的转移无法取消。

transfer_4: 突变：跳过 apply_transfer_ownership() 中的截止日期重置。 漏洞：首次转移 Admin 或 EmergencyAdmin 角色会阻止该角色的所有未来转移。

transfer_5: 突变：commit_transfer_ownership() 始终设置过去时间的截止日期。 漏洞：应该延迟的角色更改可以在启动后立即应用。

Fees Collector Crate

contract.rs 突变

contract_0 (public): 突变：删除了 commit_upgrade() 中的授权检查，该检查限制为 Admin 角色。 漏洞：任何人都可以启动包含任意代码的软件更新。

contract_1 (public): 突变：删除了 apply_transfer_ownership() 中的授权检查，该检查限制为 Admin 角色。 漏洞：任何人都可以完成 Admin 和 EmergencyAdmin 角色的转移。

contract_2 (public): 突变：get_emergency_mode() 始终返回 false。 漏洞：fees_collector.get_emergency_mode() 不可靠。

contract_3: 突变：删除了 revert_upgrade() 中的授权检查，该检查限制为 Admin 角色。 漏洞：任何人都可以取消软件更新。

contract_4: 突变：跳过在 set_emergency_mode() 中设置/清除紧急模式。 漏洞：系统无法进入紧急模式，因此通过破坏缓解机制来延续系统面临的任何风险。

contract_5: 突变：禁用 revert_transfer_ownership()。 漏洞：Admin 和 EmergencyAdmin 的转移无法取消。

contract_6: 突变：删除了 commit_transfer_ownership() 中的授权检查，该检查限制为 Admin 角色。 漏洞：任何人都可以启动将 Admin 和 EmergencyAdmin 角色转移到任意地址。

contract_7: 突变：无法在 commit_upgrade() 中存储代码哈希。 漏洞：升级永远无法完成。

contract_8: 突变：禁用 revert_upgrade()。 漏洞：升级永远无法取消。

Upgrade Crate

lib.rs 突变

lib_0: 突变：升级在 commit_upgrade() 中始终具有截止日期 0。 漏洞：升级只能在紧急模式下完成。

lib_1: 突变：跳过在 commit_upgrade() 中设置截止日期。 漏洞：升级只能在紧急模式下完成。

lib_2: 突变：跳过 apply_upgrade() 中的截止日期重置。 漏洞：任何过去的升级都可以再次应用。

值得注意的属性

捕获的实际 Bug

待处理升级的代码哈希必须在升级或取消时清除

以下两个属性捕获的真实 Bug： 两位参与者编写的属性捕获了此 Bug。问题是 commit_upgrade() 存储了“deadline”延迟时间戳和待处理升级代码的“future_wasm”哈希，但随后执行的 apply_upgrade() 或 revert_upgrade() 仅重置了截止日期，并将代码哈希保留在存储中。这会造成管理员意外（在紧急模式下）应用已取消的升级或重复升级的可能性。

作者：PositiveSecurity

fn reverted_upgrade_can_be_applied_in_emergency(e: Env, reverted_wasm_hash: BytesN<32>) {
    let admin = nondet_address();
    let emergency_admin = nondet_address();

    FeesCollector::commit_upgrade(e.clone(), admin.clone(), reverted_wasm_hash.clone());

    // Admin cancels previous upgrade
    // Admin 取消之前的升级
    FeesCollector::revert_upgrade(e.clone(), admin.clone());

    // EmergencyAdmin sets emergency mode
    // EmergencyAdmin 设置紧急模式
    FeesCollector::set_emergency_mode(e.clone(), emergency_admin.clone(), true);    

    // Reverted wasm_hash should be never deployed
    // 已恢复的 wasm_hash 不应部署
    cvlr_assert!(reverted_wasm_hash != FeesCollector::apply_upgrade(e, admin));
}

作者：alexzoid-eth

请注意，下面的 state_transition_upgrade_deadline_lifecycle() 函数可以测试不同的 call_fn 函数。它由 parametric_rule 宏 处理，此处的实现 生成每个目标函数的规则。

pub fn state_transition_upgrade_deadline_lifecycle(
    e: &Env,
    _params: &ParametricParams,
    call_fn: impl FnOnce()
) {
    let before = GhostState::read();
    call_fn();
    let after = GhostState::read();

    let valid = check_deadline_lifecycle(
        e,
        before.upgrade_deadline,
        after.upgrade_deadline,
        before.future_wasm,
        after.future_wasm,
    );

    cvlr_assert!(valid);
}

// Check deadline state change is valid: 0 -> timestamp -> 0
// 检查截止日期状态更改是否有效：0 -> 时间戳 -> 0
fn check_deadline_lifecycle(
    e: &Env,
    deadline_before: u64,
    deadline_after: u64,
    _future_before: Option<impl Clone>,
    future_after: Option<impl Clone>,
) -> bool {
    if deadline_before == 0 && deadline_after != 0 {
        // Transition from 0 to non-zero (commit)
        // 从 0 过渡到非零值（提交）
        deadline_after > e.ledger().timestamp() && future_after.is_some()
    } else if deadline_before != 0 && deadline_after == 0 {
        // Transition from non-zero to 0 (apply or revert)
        // 从非零值过渡到 0（应用或恢复）
        future_after.is_none() // <--------------------------------------------
    } else if deadline_before != 0 && deadline_after != 0 {
        // Cannot change non-zero deadline to different non-zero value
        // 无法将非零截止日期更改为不同的非零值
        deadline_before == deadline_after
    } else {
        true
    }
}

在 AccessControl 合约中捕获的突变：management

角色分配导致有效的状态更改

作者：AsafDov

捕获的突变：management_0, management_1

pub fn set_role_address_integrity(e: Env) {
    let acc_ctrl = unsafe { &mut *&raw mut ACCESS_CONTROL }.as_ref().unwrap();
    let role = nondet_role();
    let role_key = acc_ctrl.get_key(&role);
    let address_before = acc_ctrl.get_role_safe(&role);
    let address_to_set = nondet_address();

    acc_ctrl.set_role_address(&role, &address_to_set);

    let address_after = e.storage().instance().get::<DataKey, Address>(&role_key);

    match address_after{
        Some(address_after) => cvlr_assert!(
                !role.has_many_users()
            && address_after == address_to_set
            && ((address_before.is_some() && !role.is_transfer_delayed()) || (address_before.is_none()))
        ),
        None => {
            cvlr_assert!(false); // Cant set address to None
            // 无法将地址设置为 None
        }
    }
}

无法替换待处理的角色转移

作者：Bhargava-krishna

捕获的突变：management_0, management_1

pub fn management_set_role_address_panics_for_delayed_role_replacement(e: Env) {
    let access_control = AccessControl::new(&e);
    let address1 = nondet_address();
    let address2 = nondet_address();
    let role = Role::Admin;

    cvlr_assume!(!role_has_many_users(&role));
    cvlr_assume!(role_is_transfer_delayed(&role));
    cvlr_assume!(address1 != address2);

    // Set initial role
    // 设置初始角色
    access_control.set_role_address(&role, &address1);

    // Trying to replace delayed role should panic
    // 尝试替换延迟的角色应会panic
    access_control.set_role_address(&role, &address2);
    cvlr_assert!(false); // should not reach due to panic
    // 由于panic，不应到达
}

在 AccessControl 合约中捕获的突变：storage

为任何角色获取的地址与先前为该角色设置的地址匹配

作者：jraynaldi3

捕获的突变：management_1, storage_0, storage_1, transfer_2

pub fn set_role_address_integrity(e: &Env) {
    let access_control = AccessControl::new(e);
    let input: u8 = cvlr::nondet();
    let role:Role = role_randomize(input);
    let address = nondet_address();
    access_control.set_role_address(&role, &address);
    let address_after: Option<Address> = access_control.get_role_safe(&role);

    cvlr_assert!(address == address_after.unwrap());
}

具有延迟的角色转移存储未来地址和截止日期

作者：alexxander77

捕获的突变：storage_1, storage_2, transfer_5

pub fn commit_transfer_ownership_integrity(e: Env) {
    let role = nondet_role();
    let future_addr = nondet_address();
    let deadline_key = get_future_deadline_key_mock(&role.clone());
    let future_key = get_future_key_mock(&role.clone());
    let ac = AccessControl::new(&e.clone());

    let bad_role = match role {
        Role::RewardsAdmin => true,
        Role::OperationsAdmin => true,
        Role::PauseAdmin => true,
        _ => false,
    };
    let deadline_before = e.storage().instance().get::<DataKey, u64>(&deadline_key).unwrap_or(0);
    ac.commit_transfer_ownership(&role.clone(), &future_addr.clone());

    if bad_role || deadline_before != 0 {
        cvlr_assert!(false);
    } else {
        let deadline_after = e.storage().instance().get::<DataKey, u64>(&deadline_key).unwrap();
        let stored_addr = e.storage().instance().get::<DataKey, Address>(&future_key);
        cvlr_assert!(deadline_after == e.ledger().timestamp() + 3 * 86400);
        cvlr_assert!(stored_addr.is_some() && stored_addr.unwrap() == future_addr);
    }
}

在 AccessControl 合约中捕获的突变：transfer

任何具有延迟的角色转移都会存储可检索的截止日期

作者：alexzoid-eth

捕获的突变：storage_2, transfer_1, transfer_5

pub fn integrity_commit_transfer_deadline(e: Env, admin: Address, role_name: Symbol, new_address: Address) {
    let deadline = e.ledger().timestamp() + ADMIN_ACTIONS_DELAY;
    FeesCollector::commit_transfer_ownership(e.clone(), admin, role_name.clone(), new_address.clone());
    let result = FeesCollector::h_get_transfer_ownership_dl(e, role_name);
    cvlr_assert!(result == deadline);
}

应用挂起的角色转移将角色分配给预期地址并重置截止日期

作者：PositiveSecurity

捕获的突变：transfer_0, transfer_4

pub fn apply_transfer_ownership_correct(e: Env, role_name: &Symbol) {
    let admin = nondet_address();
    let role= Role::from_symbol(&e, role_name.clone());
    let new_admin = get_future_address(&role);
    FeesCollector::apply_transfer_ownership(e.clone(), admin, role_name.clone());
    cvlr_assert!(get_deadline(&role) == 0);
    cvlr_assert!(is_role(&new_admin, &role));
}

在 FeesController 合约中捕获的突变：contract

紧急模式激活，紧急升级返回预期哈希

作者：dapslegend

捕获的突变：contract_2, contract_4, contract_7, emergency_0

pub fn emergency_mode_enables_instant_upgrade_bypass(e: Env) {
    let admin = nondet_address();
    let emergency_admin = nondet_address();
    cvlr_assume!(admin != emergency_admin);

    FeesCollector::init_admin(e.clone(), admin.clone());
    let acc = access_control::access::AccessControl::new(&e);
    acc.set_role_address(&access_control::role::Role::EmergencyAdmin, &emergency_admin);

    // Enable emergency mode
    // 启用紧急模式
    FeesCollector::set_emergency_mode(e.clone(), emergency_admin.clone(), true);
    cvlr_assert!(FeesCollector::get_emergency_mode(e.clone()) == true);

    // In emergency mode, should be able to commit and apply immediately
    // 在紧急模式下，应该能够立即提交和应用
    let wasm = create_dummy_wasm(&e);
    FeesCollector::commit_upgrade(e.clone(), admin.clone(), wasm.clone());
    let applied_wasm = FeesCollector::apply_upgrade(e.clone(), admin.clone());
    cvlr_assert!(applied_wasm == wasm);
}

只有管理员可以执行升级和角色转移功能

作者：AsafDov

捕获的突变：contract_0, contract_1, contract_3, contract_6

pub fn only_admin_transfers_roles_or_upgrades(e: Env) {
    let acc_ctrl = unsafe { &mut *&raw mut ACCESS_CONTROL }.as_ref().unwrap();

    // Execute any operation, then restrict to those that require Admin
    // 执行任何操作，然后限制为需要管理员的操作
    let action = nondet_func(e.clone());
    cvlr_assume!(
        action == Action::CommitTransfer
            || action == Action::ApplyTransfer
            || action == Action::RevertTransfer
            || action == Action::CommitUpgrade
            || action == Action::ApplyUpgrade
            || action == Action::RevertUpgrade
    );

    let admin: Option<Address> = e.storage().instance().get(&acc_ctrl.get_key(&Role::Admin));
    match admin {
        Some(admin) => cvlr_assert!(is_auth(admin)),    // If there is an Admin, he must be signer.
        // 如果有管理员，他必须是签名者。
        None => cvlr_assert!(false),                    // Otherwise, the action requiring Admin should have reverted.
        // 否则，需要管理员的操作应已恢复。
    }
}

对于非管理员，升级和角色转移功能会恢复

作者：Zac369

捕获的突变：contract_0, contract_1, contract_3, contract_6

pub fn certain_functions_require_auth(e: Env) {
    // Randomly select and call a function that requires Admin or EmergencyAdmin role (without required role)
    // 随机选择并调用需要 Admin 或 EmergencyAdmin 角色的函数（不带所需的角色）
    let has_role = false;
    call_all_role_functions(e, has_role);

    cvlr_assert!(false);
}

在 Upgrade 合约中捕获的突变：lib

升级截止日期已正确设置和检索

作者：alexzoid-eth

捕获的突变：contract_7, lib_0, lib_1

pub fn integrity_commit_upgrade_deadline(e: Env, admin: Address, new_wasm_hash: BytesN<32>) {
    let expected_deadline = e.ledger().timestamp() + ADMIN_ACTIONS_DELAY;
    FeesCollector::commit_upgrade(e.clone(), admin, new_wasm_hash);
    let deadline = FeesCollector::h_get_upgrade_deadline(e);
    cvlr_assert!(deadline == expected_deadline);
}

提交升级受到限制，并设置可检索的哈希和截止日期

作者：AsafDov

捕获的突变：contract_0, contract_7, lib_0, lib_1

pub fn commit_upgrade_integrity(e: Env) {
    let admin = get_role_safe_address(Role::Admin);
    let new_wasm = nondet_wasm();

    FeesCollector::commit_upgrade(e.clone(), nondet_address(), new_wasm.clone());

    let deadline = get_upgrade_deadline(&e);
    let future_wasm = upgrade::storage::get_future_wasm(&e).unwrap();

    match admin {
        Some(admin) => cvlr_assert!(
            future_wasm == new_wasm
                && is_auth(admin)
                && deadline == e.ledger().timestamp() + 3 * 86400
        ),
        None => cvlr_assert!(false), // Cant commit upgrade if there is no admin
        // 如果没有管理员，则无法提交升级
    }
}

免责声明

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

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

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