通过形式验证审查Solana上的Token扩展

Certora 团队最近完成了对 Solana 上的 token extensions 的审查，利用了我们深入的形式验证工具。我们为代码的某些关键属性编写了规范（也称为 规则），并应用了 Solana Certora Prover，这是我们构建的一个工具，用于自动证明代码行为符合预期。该 Prover 验证 Solana 二进制格式（SBF）代码，这是实际在 Solana 区块链上运行的代码。

编写形式验证规范的好处之一是，它们可以描述极不可能发生但对安全性至关重要的场景。

在这篇博客中，我们希望为你提供我们对 token extensions 的一些关键发现的概述，来自我们的 安全报告。如果你想了解什么是形式验证，以及它如何应用于 Solana 区块链，我们已经为你创建了一系列 入门博客文章。

首先，一些关于 token extensions 的背景

Token2022 是一个在 Solana 区块链上运行的 程序，与 'legacy' SPL Token 程序并行。它于 2024 年初在主网首次部署，已成为在 Solana 上部署 token extensions 的热门选择，截至目前已经部署了超过 700,000 个 tokens。

与大型机构合作开发的 token extensions 解决了传统 token 的限制，为 Solana 开发者提供了在前所未有的水平上添加可编程特性的工具。这种灵活性在 KYC 或支付对账等企业用例中特别有价值，为 Solana 项目提供内置合规性。

尽管开发者仍可以使用传统 tokens，但新的 token extensions 提供了更简单、更强大的替代方案：

• 高级功能可以原生构建到 tokens 中，而无需依赖内部或第三方开发的自定义 token 程序。
• 丰富的链上元数据，可以通过简单的更新交易轻松初始化、存储并随后修改到 token mint。
• 目前，Token2022 总共提供 15 种扩展，可以添加到 tokens 中，以增加如机密转账、原生稳定币支持、转账费用以及创建 "soulbound"（不可转让）tokens 的能力。

结果是即插即用、符合监管要求、多功能的 token 功能，显著减少了工程时间和资源。

重要的是，Token2022 程序已经由 几位知名审计员 手动审核。然而，Certora 的工作是首次自动验证 SBF 代码。

我们主要发现的总结

以下是我们审查的一些亮点：

1. 我们的审查过程，包括对低级 SBF 代码的验证，识别出优化机会，从而使程序性能提高了多达 20%。

2. 我们开发了验证 Solana 团队最近实施的更新的规则。这些规则有助于加强现有保护措施，并通过覆盖广泛的行为范围，为潜在问题提供额外证明。

3. 我们编写了可重复使用的规范，使用它们验证多个指令。这种方法发现，尽管针对转账指令（Transfer 和 TransferChecked）已实施修复，但在燃烧指令（Burn 和 BurnChecked）中却缺失。这一差异未被之前的所有审计员发现。

让我们更详细地探讨这些问题。

识别提升性能的机会

Solana 运行时提供了系统调用 sol_memcmp，实现非重叠内存比较。Rust 编译器和 LLVM 提供了内置的内在函数 memcmp 来执行相同的操作。混合使用两者会阻止许多 LLVM 优化，因为 LLVM 将 sol_memcmp 视为未知的外部函数。同时，所有对 memcmp 的使用都被编译为多个字级比较或调用 sol_memcmp。具体选择受 Rust 编译器和 LLVM 优化开关的控制。缺乏这些优化可能会增加 SBF 文件的复杂性，因此，增加其计算单位。

在我们的报告中，我们建议不使用 sol_memcmp，而是使用 Rust 提供的跨平台独立比较。这是遵循我们建议的 提交。作为该提交的一部分，有一些测试显示了计算单位的减少。例如，对于 TransferChecked 指令，减少约为 20%。

这种优化是通过手动检查 SBF 代码发现的。

验证程序更新

在这个 修复 之前，Solana 程序库（SPL）依靠 Mint 账户跟踪不可转让 tokens。然而，SPL 也允许未检查（传统）转账，这些是没有 Mint 账户的转账。

我们编写了一个规则，检查传统与受检查转账指令是否等效，唯一例外是受检查指令需要一个 mint，而传统指令则不需要。这是该规则的简化版本：

#[rule]

/// 如果受检查转账失败，则未检查（传统）转账也应失败
fn rule_transfer_unchecked_checked() {

    // 生成符号账户
    let acc_infos = acc_infos!(); // Certora 宏
    let source_info = &acc_infos[0];
    let mint_info = &acc_infos[1];
    let destination_info = &acc_infos[2];
    let authority = &acc_infos[3];

    // 生成非确定性指令参数
    let decimals:u8 = nondet(); // Certora 函数
    let amount:u64 = nondet();

    // 增加一些限制 mint_info 的前置条件
    ...
    let res1 = process_transfer(&id(), &acc_infos, amount,
                                Some(decimals), None).is_err();
    cvt_assume!(res1); // Certora 宏
    ...

    let res2 = process_transfer(&id(),&acc_infos, amount,
                                None, None).is_err();
    cvt_assert!(res2); // Certora 宏
}

