与 3MI Labs 和 Aligned 合作发现的 Succinct SP1 zkVM 中一个漏洞的责任披露，该漏洞由两个不同的安全漏洞相互作用而产生

TL;DR: 我们发现了两个安全漏洞，它们可以组合起来在 Succinct 的 SP1 zkVM 中执行漏洞利用，从而允许你生成虚假证明。在严重的情况下，这可能导致资金损失。这项发现得益于顶级研究机构 3MI Labs、Aligned 和 LambdaClass 之间的合作。这与我们之前在博客中告知 的安全漏洞不同，它强调了多个团队关注安全并努力简化代码库的重要性。有关漏洞利用的 PoC，请参见以下仓库。

LambdaClass 和 Fuzzing Labs 将投资进一步调查 zkVM 中的关键安全漏洞。我们认为，代码库变得过于复杂和过度设计，这导致出现大量错误。我们认为，如果我们不投资、不增加关注并简化代码库，那么整个行业将面临风险。业界在安全方面变得自满，并且受到业务决策的推动而匆忙投入生产使用，将这些安全问题抛在一边，这可能导致非常严重的后果。在这篇文章中，我们分析了 SP1 的案例，但我们认为所有 zkVM 的代码库都需要简化并遵循标准，从而降低攻击面。如前所述，我们将对不同的 zkVM 进行更彻底的研究。

简介

我们已经在多个工程项目中看到了漫长而复杂的代码库的开发，这些代码库具有太多的功能，并且文档和测试都很糟糕。有些人认为，拥有这样的代码库表明你很聪明，具有出色的编码技能，并且对所有事情都进行了深思熟虑。我们不这么认为：掌握的证明在于简单。错误总会在任何项目中发生，但是发生严重错误的机会会随着代码库的复杂性和长度呈非线性增长：越长越复杂，可能出现的错误和难以预测的行为就越多。在对 zk 虚拟机和证明系统进行分析的过程中，我们发现了两个安全漏洞，它们可以组合起来产生漏洞利用，从而允许恶意方证明虚假陈述。基本上，你可以为程序生成虚假证明并修改一些公共输入，如果在链上使用此技术来验证计算，则可能导致多种漏洞利用和资金损失。

从我们的角度来看，这些漏洞利用是由于代码库的复杂性，具有许多具有不同约束的文件以及添加了多个使代码库膨胀的功能和优化而引起的。我们还认为，当我们需要专注于提高其安全性和可审核性时，业务决策正试图将这些系统匆忙投入生产。我们认为，在设计、开发和测试可能在实际应用中使用的 zk 虚拟机时，需要更加谨慎，尤其是在资金面临风险时。

漏洞利用描述

在 sp1-sdk crate 的 3.4.0 版本中发现了两个错误，这是在我们开始分析时发布的最新版本。我们能够利用它们来生成任意程序的不正确执行的有效 SP1 证明，从而导致对任意语句（即使是不正确的语句）的通用伪造证明。

错误描述

本报告描述了两个错误：

• SP1-2.1：没有 COMMIT 系统调用的未约束的 committed_value_digest
• SP1-2.2：递归树第一层中未检查的 next_pc 条件

SP1-2.1：没有 COMMIT 系统调用的未约束的 committed_value_digest

当 SP1 执行器执行 guest 程序时，由调用 sp1_zkvm::io::commit() 产生的 COMMIT 系统调用（0x00_00_00_10）会延迟到执行结束，并且仅在 main 函数返回时才发出。

由于这些系统调用是唯一对 ExecutionRecord 的 committed_value_digest 产生约束的事件，因此这意味着如果程序的执行在 main() 的返回点之前停止，那么 COMMIT 系统调用将永远不会发出。因此，committed_value_digest 保持初始化为全零值，并且在证明生成期间不受约束。

在程序执行期间，这个提交值的摘要上缺少约束，引发了对 sp1-sdk 的验证器代码与“任意”程序的证明的兼容性的进一步疑问，但是探索这一点超出了本报告的范围。

SP1-2.2：递归树第一层中未检查的 next_pc 条件

在递归树第一层的验证代码中，如果一个 shard 被指示为包含“完整”执行，则不会检查条件 next_pc == 0。但是，此检查存在于其他递归约束中（例如，二合一证明压缩、字段切换包装、证明系统切换）。

当断言 is_complete 时，存在对其他代码路径执行的其他检查，但在递归树的第一层中缺少这些检查。这些检查可能对证明的可靠性至关重要，但未在我们的利用中使用。这些可以在 sp1_recursion_circuit::machine::complete::assert_complete（对于递归约束）和 sp1_prover::verify::verify（对于普通的、未压缩的验证）中找到。这些检查包括：

• 至少存在一个执行 shard
• (执行) shard 编号是连续的，并且从一开始，
• 叶子挑战者和最终重建挑战者匹配
• 延迟的证明摘要是一致的，并且
• 累积总和是一致的。

漏洞利用描述

最初，尝试利用 SP1-2.1 是通过在 main() 中显式发出 HALT（0x00_00_00_00）系统调用来实现的。

虽然这不是最终使用的方法，但我们注意到在 main 中显式发出此类 HALT 系统调用可能会合理地被认为是 guest 程序中的一种优化，例如，通过争辩说 main 中的提前停止是缩短程序执行跟踪并因此减少其证明计算时间的一种方式。这似乎是无辜的，但是 SP1-2.1 然后意味着在系统调用之前产生的公共值的摘要将保持不受约束。

但是，创建恶意 SP1 执行器就足以在任意 pc 值处停止执行 guest 程序。只要选择的 pc 值在 main() 的返回点之前，虚拟机就不会产生 COMMIT 系统调用。在此处提供的漏洞利用中，证明伪造是通过在程序到达 main 函数的开头时立即停止执行来产生的。

