解决SNARK中的漏洞：未来的道路

在区块链世界中，SNARKs 相较于今日的透明账本，承诺了无与伦比的可扩展性和增强的隐私性。然而，现实情况是，SNARK 的实现充满了漏洞，提供的安全性靠遮掩，而不是可靠的加密保证。实现真正的安全性需要形式化验证——即证明 SNARK 系统是没有漏洞的。本文简要回顾了 Jolt，我们的 RISC-V zkVM 的进展，然后讨论我们在形式化验证方面的努力。

zkVMs 和 Jolt：简要回顾

zkVMs 是 SNARKs，允许不可信的证明者证明其正确地在证人上运行了某个指定的计算机程序，而程序作为符合特定指令集架构（ISA）如 RISC-V 的 字节码 进行指定。

zkVMs 提供了可用且可维护的 SNARKs 最有前景的路径。它们允许开发者使用任何他们喜欢的高级语言编写程序，只要该语言配有能够编译成 ISA 字节码的编译器。开发者无需直接以电路或约束的形式表达计算，甚至无需在“zkDSLs”中进行表达。构建 zkVM 的人将一次性处理约束系统和电路的复杂性，这意味着任何人都可以在不需要了解证明机制实际工作原理的情况下使用 zkVM。

2024年4月，我们 发布 了初始实现的 Jolt zkVM，以 RISC-V 为目标，并展示了其性能与其他替代方案的良好比较。我们初步调查的结果已被若干 其他 基准测试 确认。自那以来，我们已显著减少 Jolt 的证明大小（从几MB减少到200KB，甚至在稍微增加证明时间的情况下降至35KB），并加入了对 Rust 标准库和 RISC-V 乘法扩展 的支持等额外功能。

不久之后，我预计 Jolt 将成为唯一能够在资源受限环境中证明的 RISC-V zkVM（低于2GB 的证明者空间，而 RISC Zero 为8-16GB，SP1 则更高），同时还能同步实现先进的证明者时间。

不过这篇文章并不是关于 Jolt 的性能或功能支持的。它关注的是一个更重要的话题：正确性 和安全性。 本文概述了我们实现 形式化验证 Jolt 实现的 长期目标的路线图，并描述了我们在这一路径上已采取的初步步骤。

SNARKs 的一个关键风险

漏洞与灾难

SNARK 工具链中的任何轻微漏洞都可能导致灾难性的安全失败。例如，单个缺失或不当指定的约束可能意味着证明者并不真正知道它声称知道的证人（例如，实际上不知道控制辟明交易的钱包的私钥）。

在我们对工具链的完全无漏洞有信心之前，使用 SNARKs 的项目无法靠 SNARK 本身实现 真正的 安全性。充其量，它们由遮蔽保护：发现漏洞可能需要专业知识（识别缺失或错误指定的约束，或用于部署 SNARK 的工具链中的其他错误）。但漏洞就在那里——这很可能意味着一个有动机的对手可以找到令人信服的虚假陈述证明。

最坏的情况是，我们 认为 我们的 SNARK 工具链没有漏洞，因此停止将 SNARK 视为多层深度防御体系中的一层。这些其他安全层将是半中心化的。在 rollups 的上下文中，这可能意味着使用允许名单确定谁可以提交证明、使用 的 TEEs ，或一个可以“撤销”对有缺陷证明的接受的安全委员会，可能会在网络参与者认为已经确认的许多交易中造成大量成本和混乱。

长期前景光明，但遥远

从长远来看，zkVMs 不仅对 SNARK 的可用性有影响，还对正确性有影响。如果我们可以确保 zkVM 本身是无漏洞的，并确保 zkVM 应用的程序字节码正确实现了预定的证人检查程序，则整个工具链也将是无漏洞的。

以太坊基金会正在 大量投资 把这个终局变为现实——但这 还要数年。 实际上，我认为在五年后，我们仍然可能对任何具有表现能力的 zkVM 工具链的实际无漏洞性缺乏强烈信心。

今天，zkVM 工具链几乎肯定充满了漏洞。 我们应该停止假装它们不是。为了让人们意识到它们有多复杂，考虑以下几点：

