介绍zkvmBlast：以太坊zkVM的差分模糊测试框架 - ZK/SEC季刊

liumuhui 3小时前阅读数 1 #区块链

zkvmBlast · 第 1 部分（共 1 部分）

介绍 zkvmBlast：面向以太坊 zkVM 的差分模糊测试

今天，我们发布 zkvmBlast，这是一个面向 RISC-V zkVM、与具体 zkVM 无关的差分模糊测试器。它接收一个程序，在多个 zkVM 和一个参考模拟器上运行，并报告每一个重要的不一致。它主要寻找两类 bug：soundness bug（即证明者能够让验证者接受某个虚假陈述）和 completeness bug（即合法程序完全无法被证明）。这套框架还能捕获 executor-correctness bug，也就是 zkVM 自身的执行在任何证明发生之前就已经偏离了 RISC-V 规范。这项工作部分由以太坊基金会资助。

到目前为止，这些测试活动已经在 SP1、Pico 和 OpenVM 中发现了七个不同的 completeness 和 correctness bug，均已负责任地披露给相关团队，此外还复现了一个已知的 RISC0 soundness bug。本文介绍了什么是 zkVM、为什么它们的正确性对以太坊变得越来越关键、为什么 completeness 理应得到比现在更多的关注，以及 zkvmBlast 针对这些问题做了什么。我们将在后续文章中深入介绍为 zkvmBlast 开发的各种具体技术。

zkVM 及其在以太坊未来中的角色

zkVM（零知识虚拟机）让你可以用 Rust 这类常规语言编写程序，将其编译为标准的指令集（如今几乎都是 RISC-V），并生成一个简洁的证明，证实该程序确实运行过并产生了给定的输出。任何人都可以在不重新运行程序的情况下，以极低的成本验证该证明。如果你想要一份合适的入门介绍，我们写过两篇：zkVM 安全：哪里可能出错？和塑造现代 zkVM 的项目。

直到不久前，zkVM 还只是应用层组件，例如，rollup、bridge 或 coprocessor 可以使用 zkVM 来压缩计算。这种情况正在改变。以太坊基金会正在推动以太坊本身的“snarkification”，这一方向由 Vitalik Buterin 在“The Verge”中提出，即用一个有效性证明来证明普通区块，从而在验证链时不再需要重新执行每一笔交易。主要要求是**“实时”证明**：在普通的硬件上、在一个 slot 内证明绝大多数主网区块。1

这已经不再是遥远的设想。Ethproofs 是以太坊基金会的一个项目，它通过一个公开排行榜追踪真实主网区块在各 zkVM 和 prover 上的证明情况，像 L2BEAT 追踪 rollup 一样衡量延迟和成本。与此同时，EF 的 zkEVM 团队也在开展自己的基准测试工作，重点针对最坏情况下的对抗性区块，而不是普通区块。这两项工作都依赖于 Ere2，这个库把许多 zkVM 统一封装在同一个 compile/execute/prove 接口背后。

重要一旦 zkVM 成为以太坊 L1 的核心组件，它的正确性就不再是应用层的问题，而是协议层的问题。过去只影响一个应用的 bug，如今会影响所有依赖这条链的人。正是这种转变推动了这项工作。

哪里可能出错：soundness、completeness 和 executor correctness

对于证明系统本身来说，有两个属性至关重要，而且它们失效的方向恰好相反。在这两者之下还有第三个关注点：soundness 和 completeness 考察的是证明系统是否忠实地反映了 zkVM 实际执行的内容，而 executor correctness 关心的则是它执行的内容到底是不是 RISC-V。

Soundness、completeness 和 executor correctness。

Soundness：只有陈述为真时，证明才能通过验证。soundness bug 会让恶意证明者针对虚假陈述生成一个能被接受的证明。
Completeness：对于每一个真实陈述，我们都能生成一个通过验证的证明。completeness bug 意味着一个合法、正确执行的程序无法被证明，无论是证明者直接失败，还是生成了一个被验证者拒绝的证明。
Executor correctness：zkVM 执行的内容应符合 RISC-V 规范。这纯粹是执行器自身的属性，与证明系统无关。correctness bug 意味着执行器与规范对程序行为的理解不一致。

