Rust智能合约安全竞赛 - 赛后感

Certora 最近组织了有史以来第一次使用 Certora 的 开源 Prover 进行 Rust 的形式化验证竞赛。我们为 Soroban 智能合约举办了两次社区竞赛，总奖金为 40,000 USDC，合作的审计平台为 Code4rena 和 Cantina。这些竞赛向 Soroban 开发者社区介绍了形式化验证，并展示了其在基于 Rust 的智能合约中的适用性。我们将深入探讨来自我们社区的示例。

形式化验证 是一种基于数学逻辑的严谨方法，用于确保程序按照规范运行。它是一种有效的智能合约安全技术。在 Certora，我们开发了工具来保护 EVM、Solana 和 Stellar 的智能合约，并且正在研究更多链。

虽然 Certora Prover 一直是过去许多 Solidity EVM 形式化验证竞赛 的核心，但我们现在已经举办了前两次用 Rust 编写的代码竞赛，特别是为 Stellar 区块链 编写的 Soroban 智能合约。正如 我们最近的博文 中所述，使用 Rust 编写去中心化金融 (DeFi) 智能合约的团队应该考虑设计和编码选择，这些选择既可以降低逻辑错误的发生率，又可以使代码更易于形式化验证。

我们邀请了 Web3 安全社区的所有成员使用我们的形式化验证工具 Sunbeam，该工具以使用 Soroban 框架编写的 Stellar 智能合约为目标。这些合约用 Rust 编写，并以 WebAssembly 字节码的形式部署在 Stellar 上。用户使用 Certora 的 Rust 库 CVLR 编写形式化规范，表达安全和正确性相关的属性，该库具有 宏 专门 用于 Soroban。Sunbeam 编译 CVLR 规范和智能合约源代码以生成 WebAssembly 字节码，然后形式化验证字节码，证明代码是否符合规范中的属性。

评估规范

我们使用 mutation testing（突变测试）通过评估其形式规范的质量来评估竞赛参与者的工作。传统上，突变测试会在代码中注入小的、原子性的错误，并运行测试套件以查看是否捕获到这些错误。这可以用于通过添加开发人员遗漏的测试用例来提高测试套件的覆盖率。在 Certora，我们将这个想法扩展到形式化验证：我们通过（单独地）将突变应用于原始智能合约源代码并运行 Sunbeam prover 来评估规范的覆盖率和质量，以查看哪些规范可以捕获突变。

对于 Solidity，我们构建了 Gambit，一个突变体生成器，可以自动创建智能合约的突变变体。对于像 Soroban 这样的基于 Rust 的智能合约，我们同时使用手动创建的突变体和一些由类似 Gambit 的工具 universalmutator 生成的突变体。

对于两次竞赛，我们都创建了一组基于领域知识的突变体，并使用它们来评估参与者编写的规范。通过捕获更多的突变体，规范可以获得更多的比赛奖励。每个捕获的突变体的价值与捕获它的参与者数量成反比，因此更高的奖励将颁发给具有更独特覆盖率的规范。此外，参与者通过创建一个捕获协议代码中真实漏洞的规范而获得更多的奖励，这已得到 Code4rena 和 Cantina 审计竞赛评委的确认。

Blend v2 竞赛

我们的 Blend 协议 竞赛是 DeFi 领域有史以来第一次基于 Rust 的形式化验证竞赛！我们与 Code4rena 合作，在他们于 2025 年 2 月 24 日至 3 月 17 日期间对 Blend v2 智能合约进行的 社区审计 期间组织了这次竞赛。

由于比赛时间很短，我们将范围缩小到实现 Backstop 合约的关键文件。我们选择此合约是因为它对于协议的偿付能力至关重要，因为 Backstop 为每个 Blend 贷款池提供保险。在本次竞赛中，21 名参与者总共创建了 996 条规则，其中 229 条规则至少捕获了一个突变体。此处 提供了一份报告，重点介绍了其中的一些规则，包括 Zac369 的这条规则，该规则捕获了 pool.rs 文件的 3 个突变体：

#[rule]
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);
}

