SPL Token 2022 保密扩展的形式验证

作者：Jorge A. Navas

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

在之前的 帖子 中，我们展示了如何证明 Mint 操作的正确性，该操作是 SPL Token 和 SPL Token 2022 的基本功能的一部分。在这篇文章中，我们展示了 Solana Certora Prover (SCP) 如何被用于发现 SPL Token 2022 的 保密扩展 中的 Bug。

保密扩展的主要思想是允许在不实际透露其实际价值的情况下对帐户余额进行声明。虽然这似乎有些神奇，但 零知识证明 (ZK) 证据 则可以完全实现。我们在这篇文章末尾提供了一个链接，以便你想了解更多关于 ZK 证明以及它们是如何在 Solana 中高效实现的。

在这篇文章中，我们关注的是 SPL 审计员在 process_withdraw 中发现的一个 Bug。其源代码可以在 这里 获得。此函数允许从帐户中提取代币。由于实际余额是加密的，因此该函数依赖于 ZK 证明来验证帐户是否有足够的资金。一项关键的正确性属性是，与 ZK 证明相关联的公钥必须与将从中提取资金的代币帐户使用的公钥相同。此属性在旧版本的 SPL Token 2022 中未得到保持，这被归类为严重 Bug，因为可以从帐号中提取任意数量的代币。Bug 的修复可以在 这里 找到。

让我们看看如何使用 SCP 找到这个 Bug。如果你已经阅读了我们之前的 帖子，你就会知道我们需要做的第一件事是编写一个验证工具。在之前的帖子中，我们解释了验证工具是什么，并为 Mint 操作编写了一个。图1 显示了我们为 process_withdraw 编写的验证工具。

图1：process_withdraw 的验证工具

再次注意，验证工具是用 Rust 编写的，并且需要与 SPL Token 2022 一起编译。有关详细信息，请参见我们之前的 帖子。在第64行，调用了待验证的函数 process_withdraw。在第57-62行，我们为该函数创建了一个新的 Solana 环境。

这个新的环境由以下部分组成。调用 process_withdraw 的第二个参数 acc_infos 包含四个帐户。在这四个帐户中，第一个帐户称为 token account，它是用于扣除资金的帐户。process_withdraw 的第三个参数是要提取的 amount。第五个参数 new_decryptable_available_balance 包含可用余额的加密形式，最后，第六个参数 proof_instruction_offset 描述了同一事务中哪个指令包含 ZK 证明。我们省略了第一个和第四个参数的详细信息，因为它们在本文中不相关。

注意，所有这些参数都是通过调用在 这个库 中定义的 cvt::nondet 非确定性地初始化的。回想一下在之前的 帖子 中，定义变量的非确定性值允许 SCP 为该变量创建特定类型的符号值，而不是去推理具体值。最后，与 Mint 操作的验证工具不同，这个验证工具没有在新的环境中添加额外的前提条件。

调用之后，我们希望证明：

如果 process_withdraw 成功返回，则代币帐户的加密公钥与用于生成 ZK 证明的公钥相同。

首先需要注意的是，我们在返回的值上调用了 unwrap 方法，由 process_withdraw 生成。这意味着，如果 process_withdraw 产生错误，则调用将会 panic，因此，第69行的断言（图1）将永远不会执行。注意这可以接受，因为我们只想在函数成功返回时检查我们的属性。断言 CVT_assert 使用了两个辅助函数，这使我们能够访问：(1) 从 token account 的扩展 get_encryption_key_from_confidential_extension 获取加密密钥，以及 (2) ZK 证明 get_proof_withdraw_account。虽然前者没有什么特别之处，但后者构成了我们所称的 verification mock，需要更多的解释。

为了理解什么是验证 mock 以及我们在这里为什么需要一个，让我们首先描述图2中显示的 process_withdraw 的相关代码。

图2：在 process_withdraw 中使用 ZK 证明检查帐户是否有足够资金

第444-450行获取声称代币帐户有足够资金的 ZK 证明。第461-465行对加密余额进行实际提取，第469-471行检查新的可用余额是否与 ZK 证明一致，否则将返回错误。至关重要的是，第456-458行的检查最初被忽视并导致我们的属性被违反。

不幸的是，提取 ZK 证明的代码（第444-450行）对于我们的验证器和任何静态分析器来说过于复杂。在 Solana 中，事务由指令组成。例如，特定调用 process_withdraw 就构成了一条指令。有趣的是，ZK 证明不是作为另一参数传递给 process_withdraw，而是作为同一事务的一部分提供的另一条指令。图1中的参数 proof_instruction_offset 告诉我们在同一事务的哪个指令中存放 ZK 证明。因此，值得注意的是，为执行一条指令，我们需要从同一事务中提取另一条指令。这通过 instruction introspection 的机制实现。此外，由于涉及数学的复杂性，自动推理 ZK 证明的正确性非常困难。幸运的是，我们并不关心程序如何提取证明或证明是否是真实的 ZK 证明。相反，我们只关心它的公钥及 其用法。考虑到这一点，我们通过为 SCP 专门编写的 get_proof_withdraw_account 函数创建了一个验证 mock。与测试类似，verification mock 是一个函数的虚假的实现。目标是尽可能省略许多细节，仅建模与验证相关的那些方面。在我们的案例中，get_proof_withdraw_account 返回一个符号 ZK 证明，第一次初始化时使用非确定性值，但随后的调用总是返回相同的证明。

对于好奇的读者，我们在图3中展示了我们的 mock get_proof_withdraw_account 的完整代码。在我们解释代码之前，我们要强调，我们不期望 Solana 开发者编写这样的 mock。相反，我们计划扩展 Certora Verification Language 以允许用类 Rust 的语法编写规范。这将使 Solana 开发者更容易以直观的方式编写 mock。回到 mock 代码，我们使用两个实现“技巧”来模拟 mock 的预期行为：

