形式化验证 第 3 部分 - Solana SPL 隐私性扩展的形式化验证

在之前的 文章 中，我们展示了如何证明 Mint 操作的正确性，该操作是 SPL Token 和 SPL Token 2022 的基本功能之一。在本文中，我们展示了如何使用 Solana Certora Prover (SCP) 来查找 SPL Token 2022 的 隐私性扩展 中的错误。

SPL Token 2022 的 隐私性扩展

隐私性(confidentiality)扩展的主要思想是允许在不真实地揭示其实际值的情况下，对账户余额做出声明。尽管这看起来很神奇， 零知识（ZK）证明 正好可以实现这一点。我们在此帖的最后提供了一个链接，以便你想了解更多关于 ZK 证明及其在 Solana 中的高效实现。

在本文中，我们重点关注SPL审计员在 process_withdraw 中发现的一个错误。其源代码可以在 这里 找到。该函数允许从账户中提取代币。由于实际余额是加密的，因此该函数依赖于 ZK 证明 来验证账户是否有足够的资金。一个关键的正确性属性是，与 ZK 证明相关联的公钥必须与从中提取资金的代币账户的公钥相同。这个属性在先前的 SPL Token 2022 版本中并未成立，被评为一个关键错误，因为可以从账户中提取任意数量的代币。错误修复可以在 这里 找到。

让我们看看我们如何利用 SCP 找到这个错误。如果你阅读过我们之前的 文章，你已经知道我们需要做的第一件事是编写一个验证工具。在之前的文章中，我们解释了什么是验证工具，并为 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 证明的公钥相同_。

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

为了理解验证模拟以及我们为何在此需要它，首先让我们描述图 2 中所示的 process_withdraw 的相关代码。

图 2：使用 ZK 证明检查账户是否有足够资金的 process_withdraw

第 444 行到 450 行获取 ZK 证明，声称代币账户有足够的资金。第 461 行到 465 行在加密余额上执行实际的提款操作，第 469 行到 471 行检查新的可用余额是否与 ZK 证明一致，否则将返回错误。关键的是，456 行到 458 行的检查在最初被遗漏，导致我们的属性被违反。

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

对于好奇的读者，我们在图 3 中显示了模拟 get_proof_withdraw_account 的完整代码。在解释代码之前，我们想强调的是，我们不指望 Solana 开发人员编写这样的模拟。相反，我们计划扩展 Certora 验证语言 ，以允许使用类似 Rust 的语法编写规范。

这将使 Solana 开发人员能够更简单、更直观地编写模拟。回到模拟代码，我们使用了两个实现“技巧”来模拟模拟的预期行为：

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 的代码

注意： 该模拟没有描述 ZK 证明的任何细节。这是有意的，因为我们感兴趣的属性与其内容无关。

下一个图显示了我们模拟使用中的变更。提取证明的原始代码在第 444 行被模拟替换：

图 4：使用模拟获取 ZK 证明的修改后的 process_withdraw

在我们图 1 中编写的工具中，现在应该很容易理解我们为何调用模拟 get_proof_withdraw_account 以获取 ZK 证明及其公钥。

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

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

Violated: proper_use_of_encryption_key_process_withdraw_account
proper_use_of_encryption_key_process_withdraw_account: A property is violated
Reports in 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 名称显示反例。

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

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

Verified: proper_use_of_encryption_key_process_withdraw_account
proper_use_of_encryption_key_process_withdraw_account: Properties successfully verified on all inputs

正如你所看到的，SCP 能够证明修复后的代码满足我们感兴趣的属性。

挑战与未来方向

在本系列中，我们专注于合约的功能属性。当然，还有其他非常重要的安全相关属性。在 Solana 中，指令应该检查所有参数是否格式正常并正确连接。例如，哪个账户为其他账户的创建付费，哪个账户签署了交易，等等。这往往并非易事。像 Anchor 这样的框架通过允许开发人员以声明的方式指定账户约束简化了这个过程.原则上，可以使用 SCP 检查 Anchor 生成的代码是否满足这些声明性规范。

本系列中没有涵盖的另一个有趣性质与检查 访问权限 有关。例如，一个合约是否有权修改某些账户数据。虽然访问权限由 Solana 运行时保证，如果它们可以在部署之前通过 SCP 静态检查，则显然会有明显的好处。请注意，验证 Solana 中的访问权限比其他区块链（例如以太坊）要容易得多。

在以太坊中，合约可以操纵整个区块链的状态。然而，Solana 运行时确保只有读取/写入账户集被传递给合约。这使得验证访问权限的任务更容易，即使一个合约间接调用另一个合约（ 跨程序调用）。

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

另一个挑战是对 Solana 账户的 序列化/反序列化 进行精确建模。由于 Solana 缺乏适用于合约之间通信的通用格式，这些合约仅以字节数组的形式对账户进行编码。对序列化/反序列化代码的非常精确建模可能无法扩展，而不精确建模（例如，假设反序列化返回非确定性账户）可能不足以证明感兴趣的属性。我们正致力于以适当的抽象级别对序列化/反序列化进行建模。

结论

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

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

• 首先，SCP 可以正式保证某个属性始终成立，否则提供一个可以用于修复错误或规范的反例。
• 其次，规范和模拟是可_r eusable_的。在 process_withdraw中描述的相同问题是由同一审计员在 process_empty_account中发现的。我们可以重用为 process_withdraw 编写的规范和模拟，以检查同一属性在 process_empty_account上。
• 第三，如果代码被修改，则SCP可以重新检查新代码上属性的有效性而无需额外的手动工作。

这是我们关于 Solana 合约的正式验证系列文章的结尾。我们希望你喜欢它！

如果你希望将 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

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