上面的代码是一个 CVLR 规则，它陈述了许多 DeFi 协议的一个简单但重要的属性：任何用户向任何池存入，然后取出相同数量的存款，都不会导致池资产的损益。cvlr_assert!() 宏测试一个条件，Prover 尝试找到该条件为假的任何反例。如果找到，则可以调查反例的调用跟踪，以查看该行为是否表明合约逻辑中存在错误。另一方面，如果 Prover 完成而没有找到反例，则该属性被证明为真。在 Blend 竞赛中，此规则使用原始 Blend 源代码通过，但在我们突变 pool.rs 源代码时失败，从而捕获了突变体，并显示了该规则在保护协议的这一方面中的价值。

Aquarius 竞赛

我们第二次对 Rust 智能合约进行形式化验证的 竞赛 是与 Cantina 的审计 合作完成的，审计对象是 Aqua Network 的 Soroban 协议 Aquarius，时间从 2025 年 5 月 7 日到 6 月 18 日。

Aquarius 是一个为 Stellar 提供的去中心化流动性管理平台。它支持使用以下两种类型的流动性池交换代币：使用 Uniswap 的开创性恒定乘积做市商的波动资产，以及使用 Curve 的 Stable Swap 模型实现最小滑点的稳定（或“高度相关”）资产。形式化验证的范围 包括 fees_collector 和 access_control 合约，这些合约实现了协议的管理，包括升级和所有权转移。我们有 26 名参与者，他们总共为比赛编写了 1627 条规则的规范。其中，456 条规则至少捕获了一个突变体。此处 提供了一份竞赛结果报告，这是报告中高亮显示的属性之一。它由 AsafDov 编写，并捕获了 fees_collector contract.rs 文件的 4 个突变体。

#[rule]
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 {
  // If there is an Admin, he must be the sender.
        Some(admin) => cvlr_assert!(is_auth(admin)),
  // Otherwise, the action requiring Admin should have reverted.
        None => cvlr_assert!(false),
    }
}

上面的 CVLR 规则测试了一个常见的 DeFi 治理属性：只有管理员才能采取关键操作。并且它以一种允许该规则涵盖多个操作安全性的方式执行此操作。nondet_func() 在此处实现 从函数列表中随机选择。这让 Prover 可以在评估此规则时探索所有可能的执行路径。然后，该规则将搜索空间限制为仅需要 Admin 角色的函数（即转移或升级操作）。它获取当前管理员的地址，并验证任何成功执行的所选函数都必须由管理员调用。或者，如果没有设置管理员，则必须恢复执行，以防止到达 cvlr_assert!(false)。

与之前的 Blend 示例类似，此规则使用原始 Aquarius 源代码通过，但在我们将错误注入到 contract.rs 源文件中时失败，表明如果将这些漏洞引入到治理逻辑中，此规则可以捕获它们。

结论

Blend 和 Aquarius 是 Stellar 链的基石协议，其构建非常重视安全性。这些团队聘请 Certora、Code4rena、Cantina 和更广泛的 DeFi 安全社区参加形式化验证竞赛。Certora 赞扬所有竞赛参与者的工作，并祝贺顶级选手 alexzoid 和 PositiveWeb3 分别在 Blend v2 和 Aquarius 竞赛中 获得的奖励。每次都有超过 20 名竞争者，并且从第一次到第二次比赛增加了 24%，我们的安全审计师社区有能力应对保护 Rust 智能合约的挑战。我们希望这能鼓励其他人也组织形式化验证竞赛。

社区审计利用了许多人的知识和技能来保护 Blend 和 Aquarius 协议。添加 Certora 的形式化验证还利用了社区编写高级属性（超过 2600 个！）的技能，将其转化为规范，这些规范可以排除错误的存在的可能性，并且在集成到项目的开发管道中时，可以自动阻止将来引入错误。

所有智能合约开发人员都应考虑形式化验证来加强代码安全性，并且 Certora Sunbeam Prover 是保护 Stellar 区块链上 Rust 智能合约的强大工具。

致谢

我们要感谢 Stellar Development Foundation、Code4rena、Cantina、Blend 团队、Aquarius 团队、所有参与者以及我们的开发人员为实现这些竞赛所做的共同努力。

参考文献

Blend 文档：

• https://docs.blend.capital/users/general-faq
• https://docs.blend.capital/blend-whitepaper#backstop-module

Aquarius 文档：

• https://docs.aqua.network/
• https://learnblockchain.cn/article/20481

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