1. 我们定义一个外部函数 CVT_nondet_pointer_withdraw_account_data，该函数返回指向 WithdrawData 的原始指针，后者是 process_withdraw 使用的 ZK 证明的类型。由于我们未提供其实现，SCP 必须假设返回的指针是非确定性初始化的。注意，第47行的假设限制指针为非空¹。
2. 我们定义一个全局变量 CVT_PROOF_WITHDRAW_ACCOUNT，它代表 ZK 证明。第一次调用 get_proof_withdraw_account 时，全局变量被初始化。

图3：get_proof_withdraw_account 的代码

注意：

这个 mock 并未描述 ZK 证明的任何细节。这是故意的，因为我们感兴趣的属性与 ZK 证明的内容无关。

下一幅图展示了如何使用我们的 mock 进行修改。提取证明的原始代码已在第444行被 mock 取代：

图4：修改后的 process_withdraw 使用 mock 来获取 ZK 证明

在我们在图1中编写的验证工具中，现在应该很容易理解为什么我们调用 mock get_proof_withdraw_account 来获取 ZK 证明，并从中获取其公钥。

最后，我们准备使用我们的验证工具运行 SCP。在之前的 帖子 中，我们解释了如何将验证工具与 SPL Token 2022 一起编译并生成相应的 SBF 代码。在这里，我们显示在 bug 修复之前，运行 SCP 的命令：

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

违反：proper_use_of_encryption_key_process_withdraw_account
proper_use_of_encryption_key_process_withdraw_account: 一个属性被违反
报告在 file:///Users/jorge/Certora-solana-program-library/token/program-2022/src/certora_files/emv-1-release-spl_token_2022.so-04-Aug--14-28/Reports

请记得，-solanaEntrypoint 选项告诉 SCP 验证过程应从我们的验证工具开始。

SCP 报告说属性已被违反。此外，它生成了一个包含关于违反的信息的报告（称为反例）。目前，反例以 Certora 内部表示（IR）的形式显示，因此不适合 Solana 开发者。我们正在努力改善这一点，通过使用 Rust 名称显示反例。

接下来，我们在 bug 修复后对 SPL 运行 SCP：

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

已验证：proper_use_of_encryption_key_process_withdraw_account
proper_use_of_encryption_key_process_withdraw_account: 在所有输入上成功验证属性

如你所见，SCP 能够证明修复后的代码满足我们关注的属性。

挑战与未来方向

在这一系列中，我们专注于合约的功能性属性。当然，还有其他与安全相关的重要属性。在 Solana 中，期望一条指令检查所有参数是否格式良好及其连接是否正确。例如，哪个帐户为创建其他帐户付费，哪个帐户签署了事务等。这通常很难检查。像 Anchor 这样的框架通过允许开发者以声明方式指定帐户约束来简化这一过程。原则上，可以使用 SCP 来检查 Anchor 生成的代码是否满足这些声明规范。

另一个在本系列中未讨论的有趣属性是关于检查 访问权限。例如，一个合约是否有权修改某些帐户数据。虽然 Solana Runtime 确保了访问权限，但如果 SCP 能够在部署之前静态检查这些权限，那将是显而易见的好处。请注意，在 Solana 中验证访问权限的任务比在其他区块链（如以太坊）中更容易。在以太坊中，合约可以操纵整个区块链的状态。然而，Solana Runtime 确保只有一组被读取/写入的帐户被传递给合约。这使得即使合约传递调用另一个合约的任务，也使访问权限验证的任务更容易处理（跨程序调用）。

Solana 有两种主要类型的帐户：程序 和 数据 帐户。前者存储可执行的 SBF 字节码，而后者存储应用数据。例如，可以通过拥有 N 个数据帐户来实现 N 个键值条目的映射。将数据与程序链接的一种常见机制是使用 程序派生地址 (PDAs)。当前，SCP 未能准确建模程序与其 PDA 之间的连接，但我们计划支持这一点。

另一个挑战是对 Solana 帐户的 序列化/反序列化 的精确建模。由于 Solana 缺乏可以在合约之间进行通信的通用格式，这些合约只会将帐户编码为字节数组。对序列化/反序列化代码的非常精确建模可能不具扩展性，而不精确的建模（例如，假设反序列化返回非确定性帐户）可能不足以证明所关注的属性。我们正在努力在合适的抽象级别建模序列化/反序列化。

结论

我们展示了如何在 SPL Token 2022 的保密扩展中使用 SCP。这确实需要使用验证 mocks 来建模难以分析的 Solana 组件。我们还强调了当前的挑战和未来的方向。

我们还想强调自动验证与手动审计相比的独特好处。

• 首先，SCP 可以正式保证某个属性始终存在，否则提供反例，可以用于修复 Bug 或规范。
• 其次，规范和 mock 是可重用的。与 process_withdraw 中描述的相同问题也在 process_empty_account 中被同一审计员发现。我们可以重用为 process_withdraw 编写的规范和 mock，以检查 process_empty_account 上相同的属性。
• 第三，如果代码被修改，则 SCP 可以重新检查该属性在新代码中是否仍然成立，而无需额外的手动努力。

这是我们关于 Solana 合约的形式验证系列帖子的结束。我们希望你喜欢它！

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

脚注

¹ SCP 还假设外部指针已正确分配。

参考文献

有关 SPL Token 2022 的保密扩展的所有详细信息：https://spl.solana.com/confidential-token/deep-dive/overview

在 Solana 中实现的公钥加密方案：https://spl.solana.com/assets/files/twisted_elgamal-2115c6b1e6c62a2bb4516891b8ae9ee0.pdf

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