Solana智能合约的形式化验证

在我们之前的帖子中，我们描述了新的 Solana 合约验证工具。本文展示了该验证器在广泛使用的 Solana 应用 SPL Token 2022 上的实际应用。在下一篇帖子中，我们将展示如何在 SPL Token 2022 的保密扩展中发现漏洞。

Solana 的 SPL Token 类似于以太坊上的 ERC-20 tokens。例如，SPL Token 允许你铸造代币、转移代币、销毁代币等。SPL Token 2022 为 SPL Token 添加了额外的功能，例如保密转账、不可转让代币、不可变账户所有权等。在本文中，我们演示了如何证明基本操作的正确性，例如 Mint 操作。Mint 是通过函数 process_mint_to 实现的，其代码可以在 这里 找到。

代码的简要概述

请注意，此文档的范围不包括对 Mint 操作 所有细节的描述。实际上，我们认为无需成为 SPL Token 的专家，就可以验证其正确性。相反，我们仅在图 1 和图 2 中展示了一些相关代码部分。

图 1: process_mint_to 的前导部分

相关参数为 accounts 和要铸造的代币 amount。该函数的第一步是提取每个账户：

• 铸币账户 mint_info（跟踪新代币基本信息的账户，例如供应量）
• 目标账户 destination_account_info（新代币将转移到的代币账户）
• 所有者账户 owner_info（拥有代币的另一个代币账户）

该函数执行一系列检查（此处未显示），以确保操作可以进行。例如，其中一个检查确保铸币账户不被冻结，因此可以铸造代币。另一个检查验证所有者账户实际上是要转移的代币的实际所有者。

图 2: 代币的转移和代币供应的更新

图 2 展示了 process_mint_to 的实际计算过程：代币的数量被转移到目标账户，并且铸币账户被更新为新的供应量。

注意：

该代码检查整数溢出。如果对 process_mint_to 的调用成功，我们可以确定没有发生整数溢出。

编写规范

为了使用 Solana Certora Prover (SCP)，我们首先需要编写一个验证工具。在这个 验证工具 上调用被验证的函数，类似于测试工具，但测试时的函数输入必须是实际值，而在验证工具中输入可以是符号化的。在函数成功返回后，工具可以有一个或多个断言，用于描述感兴趣的属性。图 3 显示了我们的 process_mint_to 验证工具的完整代码。

图 3: process_mint_to 的验证工具

如你所见，验证工具实际上只是一个用 Rust 编写的函数。在这种情况下，我们不需要对 process_mint_to 进行任何修改。一个典型的验证工具包括三部分：

1. 一个非确定性的 Solana 环境，以及任何必要的限制环境的前置条件。
2. 调用被验证的函数。
3. 后置条件。

为了编写非确定性环境，我们构建了一个 Rust 库，扩展了 Rust 基本类型（如布尔值、整数等）和 Solana 特定类型（如 AccountInfo 或 PubKey），创建可以被 SCP 解释为完全符号化的对象（例如，见图 3 中的 nondet 函数）。

例如，acc_infos 是三个非确定性账户的数组：铸币账户、目标账户和所有者。除了创建新的环境外，请注意 Solana 开发者还可以编写限制环境的前置条件。

例如，CVT_assume(amount>0) 告诉验证器我们只关心输入量严格大于零的情况。

在此之后，验证工具用新的环境和一个符号化的非零正数量调用 process_mint_to。非常重要的是，验证工具会对 process_mint_to 返回的值调用 unwrap。这意味着如果 process_mint_to 产生某种错误（即任何检查失败），则调用将会 panic（即中止），因此，验证工具的其余部分将永远不会被执行。特别是，如果验证工具的执行发生 panic，则后置条件（之后的断言）将不会被执行。虽然这可能违反直觉，但这正是我们想要的行为。如果对 process_mint_to 的调用失败，那么进行调用的 Solana 交易将会被还原，对区块链状态没有任何影响。

最后但同样重要的是，有四个断言（见对 CVT_assert 的调用）用于建立后置条件。第一个断言检查在调用 process_mint_to 之后目标账户的代币数量必须等于调用之前的代币数量加上所铸造的代币数量。第二个断言检查调用之后的代币数量必须严格大于之前的代币数量。请注意，只有当我们添加了前置条件量大于零时，这种情况才会成立。类似地，第三和第四个断言检查相同的条件，但用于代币供应量。

编译 SPL Token 2022 和使用 SCP

由于 SPL Token 2022 是用 Rust 编写的，因此要使用我们的验证工具编译应用程序，我们首先需要修改 Cargo.toml ，以便包含 Certora 库，该库包含创建新环境所需的所有功能以及图 3 中用于编写前置条件和后置条件的特殊函数：

[dependencies.solana-cvt]
path = "../../solana-cvt"

并在 lib.rs 中添加以下行：

mod certora_verification_harness;

其中 certora_verification_harness.rs 包含了在图 3 中展示的函数 integrity_of_process_mint_to。

然后，我们就可以使用以下命令生成 SBF：

cargo build-sbf --arch=sbfv2

最后，运行 Solana Certora Prover：

certoraRun.py target/sbf-solana-solana/release/spl_token_2022.so \
              --prover-args \
              "-solanaEntrypoint integrity_of_process_mint_to"

已验证：integrity_of_process_mint_to integrity_of_process_mint_to：所有输入上的属性成功验证

选项 solanaEntrypoint 告诉验证器验证过程应从我们的工具开始。在这种情况下，SCP 可以在几毫秒内证明该属性。

结论

我们展示了如何使用 SCP 来证明 Mint 操作的正确性。作为 Solana 开发者，主要任务是编写一个验证工具，其中包含规范（前置条件和后置条件）及被验证代码所需的 Solana 环境。在我们的下一篇 帖子 中，我们将展示如何在 SPL Token 2022 的保密扩展中找到漏洞，这将需要使用验证模拟。

如果你希望将 Solana 集成到开发过程中，请与我们联系。

感谢致辞：感谢 Arie Gurfinkel 教授（滑铁卢大学）在本项目中提供的宝贵帮助，以及 Certora 团队，特别是 Alexander Bakst 和 John Toman。

参考文献

要了解更多有关 Solana 编程模型的信息，请访问 https://solanacookbook.com/

SPL Token 的源代码：https://github.com/solana-labs/solana-program-library/tree/master/token/program

SPL Token 2022 的源代码：https://github.com/solana-labs/solana-program-library/tree/master/token/program-2022

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