Soundness 是经典的目标，也理应如此。在以太坊的语境下，soundness bug 是灾难性的：恶意证明者可能让网络接受一个无效状态转换的证明，从而伪造余额或状态根。大多数 zkVM 安全工作，包括我们所借鉴的故障注入研究，都聚焦于此。我们也在 Jolt 和 OpenVM 中发现过这类问题。

Completeness 受到的关注要少得多，而这正是我们如此重视它的原因。completeness bug 听起来似乎无害：程序只是无法被证明而已。但想一想，一旦证明成为以太坊的关键路径，这意味着什么。

完备性 bug 是活性风险 图 1. completeness bug 是活性风险。区块是有效的，每个节点都顺利执行了它，但证明者无法生成协议现在所要求的证明，证明过程因此在一个合法区块上停滞了。

假设一个区块完全有效。每个节点都执行了它，状态转换是正确的。现在要求证明者证明这次执行，但证明者做不到，因为该区块恰好用到的某条指令触发了 zkVM 崩溃。在已经 snark 化的以太坊中，区块必须携带有效性证明；如果没有任何诚实的证明者能为合法区块生成所需证明，那么最终性就无法达成。这是一种活性（liveness）失败，而且不需要恶意证明者：它可能意外发生，也可能是攻击者构造一笔交易，通过故意触发 completeness bug 来对整个网络发动拒绝服务攻击。3

Completeness bug 往往隐藏在 RISC-V 规范的那些边缘地带，也就是看似简单的实现捷径会静默偏离规范的边界情况。 Executor correctness 是根本原因，而不是最终表现，其后果取决于证明系统后续所做的检查。Soundness 和 completeness 描述的是用户最终会观察到的现象。给定一条分歧轨迹（即并未按照 RISC-V 语义执行的轨迹）：

证明系统...	后果
证明了该轨迹，且验证者接受	整个 zkVM 的 soundness 失败。证明系统忠实地完成了自己的工作，但它所证明的内容并不是 RISC-V 所规定的程序行为。
拒绝了该轨迹，但该程序在规范下是合法的	completeness 失败。合法程序无法被证明，并带来上文所述的活性后果。
拒绝了该轨迹，但规范本就要求拒绝	没有安全后果。最终结果是正确的，尽管它本应在执行阶段就被更早发现。

第三行同样并非无害。开发者主要围绕执行器进行迭代开发，因为执行很快，而证明很昂贵。一个会静默接受规范所禁止行为的执行器，会让开发者以为程序没有问题；而真相要到很久之后才会浮出水面，往往表现为难以解释的失败，并且与最初的问题毫无关联（例如证明栈深处的累加和不匹配，或者在 OpenVM 中，prove 已经打印成功消息之后才出现的验证失败）。幸运的是，我们发现的所有 executor-correctness bug 都属于第三行：没有一个为分歧执行生成了被接受的证明（soundness），也没有一个拒绝了规范认定为合法的程序（completeness）。

迄今为止的形式化验证工作集中于 soundness

迄今为止，我们在 zkVM 正确性方面拥有的最强工具，大多只关注了一个方向。以太坊基金会的 Verified zkEVM 项目是一个由多个团队合作推进的项目，旨在对照 RISC-V 规范对 zkVM 进行形式化验证，其宏伟目标是在 2027 年前实现无 bug 的 zk(E)VM。我们也通过自己的 Clean 框架为这个生态系统做出贡献，该框架用于在 Lean 中验证电路和多 AIR 系统。

但迄今为止，对 zkVM 约束的形式化验证几乎完全集中在 soundness 上。典型的方式是证明这样的定理：满足某个 chip 的约束就意味着对应的 RISC-V 指令被正确执行，因而不会产生虚假证明。而相反的方向——正确的执行总是可以被证明——才是 completeness 性质，它通常被排除在范围之外：要证明这一点，需要对证明者的 witness 生成进行推理，而不仅仅是针对约束本身，这是一个更大、也更少被探索的目标。

