SPL Token 2022的形式验证

作者：Jorge A. Navas

编辑：Uri Kirstein, Chandrakana Nandi, 和 David Mwihuri

在我们之前的 帖子 中，我们描述了我们新的 Solana 合约验证工具。在本篇中，我们展示其中在 SPL Token 2022 上的应用，这是一个广泛使用的 Solana 应用。在接下来的 帖子 中，我们将展示如何在 SPL Token 2022 的机密扩展中发现缺陷。

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

代码概览

请注意，本篇的范围并不包括描述铸造操作的所有细节。事实上，我们认为不必要成为 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 证明铸造操作的正确性。作为 Solana 开发者，主要任务是编写一个验证工具，其中包含规范（先决条件和后置条件）以及所验证代码所需的 Solana 环境。我们下一个 帖子 将展示如何在 SPL Token 2022 机密扩展中发现缺陷，这将需要使用验证模拟。

致谢：感谢 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

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