塑造现代zkVM的项目——第一部分：ZKSECURITY
- zksecurity
- 发布于 2025-02-27 18:49
- 阅读 379
本文介绍了零知识虚拟机（zkVMs）的概念，zkVMs 利用零知识证明（ZKPs）来验证在特定指令集架构上执行的计算的正确性。文章回顾了zkVMs的基本原理，并讨论了多个对zkVMs的设计和发展产生重大影响的项目，包括vnTinyRAM、Cairo、RISC Zero zkVM、Jolt等，并且 zkSecurity 正在开发 zkVM 的形式化验证框架。
零知识虚拟机 (zkVMs) 利用零知识证明 (ZKPs) 来验证在特定指令集架构上执行的计算的正确性。实际上，zkVM 允许你用熟悉的级语言（例如 Rust 或 C）编写程序，而无需处理 ZKP 的细节。通过抽象这些复杂性，安全的 zkVM 可以为任何应用程序生成和验证证明。
在这篇文章中，我们将简要回顾 zkVM，并讨论几个对 zkVM 的设计和演进产生重大影响的项目。 我们要强调的是，这里讨论的项目列表既不详尽，我们也不会深入研究太多的技术细节。 相反，这篇文章标志着整个 zkVM 格局及其技术细节系列的第一部分。 对于围绕安全的介绍，我们强烈建议你看看我们关于 zkVM 安全 的博文。
现在，事不宜迟，让我们直接开始吧，好吗？
zkVM 简要回顾
诸如以太坊之类的区块链协议通常被描述为“互联网计算机”——每个人都可以通过安装自己的应用程序和使用彼此的应用程序来使用的计算机。 然而，今天的互联网计算机存在一个问题： 为了确保计算机没有出错，每个用户都被迫重新执行所有内容。 听起来像是一件相当笨拙的科技产品，不是吗？ 但不要害怕。这种情况即将改变！
最近围绕 ZKP 的进展使我们能够通过计算完整性来增强这些互联网计算机。 换句话说，只有计算机才需要计算。 由于密码学的存在，你和我可以向后靠并信任结果！
这就是 zkVM 发挥作用的地方。 但在我们超越自身之前，让我们简要回顾一下通用 ZKP 系统的低开发级别：算术电路。
算术电路是一种中间表示，它表示一个实际的电路，但使用数学方法，以便我们可以使用证明系统来证明它。 通常，你可以按照以下步骤来使用通用 ZKP 系统：
- 获取你喜欢的程序
- 将其编译成（算术）电路
- 以与执行程序相同的方式执行电路（同时记录每个步骤的内存状态）
- 使用你的证明系统来证明执行
算术电路实际上是什么样的？ 嗯，它看起来像一个电路！ 它有门和线，尽管它的门不是典型的电路门，例如 AND、OR、NAND、XOR 等。 相反，它有算术门： 一个门用于将两个输入相乘，另一个门用于将两个输入相加。
_来源：现实世界密码学_
好了，有了这些，让我们来谈谈虚拟机（VM）吧。 虚拟机通常可以分解为三个组件：
- 一些可用于存储和读取值的内存。（例如，如果你将两个值相加，你从哪里读取这两个值？你又在哪里存储结果？）
- 一组人们可以用来形成程序的指令。
- 一些可以解释这些指令的逻辑。
换句话说，虚拟机看起来非常像这样：
for instruction in program:
parse_instruction_and_do_something(instruction)
这个循环通常被称为 fetch-decode-execute cycle，因为每个指令都是从内存中获取、解码然后执行的。例如，使用 Ethereum VM (EVM) 支持的指令，你可以编写以下程序，该程序利用堆栈来添加两个数字：
PUSH1 5 // 将 5 压入堆栈
PUSH1 1 // 将 1 压入堆栈
ADD // 将从堆栈中删除这两个值并压入 6
POP // 将从堆栈中删除 6
好吧，那么 zkVM 呢？
从外部来看，zkVM 与 VM 非常相似： 它执行程序并返回其输出。 开发人员仍然可以访问同一组指令，与大多数虚拟机一样，这些指令通常只是更高级语言（可以编译成这些指令）的基础。
但是：zkVM 还会返回程序执行正确性的加密证明，用户可以验证！
查看 zkVM 内部会显示一些算术电路——还记得我们上面讨论的那些吗？ 这些算术电路“简单地”实现了我们的 VM 循环：
for instruction in program:
parse_instruction_and_do_something(instruction)
我们在这里用双引号将“简单地”括起来的原因是，在实践中实现这个循环远非简单。 但这就是 zkVM 背后的基本思想。
后，值得注意的是，还存在其他与计算完整性密切相关但不应与 zkVM 混淆的方法。 例如：
- Aleo VM — 一种中间表示，编译器稍后将 VM 指令转换为实际电路。
- zkLLVM — 通过将 LLVM 的中间表示直接编译到电路中来定位高级编程语言。
- Lurk — 通过连续尝试按照一组简单的规则来减少程序，直接证明评估程序的抽象状态机，从而绕过任何编译阶段。
但更多内容将在本系列的后续文章中…… (⌐■_■)
好了，既然我们对 zkVM 有了很好的了解，让我们仔细看看促成我们今天成果的一些项目！
OG zkVM
由 Ben-Sasson、Chiesa、Tromer 和 Virza 于 2013 年首次发布 Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture 是篇文章，提供了 zkVM 的实用构造。 正如标题所示，本文中描述的机器遵循 von Neumann architecture，即程序和数据都存储在同一内存中。 由于大多数现代 CPU 都基于这种范例，因此理论上，任何可以在经典计算机上运行的程序也可以在此架构上运行。
本文介绍了其自己的 RISC architecture，称为 vnTinyRAM，并展示了移植到目标此指令集的 C 编译器。 证明系统旨在验证程序执行的正确性，多可以执行固定数量的步骤，其基本思想是将电路构建为重复的状态转换函数，展开直到达到指令计数限制。 值得注意的是，这导致了有界 zkVM，其中证明仅涵盖预定数量的周期。 许多人认为 zkVM 本质上是无限制的，但 vnTinyRAM 的设计施加了固定的周期限制，这与 Cairo 等更现代的设计形成对比，我们将在下一节中更深入地讨论 Cairo。 与许多其他现代 zkVM 一样，Cairo 利用 STARK，它可以根据所需的周期数动态缩放，有效地启用无界 zkVM。 但我们跑题了……
vnTinyRAM 的创建为该领域树立了强大的先例，表明可以使用 ZKP 安全有效地验证现实世界的计算。 为了完整起见（双关语），我们还应该提到，后的分析发现 vnTinyRAM 的 SNARK 中存在一些疏忽。 虽然这些微小的错误实际上具有严重的安全性影响，但可以在后的修订中快速修复它们。 要阅读有关这些问题及其解决方案的信息，我们建议你查看以下两份报告：
用于 STARK 的 Von Neumann
在 vnTinyRAM 推出八年后，Cairo 标志着现代 zkVM 发展的下一个重要里程碑，它推出了第一个高效且实用的 von Neumann 架构，该架构可以与 STARK 证明系统一起使用来生成计算完整性证明。 Cairo 这个名称自“CPU AIR”，其中 AIR（算术中间表示）指的是用于 STARK 的算术化。 换句话说，Cairo 是一种实现 CPU 概念的 AIR。
一些说明：
- 如果你不熟悉算术化的概念，我们的 1 小时 arithmetization course 将让你快速入门。
- 如果你对形式化方法感兴趣，你可能还想查看 StarkWare's formal analysis 他们使用 Lean 3 对提取-解码-执行逻辑的分析。
- Bobbin Threadbare 的 Distaff 是一个基于 STARK 的 VM，它的发布时间甚至比 Cairo 还要早。然而，它从未达到可用于生产的状态。不过，它是 zkVM 历史上一个有趣的部分。有关更多详细信息，请访问 original post on EthResearch 和 Distaff repo。
Cairo 具有独特的内存模型，该模型利用置换和查找技术来强制执行自定义约束，类似于在 plookup 等查找协议中看到的方法。
来源：通过使用所谓的内置函数（直接实现为方程组的预定义操作），Cairo 成为了第一个在 zkVM 中引入预编译概念的项目。 这些内置函数使 Cairo 能够进一步程度地减少通常涉及将常见操作（例如哈希函数）转换为多项式约束的开销。 此外，应该注意的是，Cairo 使用自定义Instruction Set Architecture (ISA)，该 ISA 专为 zk 证明环境而设计，使其与其他基于 RISC-V 的系统和 zkEVM 等方法区分开来。 （稍介绍。）
后，请记住，Cairo 的设计充分利用了 STARK 的灵活性来支持无界 zkVM，其中电路可以根据程序终止所需的周期数动态缩放。 这与有界系统（如面提到的 vnTinyRAM）形成对比，后者仅将执行跟踪展开到固定的指令计数。
如果你想了解更多关于 Cairo 的信息，我们强烈建议你查看我们的 STARK book 的相关章节。
集成 RISC-V
RISC Zero zkVM 标志着 zkVM 发展的另一个重要里程碑，因为它是第一个集成 RISC-V architecture 的 zkVM。它的设计基于三电路架构：两个基于 STARK 的电路和一个 SNARK 电路。 更具体地说，首先执行给定的程序，生成多个“段”，然后使用 STARK 证明每个段。 后，所有段证明都使用 STARK 聚合到单个证明中。 后，使用 SNARK 缩减得到的证明，使验证更高效。
这种方法通常被称为延续，具有以下几个优点：它允许通过在多台机器上分发段来并行化证明过程，启用证明生成暂停和恢复，并保持内存需求固定，而与整个程序长度无关。通过延续，程序可以根据需要运行时间，同时保持高效的证明生成。
来源：RISC Zero Study Club 的 presentation on continuations
此外，RISC Zero 还优化了其 GPU 证明设计，并集成了 SHA-256 和 256 位模乘等常见操作的预编译，从而提高了性能，而无需更改底层的证明系统。后，RISC Zero zkVM 在 Rust 生态系统中具有广泛的兼容性，确保许多现有的 Rust crate 可以在没有额外配置的情况下与该系统一起使用。
通过查找参数优化 zkVM
Jolt (Just One Lookup Table) 及其配套论文 Lasso，它们于 2023 年一起发表，为 zkVM 引入了一种新的前端技术，该技术利用查找参数来简化程序执行的表示。虽然 Lasso 侧重于引入一种的查找参数系列，但 Jolt 详细介绍了如何使用 Lasso 构建 RISC-V zkVM。Jolt 没有生成一个电路来逐步选择和执行每个指令，而是用对一个的预计算表的单次查找替换了执行步骤。例如，对于一个对两个 64 位输入进行操作的 RISC-V 指令，人们可以想象一个包含 2128 个条目的表。然而，由于其结构化的设计和可分解性，这个表永远不会完全物化，并且它的属性允许高效处理。
Jolt/Lasso 的结果特别令人印象深刻的是，它实现了 Barry Whitehat 在 2022 年底发布的 the lookup singularity 的愿景。该愿景的目标是将任意计算机程序转换为仅执行查找的电路，以提高前端的性能、可审计性和正确性的形式验证。
说到可审计性：Jolt 的主要卖点之一是代码库的简洁性。虽然其他 zkVM 通常需要数万行 LOC，但 Jolt 是用不到 25,000 行 Rust 实现的。
要深入了解 Jolt zkVM，请务必查看我们关于该主题的其他博文：
- A Challenge on the Jolt zkVM
- Improving the Security of the Jolt zkVM
- A Technical Dive into Jolt: The RISC-V zkVM
的图 2 Jolt paper: 使用离线内存检查和查找来证明 CPU 执行的正确性
其他有影响力的 zkVM 项目
zkVM 格局正在迅速发展，有许多值得探索的值得注意的项目。虽然我们将在的文章中介绍它们，但这里有一个非详尽的列表（按任意顺序），供你在此期间查看。
- Valida - 基于 Plonky3。实现自定义 ISA 并与 LLVM 工具链集成。
- Scroll - 为 Scroll zk-Rollup 提供支持的 zkEVM。
- SP1 - 基于 Plonky3。实现类似 RISC-V 的 ISA。
- Nexus - 专注于并行化。实现类似 RISC-V 的 ISA。
- zkMIPS - 基于 Plonky2 和 MIPS 微架构。
- zkWASM - 支持 Web Assembly 的 zkVM。
- EraVM - 为 ZKsync 协议提供支持的 zkEVM。
- Miden - 基于 STARK 证明的 zkVM。
- Ceno - 专注于分段和并行化。
- zkMove - Move 智能合约的计算完整性。
- o1VM - 嫁接到 Kimchi 证明系统上的 MIPS zkVM。
- Linea - 为 Linea Layer2网络提供支持的 zkEVM。
zkSecurity 正在进行的工作
在 zkSecurity，我们目前正在使用 Lean 4 开发用于 zkVM 的形式验证框架，作为 Ethereum’s zk(E)VM Formal Verification Project 的一部分。我们的框架 clean 是一种嵌入式 Lean DSL，用于编写以 AIR 算术化为目标的 zk 电路。我们打算将 clean 构建成一个通用的 zk 框架，该框架可以针对所有算术化，并为整个生态系统生成经过形式化验证、无错误的电路。有关更多详细信息，请务必查看我们的 clean GitHub repo。
感谢 François Garillot、Ventali Tan 和 Jerry Kwok 的反馈和评审。
- 原文链接： blog.zksecurity.xyz/post...
- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