Jolt 的代码库已达到 34,000 行 Rust 代码（若不计算 SDK 或 RISC-V 模拟器，它大约 “仅” 25,000 行），此外，它使用了一些来自 arkworks 的功能，即 域、群 和 配对 操作。 SP1 的代码库超过 60,000 行 Rust 代码（如果包括它调用的证明系统 plonky3，会接近 100,000 行），再加上数千行的 Go 代码，以及几百行的汇编代码。 RISC Zero 的代码库更大，有超过 100,000 行 Rust 代码，几乎 200,000 行的 C++，150,000 行的 CUDA，400 行的汇编，还有更多。（所有这些统计信息均使用 cloc –vcs git 命令计算的代码行数。）

当然，这些代码行中的大多数用于实现 zkVM 验证者，但对于安全保证而言，只有 zkVM 验证者 需要正确实现，而验证者可以比证明者简单得多。尽管如此，这些统计数字给出了这些系统复杂性的一个感觉，即使是验证者的实现也是数千行代码。

鉴于这种情况，简洁性在任何 zkVM 中都是一项重要美德，而我们坚信 Jolt 是如今 RISC-V 的 最简单的 zkVM。但是，形式化方法并不是一种可以轻易应用于任何软件并神奇地消除所有漏洞的魔法棒。为了获得任何形式保障的 zkVM 工具链的端到端正确性和安全性，必须克服重大技术挑战。zkVM 中的简洁性不仅在短期内重要；它将促进这些形式验证工作，并在未来许多年中保持其美德。

通往无漏洞 Jolt 的路线图

短期努力（已完成和进行中）

在中期，审计和漏洞挖掘工作是不可替代的。 Jolt 还未经历完整的审计，但它已经接受了大量审查。最近， zkSecurity 团队在 Jolt 中发现了几个漏洞。这些漏洞并不在证明机制的“核心”中，而是有关输入和输出是如何处理的，Jolt 如何确保证明者实际执行了计算机程序的完成而不是“提早停止”，以及允许证明者指定某些参数，反而应该由验证者或其他诚实方来指定。（有关漏洞及其发现方式的更多细节，请参见 zkSecurity 的 配套帖子）。

除了漏洞发掘工作外，我们已经在（非常）漫长的形式化验证 Jolt 实现的道路上迈出了第一步。首先，Jolt 简单性的一个主要原因是其以查找为中心的设计：Jolt 并未将 VM 的每个基本指令表示为电路或约束系统，而是“分解”每个指令为少量的小查找，并使用我们的 Lasso 查找论证 来可验证地执行这些查找。与 Carl Kwan 和 Quang Dao 合作，他们领导 Jolt 的形式化验证工作，我们已使用 ACL2 自动定理证明器 来 验证 Jolt 的查找分解的正确性。这一形式化高度自动化，这意味着这些技术将易于扩展至不同且更丰富的 ISA，若社区日后对此表示关注。这些验证工作也通过自动识别我们为少数基本 RISC-V 指令执行的一些不必要查找，推动了 Jolt 的性能改进。

其次，Quang 和合作者 Gregor Mitscha-Baude 来自 zkSecurity 和 Devon Tuma 正在使用 Lean 验证 Jolt 核心的 Spartan、Lasso 和 Spice 多项式 IOPs 的健全性。这项工作将广泛延伸到实践中使用的所有 PIOPs，而不仅仅是 Jolt 中使用的那些。这项工作预计将在2025年中期完成。与 Jolt 一样，这项工作是在公开中进行的，你可以通过访问 Quang 的 ZKlib 仓库 来跟踪他的进展。这一努力是最近得到以太坊基金会支持的 形式化验证项目 的资金支持的。

第三步是验证（假设上述多项式 IOP 的健全性）在 Jolt 中应用于 Spartan 的约束系统，加上 Jolt 对 Lasso 和 Spice 应用的查找和对此的读/写内存，能共同捕获 RISC-V ISA。这项工作的组成部分首先是在 ACL2 中构建一个形式的 RISC-V 模型（已完成），然后使用 ACL2 验证模型与 Jolt 的约束、查找和内存操作组合的等价性（当前正在进行中）。

长期努力

聚焦于定理证明器

