利用无界单跳声明破坏Jolt验证器

我在 Jolt 的透明/非零知识验证器中发现了一个可靠性缺陷，它允许一个伪造的证明针对从未实际发生的执行通过验证（X 帖子）。

在我私下披露此问题后，该缺陷在 PR #1474 中得到了快速修复。

从高层次看，验证器信任了证明提交的中间声明，而没有检查它是否确实由先前的多项式消息生成。这个缺失的等式检查足以让恶意证明者将两个局部一致的证明组件拼接成一个全局上错误的证明。

缺陷总结

Jolt 的 uni-skip 验证器接受了一个由证明提供的输出声明，而没有检查它是否与提交的单变量多项式在验证器挑战点上的求值结果一致。

缺失的检查本质上是：

claimed_output == uni_poly.evaluate(r0)

其中 r0 是在第一轮单变量多项式之后通过 Fiat–Shamir 采样的挑战点。

没有这个检查，第一轮的 uni-skip 证明和后续的剩余证明各自看起来是有效的，但实际上它们悄然指向了不同的声明。

换句话说，验证器检查了桥的两端，但忘记了检查桥本身是否连接。

Uni-Skip 是什么

Uni-skip 是 sumcheck 的一种证明方优化策略。论文 Speeding Up Sum-Check Proving 将其描述为一种优化，它通过用更高次数的单变量步骤替换部分常规 sumcheck 流程来修改协议。在 Jolt 中，它被用作优化的 Spartan 证明者路径的一部分。

在普通的 sumcheck 中，证明者一次减少一个变量的多线性声明。在证明者发送当前轮次的单变量多项式后，验证者采样一个挑战 r，在这个多项式上对 r 求值，并将结果用作下一轮的声明。

Uni-skip 压缩了部分工作。它不是以常规方式经历几个小的布尔轮次，而是发送一个更大的单变量多项式，代表计算的一个打包切片。然后验证者采样一个挑战 r0，协议继续执行一个从该单变量多项式在 r0 处的值开始的剩余 sumcheck。

约束条件

Uni-skip 改变了 sumcheck 第一部分的表示方式，但没有改变验证者必须从中获取的信息：在采样 r0 之后，验证者必须使用提交的单变量多项式在 r0 处的求值结果作为剩余 sumcheck 的下一轮声明。

在这个缺陷中，验证者检查了提交的单变量多项式的总和是否正确，并且也检查了从声称输出值开始的剩余证明。但它没有检查声称输出值是否确实是多项式在 r0 处的求值结果。

这个缺失的检查就是整个缺陷：

claimed_output == uni_poly.evaluate(r0)

两个受影响的 Uni-Skip 路径

有两个相关的 uni-skip 路径：

SpartanOuter
SpartanProductVirtualization

两者都有相同的缺失边界检查，但它们位于验证器的不同部分。

α_outer

α_outer 是 SpartanOuter uni-skip 路径的输出声明。

它成为 Stage 1 外部剩余 sumcheck 的输入声明。

Stage 1:
  SpartanOuter uni-skip
      -> α_outer
  SpartanOuter remainder
      -> input claim = α_outer

这条路径特别重要，因为 SpartanOuter 是 Jolt 外层 R1CS 层检查虚拟机执行语义的地方：指令行为、寄存器值、RAM 访问、存储/加载一致性以及相关约束。

因此，如果伪造证明可以安排仅剩的不匹配是执行语义违规，那么该不匹配自然落在 Stage 1。

α_product

α_product 是 SpartanProductVirtualization uni-skip 路径的输出声明。

它进入 Stage 2，但并非作为整个 Stage 2 声明。Stage 2 将多个 sumcheck 实例批量处理：

Stage 2:
  0. RAM 读/写检查
  1. Spartan product remainder        <- input claim = α_product
  2. 指令查找声明约减
  3. RAM RAF 求值
  4. 公共输出检查

因此 α_product 专门是 Stage 2 中 Spartan product remainder 实例的输入声明。

这条路径涉及 product-virtualization 约束。它受到相同的缺失绑定检查影响，但对于我的伪造输出 PoC 而言，它并非最直接的途径。

为什么 PoC 使用 α_outer

对于 PoC，我针对的是返回值路径，而不是单纯更改公共输出。

guest 返回其输入，因此该值出现在 CPU 轨迹中，并通过返回/输出路径写入。通过修改该路径周围的 CPU 端 witness 生成，我可以使面向验证器的证明状态对应于伪造的输出。

这并不会使执行变得有效。它只是将剩余的不一致之处转移到外部执行约束，而这些约束由 SpartanOuter 强制实施。

这正是 α_outer 发挥作用的地方。

伪造证明将最终的谎言留在 Stage 1 的外部 R1CS 边界处，然后依赖缺失的绑定检查将外层第一轮多项式与外层剩余证明解耦。

结果是，该证明的各个部分在局部上是一致的，但执行的声明在全局上是错误的。

影响

影响是透明/非零知识路径中的验证器可靠性失效：验证器可以接受 guest 程序未生成的公共输出。

在最简 PoC 中，guest 程序原样返回其输入。对于输入 1333337，有效输出应为 1333337，但未打补丁的验证器接受了一个声明为 1333338 的证明。

#![cfg_attr(feature = "guest", no_std)]

#[jolt::provable(heap_size = 128, max_trace_length = 1024)]
fn return_same(x: u64) -> u64 {
    x
}

输入:              1333337
有效输出:          1333337
声称输出:          1333338
未打补丁的验证器:  接受
已打补丁的验证器:  拒绝

这就是 zkVM 可靠性缺陷的核心失效模式：验证器接受了一个 guest 程序未生成的公共输出。

补丁

修复在概念上很简单：在采样 r0 之后，将证明提供的输出声明与提交的单变量多项式的实际求值结果进行比较。

let expected_output = proof.uni_poly.evaluate(&r0);
let claimed_output =
    sumcheck_instance.expected_output_claim(opening_accumulator, &[r0]);

if claimed_output != expected_output {
    return Err(ProofVerifyError::UniSkipVerificationError);
}

重要的是，这个检查发生在声称输出被用作剩余证明的输入声明之前。

PoC

更多详情和可工作的 PoC 请参见 jolt-uni-skip-exploit。

感谢 young (coo) 在我寻找过程中给予的鼓励。

分享本文

在 X 上分享 在 LinkedIn 上分享 通过邮件分享

zkSecurity 为密码学系统提供审计、研究和开发服务，包括零知识证明、MPC、FHE、共识协议等。

了解更多 →

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