这个缺口并非假设。当 Succinct 和 Nethermind 对 SP1 Hypercube 的核心进行形式化验证时，这项工作为 RV64 操作码确立了 soundness，但据其自述，completeness 被搁置在了一旁。随后，一个目标未对齐的 JALR bug 正好从这个缺口漏了过去：该跳转的目标地址最低位为 1，按规范这是有效且定义良好的行为，但证明者会崩溃，或者验证者会拒绝。EF 自己的文章称其为“一个 completeness bug，在实际中可能成为拒绝服务向量”，并指出它超出了验证工作的范围，凸显了需要用其他技术补充形式化方法，以确保证明者的可用性。这正是 zkvmBlast 旨在暴露的类别；我们的 RISC-V 枚举甚至为此类未对齐跳转目标专门设置了探针。

与形式化验证互补差分模糊测试提供的保证弱于形式化验证，但它可以同时在多个 zkVM 上低成本运行，并且擅长发现 soundness 证明覆盖不到的 completeness 和 liveness bug。zkvmBlast 的定位是与这些验证工作并行，而不是取代它们。

zkvmBlast 做什么

zkvmBlast 是一个差分测试框架。其核心思想简单且由来已久：让同一个程序在多个独立实现和一个可信参考实现上运行，它们应当保持一致，任何不一致都是候选 bug。它之所以适用于 zkVM，是因为它跨越整个技术栈开展工作，从高级 Rust guest 程序一直到单条 RISC-V 指令，并且加入了不仅能发现崩溃、还能发现错误结果和无法证明执行的 oracle。

zkvmBlast 架构 图 2. zkvmBlast 概览。多种程序源为两个差分 harness 提供输入，它们驱动一组共享的 zkVM 执行器以及 Spike 参考模拟器（绿色）。差分 oracle 会将每个执行器与参考实现进行对比：结果一致即为正常，任何不一致都会被归类为 completeness、executor-correctness 或 soundness bug。

该框架由四个部分组成，各部分刻意保持解耦，因此可以添加新的程序源、新的 zkVM 或新的 oracle，而无需改动其他部分。

程序源（seeds）：模糊测试器的效果完全取决于它的种子，因此我们通过不同的方法来生成种子，以覆盖 zkVM 的大部分基础设施。在 Rust 方面，包括：从真实算法代码和编译器测试中收集并变异得到的语料库；我们对 RustSmith 的 fork——zkRustSmith——用于生成随机 Rust 程序；在 guest 中执行的完整 Reth 以太坊区块；以及用来测试预编译（precompile）功能的程序。在 RISC-V 方面，包括：随机的 Cascade 风格 RV32IM 程序；手工构建的 spec-isolation 语料库，用于锁定一个个规范边角；以及一种改编的 Skeletal Program Enumeration 方法，用于系统地枚举指令变体。RISC-V 种子语料库已作为独立仓库发布：riscv-seeds-lab。
执行器（Executors）：每个程序都会被转换成每个目标所期望的格式，然后并排运行。在 Rust 路径上，我们通过 Ere 覆盖 SP1、RISC0、OpenVM、Pico 和 Zisk；在 RISC-V 路径上，我们以 Spike 参考模拟器为基准，覆盖 SP1、RISC0、OpenVM、Pico 和 Airbender，该模拟器作为正确 RISC-V 机器行为的基准真相。需要说明的是，我们为 RISC-V 程序提供了适配器，以便高效地对这些 zkVM 进行模糊测试。
差分 oracle：不一致会在多个层面被捕获，例如：程序是否以相同方式终止（成功、trap 或超时）；是否达到相同的最终寄存器状态；参考实现接受的程序是否真的能被证明；以及对于 soundness oracle，被篡改的执行是否仍然产生了验证者接受的证明。
故障注入：差分 oracle 只能看到诚实运行产生的结果，但 soundness bug 需要的是不诚实的证明者，因此我们自己模拟了一个。该 harness 会修改 witness 生成逻辑，在一条原本正常的证明运行中注入单个受控故障，保持约束系统不变，然后把生成的证明交给一个独立的、未经修改的验证者。如果该验证者仍然接受，且公共值与干净运行时不同，就说明约束没能锁定它们本应锁定的内容，这就是 soundness bug。注入的故障都很小且目标明确，例如篡改 ALU 结果、重定向寄存器写入、篡改取到的指令字或程序计数器，或者改变内存读取返回的值，每个故障都针对约束系统的不同部分。该设计沿袭 Arguzz 的做法，使用 ELF 输入，而非 CircIL 派生的产品程序。目前，我们只在 SP1、OpenVM 和 Risc0 上尝试过注入故障，因为对 prover 进行插桩意味着要修改其源代码，而且高度依赖具体架构（这与上述差分测试不同，后者只需要匹配候选程序所期望的二进制格式即可）。