我们计划将所有 ACL2 形式化转移至 Lean。Lean 较 ACL2 更新且不够成熟，但在数学上有更多社区支持/库，以及在 SNARK 社区中更大的发展动力（例如，以太坊基金会的 zkEVM 验证工作 的大部分预计会在 Lean 中进行）。我们最初的努力主要使用 ACL2，很大程度上是为了利用其对 自动化技术如位炸裂 的广泛支持（例如，通过将位向SAT求解器传递来进行比特量子推理）和重写。 Lean 最近 增加了支持 了初步位炸裂，因此从长期来看，可能有意义将整个努力转向 Lean。

验证 Jolt 的实际实现

一个主要的长期挑战是实际验证 Jolt 验证器的 Rust 实现（更不必提同样的链上实现，通过 Solidity 或 EVM 字节码）。我们在这方面尚未真正取得进展。 Jolt 实际上只是一个用于证明 RISC-V 程序正确执行的多项式 IOP，目前我们的工作主要集中在确保多项式 IOP 是安全的，而不是 验证 Jolt 的 Rust 实现是否正确实现了多项式 IOP。迄今为止的主要例外：通过模糊测试，我们验证了在 ACL2 中形式化的查找分解与 Jolt 的 Rust 代码库中实现的分解相匹配。

在这里，我们需要良好的工具来确保 Rust 代码的正确性（根据特定规范）。为实现这一目标，各种潜在的方法可用于启用此功能，包括 限制算法Rust（Restricted Algorithmic Rust (RAR)）、Aeneas、Verus 以及 其他 工具。另一种可能的方法是规避源自 Rust 编程问题。许多定理证明器（例如 ACL2、Lean、Coq）支持代码提取到某些目标语言（例如 OCaml、C、Lisp），并且 Rust 未来可能得到支持。代码提取的一个主要问题是，通常“交叉编译”步骤本身并没有经过验证。 ACL2 的一个独特优势是，定理证明器中的执行与原生 Common Lisp 执行是相同的，因此在 ACL2 中的“形式验证过的 Jolt 验证者”可以根据需要调用，无需交叉编译到目标语言。整体来说，我不会惊讶如果我们在一年半或更久的时间后才认真打算这一必要方向。这个时间线的另一个好消息是， Rust 工具将在此期间实现显著成熟。

与此同时，在使用 Lean/ACL2 验证 Jolt 的多项式 IOP 和约束系统的各种组件的正确性时，我们将广泛测试验证模型与 Jolt 的 Rust 代码的一致性。这是我们在验证 Jolt 的查找分解时所采取的方法。虽然这远未达到“形式验证 Rust 验证者”的最终目标，但它让我们对 Jolt 代码库不同部分的正确性建立了信心。

用于 Jolt 所有“约束”的 DSL

与其他 zkVMs 不同，后者主要使用所谓的 Plonkish 或 AIR 约束系统来捕获 VM 执行，Jolt 使用 R1CS 和通过 Lasso 和 Spice 的“离线内存检查”技术的组合，检查证明者是否正确地从只读内存（即查找）和读写内存（即寄存器和 RAM）中执行读取。

目前，Jolt 实现以特定方法指定了上述约束/查找/内存操作。对于 R1CS 的规范，我们最初使用 Circom，但由于开销不可接受，我们手动制作了自己的 R1CS 规范语言，并将其 纵向集成到 Jolt。同样，寄存器和 RAM 的查找、读取和写入通过内部 API 进行规范。

为了可维护性和在 Jolt 发展过程中持续验证，在此情况下最好有一个单一 DSL，可以清晰地捕获 R1CS、查找、寄存器/RAM。这对于预编译规范也会很有帮助。（像 Jolt 本身一样，Jolt 中的预编译将由 R1CS、查找和算术电路的组合组成，即将应用于 GKR 协议 的组合。）我们正在与 Galois 为此方向采取步骤。

形式化验证和控制证明者内存

形式化验证工作的一个挑战是今天的 zkVM 中广泛使用 SNARK 递归。为了保持证明者的空间是有限的（即避免需要 TB 级空间来证明即使是小型程序的执行）并减少证明大小，今天的标准程序是将 VM 执行分成“分片”，证明每个分片的正确执行，然后递归聚合证明。这需要将 SNARK 验证者转化为电路或约束系统，并证明一个人知道这个电路的满足赋值。电路规范中的任何错误都可能导致灾难性的安全失败。从可用性的角度来看，递归使公众很难告知实际正在验证的陈述。不再是证明者简单地证明：“我正确运行了这个计算机程序。”而是证明者证明：“我知道许多证明，每个分片 ， 证明每个分片都正确执行，并且分片 i 结束时机器的状态与分片 i +1 开始时的状态相匹配。”