然后在返回生成的 ExecutionRecord 之前，恶意执行器可以自由地将 public_values: PublicValues 字段的 committed_value_digest 替换为任意值的摘要。这使得看起来好像 guest 程序在执行期间已提交到它。

然后，运行一个诚实的 CoreProver（sp1_prover::components::SP1ProverComponents::CoreProver），以使用恶意制作的 ExecutionRecord 生成一个 SP1CoreProof（sp1_prover::types::SP1CoreProof）。由于记录中没有包含 COMMIT 系统调用，因此更改后的 committed_value_digest（与程序提交的值的摘要不匹配）不会导致证明生成失败。因此，CoreProver 成功创建了一个包含两个 shard s1 和 s2 的 SP1CoreProof。

最后，创建一个恶意的 SP1Prover（sp1_prover::SP1Prover），并进行以下两个修改：

1. 丢弃 SP1CoreProof 的第二个 shard s2。
2. 在从剩余的第一个 shard s1 创建的 SP1RecursionWitnessValues 中，将 is_complete 标志设置为 true。然后，在生成用于使用 CompressProver 压缩 SP1CoreProof 的递归程序时，将使用此递归见证。

由于恶意执行器使用指向 main 开头的 next_pc 值停止了 guest 程序，因此第一个 shard s1 具有非零的 next_pc 值。但是，由于 is_complete 标志为 true，SP1-2.2 意味着 CompressProver 不会约束等式 next_pc ==0，从而导致生成没有错误的 SP1ReduceProof 证明。当由诚实的 prover 反序列化并提交以进行验证时，此 SP1ReduceProof 然后会通过 guest 程序的诚实验证。

漏洞利用演示

我们随附了错误报告，其中包含两个 artifacts，演示了如何利用这两个错误来提供任意程序的无效执行的有效证明。请参阅 代码的 repo。

该 is-prime 目录包含程序 (./is-prime/program) 的源文件和编译后的 ELF 版本，该程序检查从 sp1_zkvm::io 读取的数字的素数性，以及一个脚本 (./is-prime/script)，该脚本演示了 42-is-prime.proof (./is-prime/script/42-is-prime.proof) 是一个有效的证明，表明执行该程序导致 42 被验证为素数。

该 i-am-satoshi (./i-am-satoshi/) 目录包含此技术的可转移性的示例。在此，guest 程序使用独立的 bitcoin crate 来计算与作为输入给出的密钥对应的比特币地址，然后使用 sp1_zkvm::io::commit() 提交到生成的地址。运行相应的 验证器程序 (./i-am-satoshi/script/src/main.rs) 会发现该证明证明了对“创世中本聪地址” 1A1zP1eP5QGefi2DMPTfTL5SLmv7DivfNa 背后的密钥的了解。

这个概念证明说明了 SP1 验证器的任意语句证明，通过验证对在比特币创世区块中奖励地址的密钥的了解。要执行这些漏洞利用，需要在本地修改 prover 客户端。

后果和限制

虽然此漏洞利用中介绍的第一个程序足够无辜（42 显然不是素数），但第二个程序举例说明了更严重的后果。

任何区块链上任何地址的所有权证明都可以被伪造，并且会被天真的验证者接受。我们提请注意，程序本身没有被修改。创建证明伪造的所有修改都是在 proving 客户端本地执行的，这意味着此伪造方法可以推广到任意 guest 程序。

我们注意到 SP1-2.2 是仅限于递归树第一层的错误，并且证明的后续递归证明将失败，因为当 is_complete == true 时，ShrinkProver 正确地约束了 next_pc == 0 检查。

但是，诚实验证者代码 (./is-prime/script/src/bin/verifier.rs) 不知道它反序列化的证明的种类，这意味着恶意的 prover 没有被迫进一步减少或包装伪造的证明，然后再将其提交给运行来自 sp1-sdk crate 的 Rust 验证器的系统进行验证。

可能的缓解措施

缓解 SP1-2.1

缓解 SP1-2.1 需要确保 committed_value_digest 在证明系统中受到约束，即使没有发出 COMMIT 系统调用也是如此。

此缓解措施的任何实现都会与当前实现冲突，因为当前实现假定 committed_value_digest 只写入一次。一个具体的提案需要进一步探索可能性，这超出了本报告的范围。

缓解 SP1-2.2

最终，应该对递归程序的代码进行修补，以便 CompressProver 在递归树的第一层中应用 next_pc == 0 约束（以及用于完整程序的其他相关约束），就像在其他递归程序中一样。

作为对当前可接受的验证密钥进行热修复（不会造成重大更改），由于 next_pc 值可以作为证明的一部分进行访问

公共值，验证器的 Rust 代码应检查它是否为 0，即使这在证明系统中没有受到约束也是如此。此热修复程序将进一步使现有的验证器能够检查此错误是否由仍在存储中的证明触发。

总结

我们与 3MI Labs 和 Aligned 一起，在 Succinct 的 SP1 zkVM 中发现了两个安全错误，并展示了如何使用它们来执行漏洞利用，以生成诚实验证者会接受的虚假证明。由于这些漏洞利用不需要更改程序的代码并且是在本地完成的，因此它们可以在没有天真的验证者怀疑它是恶意证明的情况下使用。我们认为，代码库的复杂性和长度以及不清楚的文档会导致错误的扩散，并且我们应该更加努力地简化代码库并关注安全性，而不是由于业务方面的考虑而匆忙投入生产，尤其是在资金可能面临风险时。

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