回顾同一个程序，多个 zkVM，一个可信参考。不一致就是潜在漏洞的线索。oracle 决定了你能发现哪类 bug。终止方式和寄存器状态的差异，加上对选定轨迹进行证明和验证，使我们能够捕获 executor-correctness、soundness 和 completeness 问题。此外，专门的故障注入模块让我们能够模拟恶意证明者，针对 soundness 问题。

整个设计过程中，我们始终以低门槛采用为目标。zkVM 团队可以将 harness 指向自己的 guest 程序，通过 Ere 接入新后端，然后把它作为 CI 任务来运行——只要出现任何无法解释的分歧，CI 就会失败。

目前我们已经发现了什么

以下是我们目前可以分享的发现——这些发现我们已经完成分类，并分享给了相关团队。所有发现都已负责任地披露给受影响的团队；其中一些已经修复。

发现	类别	目标	捕获位置	状态
非零 ALU 结果写入 `x0` 无法被证明	Completeness	SP1 v6.0.2	Prover	上游已修复
同一 `x0` 写入类别	Completeness	Pico v1.3.0	Prover	已报告
计算目标为奇数的合法 `jalr` 无法被证明	Completeness	Pico v2.0.0	Prover	已报告
未对齐的指令获取静默继续	Executor correctness	SP1 v6	Prover	已报告
未对齐的指令获取静默继续	Executor correctness	OpenVM	Verifier	已报告
未对齐的指令获取静默继续	Executor correctness	Pico v1.3.0	Prover	已报告
未对齐的 `lw`/`sw` 被静默舍入到对齐地址	Executor correctness	OpenVM	Prover	已报告
复现：内存检查（SubConfusion）伪造任意读取4	Soundness	RISC0 v2.0.0	未捕获	已在 v3.0.5 修复

每一个 completeness 和 executor-correctness 发现都会在流水线的某个环节被拦下，通常是一个失败或挂起的 prover；在一种情况下，则要等到 verifier 阶段——而且是在 prove 已经报告成功之后——才被拦住。Soundness 行是唯一被标记为 Not caught（未捕获）的，而这正是它成为 soundness bug 的原因：流水线中没有任何环节提出异议。有三个发现值得仔细看一下：一个 completeness bug 和两个 executor-correctness bug，后两者的分歧轨迹在流水线下游被证明系统拒绝了。

向 x0 写入非零结果。 RISC-V 规范将寄存器 x0 固定为零，因此对它的任何写入都会被丢弃。解释器遵循规范，直接丢弃这次写入。但是，如果证明者在某个 chip 上计算原始 ALU 结果，又在另一个 chip 上单独将 x0 约束为零，那么每当被丢弃的结果恰好非零时，就会产生一个不可满足的约束，导致合法程序无法被证明。

li   t0, 7
li   t1, 3
add  x0, t0, t1    # 结果 10 被丢弃；根据规范 x0 保持为 0

这是合法的 RISC-V，Spike 可以干净地停机，但 SP1 v6.0.2 和 Pico v1.3.0 在证明时拒绝了它。SP1 已在上游修复了该问题。

未对齐的指令获取。 分支或跳转到非四字节对齐的目标地址时，必须触发 instruction-address-misaligned trap。OpenVM、Pico 和 SP1 v6 在执行期间反而会静默地在未对齐的地址上继续运行。这种分歧会在下游被捕获，但不会在执行期间暴露：Pico 的 prover 会 panic，报出 Regional cumulative sum is not zero，这是由其内部深处的一个一致性检查引发的；SP1 v6 会因 GKR cumulative sum mismatch 对某个分片无限重试；OpenVM 会生成证明、打印 App proof completed!，然后直到 cargo openvm verify 时才以 stark verification error: challenge phase error 失败。这些错误消息没有一条能让人联想到未对齐的跳转。