至少对于基于和检查的 SNARK，如 Jolt，实际上已经知道如何在没有 SNARK 递归的情况下保持证明者的空间有界 处理。我们将在即将到来的电子打印中详细描述 Jolt 中的细节，并已开始实施这样的非递归空间受限证明者。实现这样方法的一个高性能实施将需要重大工程努力，但最终将获利，促成更简单、更易验证的实现。

折叠

从长远来看，我预计对 SNARK 证明者的“非递归空间控制”将是一种有效的方法，以在使用如 Ligero、Brakedown 或 FRI-Binius 的哈希承诺方案时实现简单且具有性能的证明者。但对于 Jolt 当前支持的椭圆曲线承诺方案， 折叠 是最大限度减少证明者空间而保持证明者快速的正确方式。由于折叠固有地涉及递归，因此将需要形式验证 Jolt 验证者电路表示的正确性。这个任务可能复杂，但将因来自 zkEVM 形式验证项目的新工具而受益。

（我并不觉得整合折叠到 Jolt 会有太大难度，但由于它在复杂验证过程中应用递归证明，确认其正确性会面临挑战。幸运的是，许多工具正在开发以帮助完成这一任务。）

验证承诺方案和 Fiat-Shamir

简洁议论通常由两个组成部分构成：PIOP 和多项式承诺方案。结合在一起，这会生成一个简洁的 交互式 论点，然后通过 Fiat-Shamir 变换 将其呈现为非交互式。上述努力虽然形式验证了 Jolt PIOP 的健全性，但本身并不足以保证 Jolt SNARK 的安全。我们还必须验证 Jolt 支持的多项式承诺方案是安全且正确实现的，并亲自验证将 Fiat-Shamir 应用于结果简洁论证是安全和正确实现的。这是 Quang 和他的合作者在 Zklib 工作的未来目标，即不仅验证 PIOPs 的健全性，还验证多项式承诺方案及 PIOP 到 SNARK 的变换。

其他方向

验证的字节码

一些项目通过讨论从高层语言到 RISC-V 字节码的编译器中的漏洞，批评了 RISC-V zkVMs，并对 Rust 作为高级语言表达了不满。我们的观点是，如果想要经过验证的 RISC-V 字节码，那么应直接验证字节码，或者使用经过验证的编译器。如果不喜欢 Rust 作为高级语言，那就可以自由使用任何其他能够编译成 RISC-V 的高级语言。

当然，额外的工具以生成经过验证的 RISC-V 字节码对 zkVM 将大有价值。但这不在 zkVM 本身的范围内。zkVM 的工作是确保它所接收到的字节码正确执行。

通过 Jolt 的 EVM 验证实现与预编译

RISC-V zkVMs 是构建 zkEVMs（EVM=以太坊虚拟机）的极具潜力的工具。 Jolt 非常适合这一任务，但为了实现最佳性能，这将涉及在 Jolt 中整合几个预编译（并正式验证其实现确实捕捉了 EVM 语义）。这在 Jolt 的路线图上，形式验证部分将能利用以太坊基金会 zkEVM 形式验证项目的其他工作。

\\*\

我对急于部署 zkVM 而忽视潜在漏洞的情况表示严重担忧。通往无漏洞 zkVM 的道路漫长，我们在这条路上应当极为谨慎。不过，最终我们将到达那儿，而在此过程中开发出的方法和技术将在计算机科学和数学领域带来丰厚回报，远超 SNARK 设计。

\\*\

Justin Thaler 是 a16z 的研究合作伙伴，并且是乔治城大学计算机科学系的副教授。他的研究兴趣包括可验证计算、复杂性理论和针对大规模数据集的算法。

\\*\

该内容仅在所示日期有效。该材料中表达的任何预测、估计、预测、目标、前景和/或意见均可能会有所变化，恕不另行通知，可能与他人表达的意见相悖。有关其他重要信息，请参见 https://a16z.com/disclosures/。

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