Certora 规则是用 Rust 编写的特殊函数。规则与测试工具非常相似。首先，为被验证的函数创建一个环境。与测试类似，此环境可能包含限制环境的前置条件。其次，调用要验证的函数。第三，一些预期属性被检查。

形式验证与测试的主要区别在于，验证的环境不需要是具体的。我们规则创建的环境通过调用 Certora 提供的宏 acc_infos! 生成一组符号的 AccountInfo。该宏生成区块链状态，在该状态下，对 process_transfer 的调用将被执行。除非额外写入前置条件，否则账户是完全不受限制的。例如，账户的公钥是符号的，因此可以取任何值。同样，账户的数据仅仅是一个非确定性字节数组。基本类型（例如 u8 和 u64）实现了一个新的 Rust trait Nondet，生成适当类型的符号值。前置条件或假设可以通过调用宏 cvt_assume! 编写。最后，通过调用宏 cvt_assert! 检查属性。

我们的规则创建了一个由四个账户组成的符号环境：source、mint、destination 和 authority。第二个账户是特别重要的，因为该工具需要增加一些额外的前置条件以排除错误格式的 Mint 账户。这是因为只有在指令不因与 Mint 账户相关的错误而回滚时，我们的属性才成立。为了简单起见，我们从上述规则描述中排除了这些前置条件。此外，该规则还为预期的 Mint 账户的 decimals 和待转移的金额创建了两个额外的不受限制的符号值。然后，该工具声明，如果带 Mint 账户的 process_transfer 调用（这通过第四个参数不是 None 之一设置为已知）回滚，则不带 Mint 账户的 process_transfer 调用（第四个参数为 None）也必须回滚。

该规则发现了在 这里 修复的问题，并确认修复是正确的。重要的是注意，这个规则实际上是相当通用的，可以检测未检查和受检查转账之间的其他不一致性。

编写可重复使用的规范

CpiGuard 扩展确保在 CPI（跨程序调用）期间某些操作不能进行。例如，当受到 CpiGuard 扩展保护时，资金减少的指令（Transfer、TransferChecked、TransferCheckedWithFee 和 Burn）在由所有者签名时不应被允许。其目的是只有在由其他账户委托签名时，才允许它们在 CPI 中被调用。具体而言，如果启用了 CpiGuard，则应禁止以下场景（即指令应回滚）：

1. 帐户被委托给自己
2. 帐户是 Mint 的永久委托
3. 帐户由系统程序或销毁器拥有（在此情况下，签名权限不被检查，可以是任意的）

在这个 提交 之前，SPL 允许账户自我委托并签署燃烧指令（Burn 和 BurnChecked）。Certora 团队编写了这个规则，以检查上述提交是否确实排除了自我委托：

#[rule]

fn rule_process_burn_cpi() {
   let acc_infos = acc_infos!(); // Certora 宏
   let source_info = &acc_infos[0];
   let authority_info = &acc_infos[2];
   let source_base =
       get_account_base!(source_info); // Certora 宏
   let amount_arg: u64 = nondet(); // Certora 函数
   let expected_decimals_arg:u8 = nondet(); // Certora 函数
   let source_data = source_info.data.borrow();
   let acc = StateWithExtensions::<Account>::unpack(&source_data)
             .unwrap();
   let ext = acc.get_extension::<CpiGuard>().unwrap();
   cvt_assume!(ext.lock_cpi.into()); // Certora 宏
   cvt_assume!(in_cpi()); // Certora 宏
   process_burn(&id(), &acc_infos,
                amount_arg,expected_decimals_arg.into()).unwrap();
   cvt_assert!
      (&source_base.owner != authority_info.key); // Certora 宏

这个规则与前一个规则的结构相同。我们首先通过调用 acc_infos! 和 nondet 生成符号环境和指令参数。新的一部分是，规则仅在源账户具有扩展 CpiGuard（第 8-9 行）、lock_cpi 被启用，并且当前指令通过其他指令以 CPI 方式执行（第 11 行）时才会成功。在那之后，如果指令 BurnChecked 成功（通过对 process_burn 调用识别，第四个参数不同于 None），则源的所有者不能签署该指令（第 13 行的断言）。

我们对转账指令（Transfer 和 TransferChecked）应用了相同的规则，仅将对 process_burn 的调用替换为对 process_transfer 的调用，发现转账仍然允许自我委托。该问题已被 SPL 开发人员认可并在这个 提交 中修复。

结论

使用 Certora Solana Prover，我们能够通过正式验证一些关键逻辑、验证以前的代码更新和识别性能优化，为 Token2022 程序的安全性做出贡献。

作为 Solana 开发者，你也可以将形式验证的好处应用于你的项目，并在部署到生产之前检测问题。

要了解有关我们的工具以及我们如何帮助保护你的应用程序的更多信息，请访问我们的网站 certora.com，并通过 此邀请链接 加入 Certora Discord 服务器。我们期待你加入我们的社区！

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