auipc t0, 0         # t0 = 这条指令的地址
addi  t0, t0, 6     # target = 该地址 + 6，即 2 mod 4
jalr  zero, t0, 0   # jalr 清除第 0 位，但 6 是偶数，因此目标地址保持为 2 mod 4
                    # 规范：抛出 instruction-address-misaligned trap
                    # OpenVM、Pico 和 SP1 v6：在未对齐的 PC 处继续执行

OpenVM 中未对齐的字加载/存储。 规范允许未对齐数据访问有两种行为：trap，或者执行访问并返回正确结果。对于 lw 和 sw，OpenVM 两者都没有做到——它会静默地将地址向下舍入到最近的四字节边界，然后读取或写入错误的字节，而同一模块处理半字变体时却是正确的。给定一个前四个字节为 01 02 03 04 的缓冲区：

lw   t0, 1(a0)     # 规范：trap，或返回偏移 1..4 处的字节 (0x00040302)
                   # OpenVM：静默返回 0x04030201（偏移 0）

Prover 会拒绝为这个未对齐访问构建轨迹，并 panic 报出 unaligned memory access not supported: LOADW, shift: 1，因此错误的值永远不会被认证。只有在执行器这一阶段，程序看上去才像是运行正常的。

这些 bug 类别都不在标准 riscv-tests 套件的覆盖范围内，这正是为什么需要根据规范生成针对性测试，而不是仅仅复用现有测试。

注意这份清单只是一个快照，不是最终统计。我们仍在继续开展测试活动，并预计 completeness 发现的数量还会增加。随着新 bug 得到确认和披露，我们会更新这份清单。

结论

zkVM 正在成为以太坊可信计算基础的一部分。当这一天到来时，zkVM 与 RISC-V 规范之间的每一个差距，都会成为以太坊安全性或活性上的差距。zkvmBlast 正是我们系统性弥合这些差距的尝试：一个程序、多个 zkVM、一个可信参考，以及一个足够强大的 oracle——它能够发现 soundness 失败、静默偏离规范的执行器，而且至关重要的是，能够发现可能导致链停滞的 completeness bug。其成果是一个可复用的框架，zkVM 团队几乎不需要什么成本就能采用，并且可以持续在 CI 中运行；第一批真实发现也已经证明了它的有效性。

如果你正在构建或依赖于某个 zkVM，并希望对其进行模糊测试、加固或审计，我们很乐意与你合作。欢迎通过 zksecurity.xyz/contact 联系我们。

致谢

这项工作部分由以太坊基金会资助，正是他们的支持让这个项目成为可能。我们还要感谢 Cody Gunton 在整个过程中提供的宝贵反馈和头脑风暴。

以太坊基金会所阐述的 Ethproofs 北极星目标是：在约 10 秒内证明 99% 的主网 EVM 区块，功率预算约 10 kW，达到目标安全级别，并且整个技术栈已通过审计或形式化验证。关键指标是延迟，而不仅仅是成本。 ↩
Ere 正是 zkvmBlast 的 Rust harness 所依赖的同一抽象层，因此一旦 Ere 支持某个 zkVM，它就能立即成为模糊测试目标。借助生态系统的共享工具，我们得以与 EF 自身测试这些系统的方式保持一致。 ↩
EF 的基准测试团队也提出了关于性能的相同观点：一个无法及时证明的区块“会与一个定价错误的 opcode 或 precompile 一样，使网络的活性和最终性面临风险”。一个完全无法证明的区块，则是这种风险最尖锐的版本。 ↩
RISC0 内存检查 bug（GHSA-g3qg-6746-3mg9）通过故障注入机制在这里得到了复现：它让恶意证明者能够通过自抵消的排列条目，伪造任意内存读取并让验证者接受。该 bug 已在 RISC0 v3.0.5 中修复，最初由 Arguzz 模糊测试器于去年发现，我们的 soundness 转换正是基于其故障注入方法。这类故障注入的原始思想在论文 "Towards Fuzzing Zero-Knowledge Proof Circuits" 中有描述。复现这个 bug 起到了阳性对照的作用，表明只要存在真正的 bug，我们的 soundness oracle 就能捕获它。 ↩