不诚实的声明:攻破六个zkVM系统

osecio 发布于 2026-03-04 阅读 13

本文揭示了六个主流zkVM系统(Jolt、Nexus、Cairo-M、Ceno、Expander、Binius64)中存在的关键安全漏洞,均源于Fiat-Shamir变换的实现缺陷:prover控制的值(如opening_claims、claimed_sum、public_data等)未在挑战生成前绑定到哈希转录本,导致攻击者可先计算挑战值再调整这些数据,从而伪造证明(如证明费马大定理的反例)。

引言

zkVM 验证器首先必须忠实于一件事:其公共声明。如果声称的输入/输出语句为假,验证必须失败。

我们在六个系统中发现了这种忠实的缺失。在 JoltNexusCairo-MCenoExpanderBinius64 中,公共声明数据并不总是在挑战生成前被绑定到 Fiat-Shamir 交互式证明(transcript)中。这个微妙的顺序缺陷将声明值变成攻击者在后续验证方程中可控制的变量。

在这篇文章中,我们演示如何利用这些未绑定变量来完全绕过密码学,证明数学上不可能的语句,例如找到费马大定理的反例(参见 挑战 亲自尝试)。在区块链环境中,这可能意味着凭空获得 100 万美元。


术语速查表

ZK 生态系统术语和缩写特别多,可能让新手望而却步,因此请将本节收藏。在我们深入之前,这里为每个你将遇到的术语提供一句话解释:

  • Fiat-Shamir:不用真正的验证者发送随机挑战,而是哈希到目前为止的所有内容来获取“随机”挑战。使证明变为非交互式。
  • 交互式证明(Transcript):正在运行的哈希状态。你将数据“吸收”进去,然后“挤出”挑战。
  • 多项式承诺:类似于哈希,但针对多项式。你对多项式进行承诺,之后证明“我的多项式在点 7 处求值为 42”而无需透露整个多项式。
  • Sumcheck:一种协议,用于证明“这个多项式在所有布尔输入上的和为 $H$”,而无需实际计算指数级的项。它简化为检查一个随机点。
  • MLE(多重线性扩展):将值表转换为多项式。该多项式在 $0/1$ 输入处与表相同,并在其他地方平滑插值。关键性质:其求值是表条目的线性函数。
  • Lookup / LogUp:通过将成员关系编码为分数和来证明“我所有的值都出现在这个表中”。如果和匹配,则集合匹配(概率很高)。
  • AIR:“代数中间表示”——一种将“有效执行轨迹”写成多项式方程的方法。如果方程成立,则轨迹有效。
  • STARK:使用承诺 + 随机抽样 + FRI 证明 AIR 约束成立。无需可信设置。
  • FRI:“快速 Reed-Solomon IOP”——证明一个承诺的函数确实是一个低次多项式,而不是任意可通过抽查的垃圾。
  • OODS:“域外采样”——在执行域之外的随机点检查约束多项式。将所有内容联系在一起。
  • GKR:使用 sumcheck 逐层验证算术电路。将“检查这个巨大电路”简化为“检查几个随机求值”。
  • claimed_sum / opening_claim:证明者提供的值,用于验证方程。这些是绑定错误的常见嫌疑对象。

我们到底在破坏什么?

zkVM 是什么?

zkVM 证明声称一个程序在公共输入上正确执行,产生了声称的公共输出,同时隐藏了完整的执行轨迹。

形式上,验证者确信存在一个有效轨迹 $T$ 使得:

$$ \exists T : \mathsf{VM}(P, X, T) \to Y $$

其中:

  • $P$ = 程序/电路描述(公共)
  • $X$ = 公共输入
  • $Y$ = 声称的公共输出
  • $T$ = 私有见证/轨迹(寄存器、内存历史、中间值)

验证者不会逐步重放执行过程。相反,它检查承诺多项式上的代数约束。

本文中的一些系统是可验证计算系统,而非完整的零知识系统,但关键属性仍然是可靠性

  • 完备性:诚实执行能验证通过。
  • 可靠性:虚假执行不应验证通过。

我们在所有六个系统中破坏了可靠性

定义(忠实性)

当验证者接受的公共声明正是绑定到证明中的声明时,验证者是忠实的。在本文中,每个错误都允许证明者控制的声明在 know 交互式证明(transcript)挑战之后改变,而证明仍然验证通过。

在所有六个代码库中,验证遵循以下抽象流程:

  1. 固定公共声明数据。
  2. 解析证明负载(承诺、约简消息、打开)。
  3. 从交互式证明(transcript)状态重建 Fiat-Shamir 挑战。
  4. 在采样点检查约束方程。
  5. 检查 PCS/打开一致性。
  6. 只有当所有检查共同一致时才接受。

公共声明数据同时输入证明者的执行和 Fiat-Shamir 交互式证明(transcript)。证明者执行程序,构建包含承诺、约简消息和打开的证明负载,验证者按协议顺序吸收声明和证明元素,然后挤压挑战并运行约束、PCS 和全局一致性检查以接受或拒绝。\ \ 验证者检查\ \ Fiat-Shamir 交互式证明(transcript)重建\ \ 证明负载(发送给验证者)\ \ 证明者端\ \ 公共声明\ \ 程序 $P$\ \ 输入 $X$\ \ 声称输出 $Y$\ \ 元数据\ \ 大小、根、域\ \ 执行 $P(X)$\ \ 私有轨迹 /\ \ 见证 $T$\ \ 构建证明\ \ 承诺\ \ 约简消息\ \ sumcheck / GKR / STARK 轮次\ \ 声称求值 /\ \ 打开\ \ 吸收 声明 元素\ \ 吸收 证明 元素\ \ 按协议顺序\ \ 挤压挑战\ \ 约束检查\ \ (在挑战点)\ \ PCS / 打开检查\ \ 全局一致性\ \ 检查\ \ 接受 / 拒绝

不可协商的不变量是交互式证明(transcript)顺序:如果一个值影响验证方程,它必须在采样控制该方程的挑战之前被吸收。违反这一点会给证明者一个攻击者可控制的自由度。


基础构件

在理解错误之前,我们需要理解它们破坏的协议。这些是 zkVM 组合使用的工具。

Fiat-Shamir 变换

交互式协议1 需要实时通信。它涉及验证者发送随机挑战,证明者响应。这不适用于区块链(没有实时验证者)或当你想让任何人在以后验证你的证明时。

解决方案是用哈希函数替换验证者的随机性。证明者“自言自语”,使用到目前为止所有内容的哈希作为挑战。如果我们使用密码学哈希函数,这意味着挑战是完全不可预测的。

在交互式协议中,证明者发送一个承诺,验证者回复一个随机挑战,证明者响应,然后重复,最后验证者运行最终检查。\ \ 验证者\ \ 证明者\ \ $\mathsf{verify}(C, r_1, R_1, r_2, R_2)$\ \ 承诺 $C$\ \ 随机挑战 $r_1$\ \ 挑战响应 $R_1$\ \ 随机挑战 $r_2$\ \ 挑战响应 $R_2$

证明者将每条消息吸收到交互式证明(transcript)中,并从中挤压挑战,而不是与实时验证者对话,然后发送证明,验证者重放相同的吸收-挤压步骤,用自己的交互式证明(transcript)检查。\ \ 验证者交互式证明(transcript)\ \ 验证者\ \ 证明者交互式证明(transcript)\ \ 证明者\ \ $\mathsf{verify}(C, r_1, R_1, r_2, R_2)$\ \ 吸收承诺 $C$\ \ 挤压挑战 $r_1$\ \ 吸收挑战响应 $R_1$\ \ 挤压挑战 $r_2$\ \ 发送证明 $(C,R_1,R_2)$\ \ 吸收承诺 $C$\ \ 挤压挑战 $r_1$\ \ 吸收挑战响应 $R_1$\ \ 挤压挑战 $r_2$

重要

哈希(交互式证明(transcript))必须在从它派生的挑战被使用之前,包含所有影响验证的内容。

如果某个值 $V$ 影响验证方程,但 $V$ 在相关挑战被挤压之前没有被吸收,那么挑战完全独立于 $V$。这意味着证明者可以在选择 $V$ 之前“看到”(提前计算)挑战,这可能允许它精确选择 $V$ 使得验证通过,尽管本应不行。

这是我们在所有六个系统中发现的错误类别。

Sumcheck 协议

Sumcheck 协议证明一个多项式在布尔超立方体(所有输入在 ${0,1}^n$ 中)上的和等于声称的值,即声明:

$$ H = \sum_{x_1 \in {0,1}} \sum_{x_2 \in {0,1}} \cdots \sum_{x_n \in {0,1}} g(x_1, x_2, \ldots, x_n) $$

朴素的方法是让验证者计算所有 $2^n$ 个求值。这是指数级昂贵的。

Sumcheck 协议是一个巧妙的交互式协议,将指数级的多项式求值减少到仅检查 一个

逐轮,证明者发送一个单变量多项式,验证者根据当前声明检查它并回复一个随机挑战,将多元和减少到一个通过一次打开证明检查的求值。\ \ 验证者\ \ 证明者\ \ 声明 $H=\sum_{\vec{x}\in{0,1}^n} g(\vec{x})$ 关于 $\vec{x}=(x_1,\dots,x_n)$\ \ 第1轮:$g_1(X)=\sum_{x_2,\dots,x_n} g(X,x_2,\dots,x_n)$\ \ 验证 $g_1(0)+g_1(1)=H$\ \ 第2轮:$g_2(X)=\sum_{x_3,\dots,x_n} g(r_1,X,x_3,\dots,x_n)$\ \ 验证 $g_2(0)+g_2(1)=g_1(r_1)$\ \ 重复 $n$ 轮...\ \ 最后一轮:验证 $g(r_1,\dots,r_n)=g_n(r_n)$ (对承诺多项式的单次打开证明)\ \ $H$\ \ 单变量 $g_1(X)$\ \ 随机挑战 $r_1$\ \ 单变量 $g_2(X)$\ \ 随机挑战 $r_2$

在每一轮中,证明者必须发送一个多项式 $g_i(X)$,使得 $g_i(0) + g_i(1)$ 等于前一个声明。如果证明者关于原始和 $H$ 撒谎,那么他们必须在某个地方对 $g_i$ 撒谎。但由于验证者选择一个随机 $r_i$,大概率下,证明者将无法匹配原始多项式的求值。

压缩技巧

对于一次(多重线性)多项式,$g_i(X)=a+bX$ 只有两个系数。由于验证者知道 $g_i(0)+g_i(1)=H_{i-1}$(前一个声明),我们有:

$$ a+(a+b)=H_{i-1} \implies b = H_{i-1} - 2a $$

因此,证明者只发送 $a=g_i(0)$,验证者恢复 $b$。这节省了 50% 的通信成本。

链条中的下一个声明是:

$$ H_i = g_i(r_i) = a + b \cdot r_i = a + (H_{i-1} - 2a) \cdot r_i = a(1 - 2r_i) + H_{i-1} \cdot r_i $$

这个式子关于 $H_{i-1}$ 是线性的!通过归纳,最终声明关于原始 $H$ 是线性的。如果 $H$ 不在交互式证明(transcript)中,我们可以解出它。

直觉(为什么线性性重要)

一旦挑战固定,验证者就意外地将声称的和变成了一个旋钮。如果方程关于那个旋钮是线性的,攻击者不需要破坏承诺方案;他们解出验证者会接受的值。

多重线性扩展(MLE)

MLE 就是表在 ${0,1}^n$ 上的多项式视角:它在布尔点上与表匹配,并将其扩展到域点上。

对于本文,你只需要这个性质:

$$ \tilde{f}(\vec{r}) = \sum_{\vec{b} \in {0,1}^n} f(\vec{b}) \cdot \text{eq}(\vec{b}, \vec{r}) $$

在固定挑战点 $\vec{r}$ 处,系数 $\text{eq}(\vec{b}, \vec{r})$ 是常数,因此 $\tilde{f}(\vec{r})$ 关于表值 $f(\vec{b})$ 是线性的。

正是这种线性性使得缺失交互式证明(transcript)绑定很危险:如果 $\vec{r}$ 在这些值被绑定之前已被采样,攻击者可以在保留相同求值声明的同时重新编程值。

查找参数(LogUp)

zkVM 需要检查值是否满足某些性质。例如:

  • 这个字节是否在范围 $[0,255]$ 中?
  • 这个操作码是否正确解码?
  • 这次内存访问是否与之前的访问一致?

朴素方法: 为每个检查添加约束。代价高。

聪明方法: 预计算一个有效元组表。证明程序使用的每个值都出现在表中。这是一个多重集成员关系检查。

LogUp(对数导数): 将多重集成员关系编码为分数之和。

如果多重集 $A$ 应该等于多重集 $B$:

$$ \sum_{a \in A} \frac{1}{z - a} = \sum_{b \in B} \frac{1}{z - b} $$

对于随机挑战 $z$。如果多重集匹配,则和相等。如果不同,则和以压倒性概率不同。

在 zkVM 中: 不同组件发出和消耗查找元组:

  • CPU 发出:“我在时间 $t$ 从地址 $a$ 读取值 $v$”
  • 内存表消耗:“在时间 $t$,地址 $a$ 包含 $v$”

如果一切平衡,则执行一致。

claimed_sum: 每个组件计算其对 LogUp 和的贡献:

$$ \text{claimed_sum}_i = \sum_j \frac{1}{z - \text{emit}_j} - \sum_k \frac{1}{z - \text{consume}_k} $$

全局检查:$\sum_i \text{claimed_sum}_i = 0$。

为什么这容易受到攻击: claimed_sum 值由证明者提供。如果它们在挑战派生之前不在交互式证明(transcript)中,证明者可以调整它们以使和为零,即使执行无效。


通用攻击模式

现在我们描述适用于所有六个系统的攻击模式:

一个四步攻击。第1步找到证明者控制的值,并检查它们是否在挑战之前绑定到交互式证明(transcript);如果没有,则是候选。第2步追溯一个值 $V$ 如何影响验证,写出关于 $V$ 的验证方程,并确定它是线性的还是低度的。第3步固定交互式证明(transcript)和挑战,将未绑定值视为变量,并收集验证者方程。第4步建立方程组,求解,修补证明,然后伪造的证明验证通过。\ \ 第4步:求解和伪造\ \ 建立方程组\ \ 求解\ \ 用解修补证明\ \ 第3步:推导约束\ \ 固定交互式证明(transcript)/ 挑战\ \ 将未绑定值视为变量\ \ 收集涉及它们的验证者方程\ \ 第2步:追溯至方程\ \ 值 $V$ 如何影响验证?\ \ 写出关于 $V$ 的验证方程\ \ 确定:方程关于 $V$ 是线性/低次吗?\ \ 第1步:识别未绑定值\ \ 找到证明者控制的值\ \ 检查:它们是否在挑战之前就在交互式证明(transcript)中?\ \ 如果不是:攻击的候选\ \ 伪造的证明验证通过!

当一个值 $V$ 未绑定到交互式证明(transcript)时:

  1. 挑战固定(独立于 $V$)
  2. 验证方程形式:$f(V) = \text{target}$
  3. 如果 $f$ 是线性的:$\alpha \cdot V + \beta = \text{target}$
  4. 求解:$V = (\text{target} - \beta) / \alpha$

命题(未绑定线性声明)

如果一个证明者控制的值 $V$ 以 $\alpha V + \beta$ 的形式影响验证者检查,并且定义 $\alpha$ 和 $\beta$ 的挑战是在 $V$ 被绑定之前采样的,那么只要 $\alpha \ne 0$,证明者就可以在看到交互式证明(transcript)后选择 $V = (\text{target} - \beta) / \alpha$。

在最简单的线性情况下,伪造简化为求解一个低维域方程,而其他系统需要小型耦合系统。

对于有多个未绑定值的系统,我们得到一个线性方程组。高斯消元法在 $O(n^3)$ 次域运算中求解它。对于非线性约束,我们可能需要使用更高级的技术,如结式和 Groebner 基。


六个被破坏的系统

六个系统根据未绑定值所在位置分为两组。在 Jolt(opening_claims)、Nexus(claimed_sum)和 Ceno(out_evals)的证明负载中;作为声明参数传递给 Cairo-M(public_data)、Expander(public_input / claimed_v)和 Binius64(public witness)。\ \ 未绑定值作为声明参数传递:Cairo-M(public_data,有理系统)、Expander(public_input / claimed_v,线性)、Binius64(public witness,线性)。\ \ 未绑定值位于证明负载中:Jolt(opening_claims,线性系统)、Nexus(claimed_sum,线性)、Ceno(out_evals,线性 + 乘积)。

现在让我们看看这在每个系统中如何体现。我们将深入第一个(Jolt)以建立模式,然后关注每个后续系统的独特之处。


Jolt(a16z)

Jolt 是一个针对 RISC-V 程序的 zkVM,由 a16z 构建。它广泛使用 sumcheck 来验证执行约束。

证明结构:

JoltProof {

    commitments: Vec<Commitment>,           // 对轨迹的多项式承诺

    opening_claims: Map<OpeningId, Claim>,  // <- 易受攻击的值

    proofs: Map<Stage, SumcheckProof>,      // Sumcheck 和打开证明

    ...

}

验证流程:

验证者接收 JoltProof 和公共 I/O,设置交互式证明(transcript),运行批量 sumcheck,验证打开与承诺,并接受。\ \ 阶段5:打开验证(批量验证多项式求值,检查与承诺)\ 阶段2-4:批量 sumcheck(推导批量系数,计算 BatchedClaim,验证 sumcheck 轮次)\ 阶段1:交互式证明(transcript)设置(初始化交互式证明(transcript),吸收公共 I/O、轨迹长度、吸收承诺)\ 验证者接收 JoltProof 和公共 I/O,然后接受。

错误: 每个 sumcheck 实例提供一个 input_claim,即多项式据说在布尔超立方体上求和的值。这些声明来自证明中的 opening_claims,但它们从未在批量系数派生之前被吸收到交互式证明(transcript)中

承诺、公共 I/O 和轮次消息被吸收以推导批量系数和 sumcheck 挑战,但 opening_claims 从未被吸收,然而来自 opening_claims 的 $H_i$ 作用于 BatchedClaim 验证方程。\ \ 验证方程:BatchedClaim = $\sum_i \alpha_i \cdot H_i$\ \ 挑战推导:$\alpha_i$(批量系数)和 sumcheck 挑战来自交互式证明(transcript)状态。\ \ 未吸收:opening_claims(缺失)。\ \ 交互式证明(transcript)状态:包括承诺、公共 I/O、轮次消息。

Sumcheck 如何使用 opening_claims:

在 Jolt 的批量 sumcheck 中,验证者通过取各声明 $H_i$ 的随机线性组合来计算目标值 BatchedClaim

$$ \text{BatchedClaim} = \sum_i \alpha_i \cdot H_i $$

其中 $\alpha_i$ 是从交互式证明(transcript)派生的随机系数。由于 opening_claims(包含 $H_i$)不在交互式证明(transcript)中,$\alpha_i$ 值与 $H_i$ 无关。

为什么是线性的:

由于压缩优化(证明者每轮省略一个系数),最终验证方程通过各轮回溯,变成关于输入声明 $H$ 的线性形式:

$$ C_{\text{final}} = a \cdot H + b $$

其中 $a, b$ 由交互式证明(transcript)决定(独立于 $H$)。验证者检查 $C_{\text{final}} = \text{expected_eval}$(来自 PCS 打开),这变为 $a \cdot H + b = \text{expected_eval}$。

由于多个声明跨验证阶段耦合,攻击者可能需要同时调整一小部分声明值以满足所有受影响的约束。

这可以通过求解一个关于少数未绑定声明值的小型线性方程组来利用,使得所有受影响的检查同时通过。

状态: 于 2025 年 10 月 3 日通过 PR #981 修复


Nexus

Nexus 是一个基于 Stwo 证明器(来自 StarkWare)的 zkVM。它使用带有 logup 查找参数的 STARK。

Nexus 将验证拆分为组件,例如指令执行、内存、寄存器等。每个组件处理一部分约束。

每个组件发出和消耗查找元组。组件的 claimed_sum 总结其净贡献:

$$ \text{claimed_sum}_i = \sum_j \frac{1}{z - \text{produced}_j} - \sum_k \frac{1}{z - \text{consumed}_k} $$

所有 claimed_sum 值必须总和为零(所有生产的东西都被消耗)。

所有约束组合成一个组合多项式。然后验证者在执行域之外的一个随机点检查这个多项式,这称为 OODS(域外采样) 测试。

证明结构:

NexusProof {

    stark_proof: {

        commitments: [Merkle 树根 of 迹列]

        sampled_values: [多项式求值]

        fri_proof: [低度测试证明]

    }

    claimed_sum: [FieldElement; NUM_COMPONENTS]  // <- 易受攻击

    log_size: [组件大小]

}

检查 claimed_sum 值长度正确、总和为零,并用于最终的组合多项式。但它们在交互式证明(transcript)中从未被吸收。

associated_data、log_sizes 和迹承诺推导查找元素、OODS 点和组合系数,而 claimed_sum 独立于交互式证明(transcript)却作用于验证检查。\ \ 验证:检查 $\sum_i \mathrm{claimed_sum}_i = 0$,$CP(\mathrm{oods}) = \mathrm{expected}$。\ \ 不在交互式证明(transcript)中:claimed_sum。\ \ 推导的挑战:lookup_elements ($z$)、OODS 点、组合系数来自交互式证明(transcript)状态。\ \ 交互式证明(transcript)状态:独立于 claimed_sum。

OODS 检查计算组合多项式,其中包括 logup 边界约束。这些约束相对于 claimed_sum线性的

组合多项式是约束的随机线性组合:

$$ C(x) = \sum_i \alpha_i \cdot \text{constraint}_i(x) $$

由于每个约束相对于其 claimed_sum 是线性的,整个组合多项式关于所有 claimed_sum 值是线性的。

验证者检查 $C(\text{oods_point}) = \text{expected}$。

由于 claimed_sum 不在交互式证明(transcript)中,组合多项式变成 claimed_sum 值的线性函数。结合声明的总和必须为零这一约束,这是一个容易求解的小型线性系统。

状态: 于 2025 年 10 月 24 日通过 PR #503 修复


Cairo-M(Kakarot Labs)

Cairo-M 由 Kakarot Labs 构建,是 Cairo VM(用于 Starknet)的另一种证明系统。

Cairo-M 在许多方面与 Nexus 类似。它使用 logup 来证明关于执行的全局语句。

证明结构:

Proof {

    claim: ComponentSizes,

    interaction_claim: LogupClaimsPerComponent,

    public_data: {          // <- 易受攻击

        initial_registers: { pc, fp },

        final_registers: { pc, fp }, // <- 伪造

        clock,                       // <- 伪造

        initial_root,

        final_root,                  // <- 伪造

        public_memory: { program, input, output }, //输出被修改

    },

    stark_proof: [...],

}

验证流程:

证明者设置元素被吸收,查找挑战被抽取,但 public_data 在它用于 claimed_sum 检查时尚未进入交互式证明(transcript),使其未绑定。\ \ 验证流程:混合 PCS 配置,提交迹根,混合 claim(组件大小),检查工作量证明,吸收设置元素,抽取查找挑战 $z,\alpha$,BUG: public_data 尚未在交互式证明(transcript)中,检查:$\mathrm{claimed_sum}(\mathrm{relations}, \mathrm{public_data}) = 0$,混合 interaction_claim,验证 STARK 证明。

查找挑战派生时没有将 public_data 混合到交互式证明(transcript)中。

public_data(程序 I/O、边界寄存器、内存根)通过挑战加权的元组编码以_分母_形式进入查找关系。抽象而言,验证者检查一个形式如下的关系:

$$ L(\text{public_data}) + \text{(其他交互式证明(transcript)绑定的项)} = 0, \quad L = \sum_i \frac{1}{z + \langle \alpha, t_i(\text{public_data})\rangle + \beta} $$

全局检查是 $L(p) + \text{(其他项)} = 0$。

随着挑战固定,这是关于公共数据的一个有理方程。这不是线性的,但仍然代数可解。

公共数据坐标通过扩展域算术(包括扩展域值的公共内存条目)参与验证关系,因此伪造参数搜索是一个耦合的扩展域系统。

状态: 于 2025 年 10 月 31 日通过 commit 92b6740 修复


Ceno(Scroll)

Ceno 是 Scroll 的 zkVM,使用带有塔 sumcheck 结构的 GKR。

Ceno 将验证拆分为芯片,每个操作码或查找表一个。每个芯片独立证明其约束。

许多每条记录的值(读、写、查找)被批处理到二叉树结构中。每一层用随机挑战折叠值对;这就是塔 sumcheck

所有读记录必须匹配所有写记录(加上初始/最终状态)。这次通过一个乘积(而不是 logup)检查多重集相等:

$$ \prod_i \text{r_out_evals}_i = \prod_j \text{w_out_evals}_j \cdot (\text{状态因子}) $$

证明结构:

ZKVMChipProof {

    r_out_evals: [[FieldElement]],   // <- 易受攻击

    w_out_evals: [[FieldElement]],   // <- 易受攻击

    lk_out_evals: [[FieldElement]],  // <- 易受攻击

    tower_proof: [...],

    gkr_iop_proof: [...],

}

r_out_evalsw_out_evalslk_out_evals 用于初始化塔 sumcheck 声明,但它们从未被吸收到交互式证明(transcript)中。这给我们留下了两个方程:

  1. GKR/塔方程(关于 out_evals 是线性的):

塔 sumcheck 声明是 $\text{claim} = \sum_j \alpha^j \cdot \text{out_evals}_j$。

这个检查关于 out_evals 是线性的。

  1. rw-乘积一致性(关于 out_evals 是双线性的): $$ \prod_i \text{r_out_evals}_i = \prod_j \text{w_out_evals}_j \cdot (\text{状态因子}) $$ 如果我们改变 $x_0 = \text{r_out_evals}[0][0]$ 和 $x_1 = \text{r_out_evals}[0][1]$,我们得到以下约束: $$ x_0 \cdot x_1 \cdot (\text{乘积的其余部分}) = \text{target} $$ 这是关于 $(x_0, x_1)$ 的双线性形式。

我们有两个未知数 $(x_0, x_1)$ 和两个方程,一个线性,一个双线性:

  1. 线性(来自 GKR):$a_0 x_0 + a_1 x_1 + c = 0$
  2. 双线性(来自多重集):$k \cdot x_0 \cdot x_1 + d = 0$

代入法将其化简为关于一个变量的二次方程,可以用二次公式求解。

状态: 于 2026 年 3 月 5 日通过 PR #1262 修复(原始报告:#1125


Expander(Polyhedra)

Expander 是一个基于 GKR 的算术电路证明系统。

证明结构:

Proof(原始字节,按顺序解析):

    - PCS 承诺

    - Sumcheck 轮次多项式(每层)

    - 层声明(claim_x, claim_y)

    - PCS 打开证明

不在证明字节中(单独传递):

    - public_input    // 单独传递的声明数据

    - claimed_v       // 单独传递的声明

在 Expander 的电路模型中,常数门可以引用公共输入值。在 GKR 验证期间,eval_cst() 计算这些门在 sumcheck 挑战点处的贡献:

sum -= GKRVerifierHelper::eval_cst(&layer.const_, public_input, sp);

这个求值是公共输入值的线性组合,权重系数来自存储在验证者暂存区 (sp) 中的挑战。

漏洞:

public_input 从未被吸收到交互式证明(transcript)中。交互式证明(transcript)从 PCS 承诺和 sumcheck 轮次消息初始化,但公共输入单独传递给验证者。

交互式证明(transcript)仅由证明字节构建;public_input 和 claimed_v 单独传递且从未被吸收,然而它们用于 GKR sumcheck 检查,该检查关于 public_input 是线性的。\ \ GKR sumcheck 验证使用 (public_input, claimed_v) – 关于 public_input 是线性的。\ \ 交互式证明(transcript)仅由证明字节构建(PCS 承诺、sumcheck 轮次、层声明、打开证明)。\ \ 从未被吸收:public_input, claimed_v。

eval_cst() 函数计算一个线性组合:

$$ \text{eval_cst} = \sum_i {\text{public_input}[i]} \cdot \text{eq}(i, \vec{r}) $$

其中 $\vec{r}$ 包含挑战。由于挑战是在声明数据绑定之前派生的,它们独立于 public_input。这使得攻击者可以选择一个任意虚假声明(例如,伪造的输出),然后求解诱导出的线性约束,得到一个修改后的 public_input,使验证者的检查通过。

状态: 于 2026 年 1 月 21 日通过 commit 4a8c2be 修复;声称 50 万美元 bug 赏金 奖励待定。


Binius64

Binius64 是一个针对二进制域优化的证明系统,旨在 64 位 CPU 上高效。Binius 使用 $\mathbb{F}_{2^{128}}$(或其变体),其中加法是 XOR。这使得某些操作非常快速。

Binius 的关键特性之一是其用于位运算的专门协议。移位协议高效处理位移和循环移位(对像 SHA-256 这样的哈希函数至关重要),而不会像其他证明系统那样产生巨大开销。

漏洞:

验证者将公共见证(程序输入/输出)作为单独参数接收:

pub fn verify<F, C>(

    constraint_system: &ConstraintSystem,

    public: &[Word],    // <- 从未被吸收

    // ...

) -> Result<VerifyOutput<F>, Error>

在移位协议中,挑战 $r_j$ 和 inout_eval_point 在公共见证绑定之前被采样。

验证流程:

第一个 sumcheck 和采样的挑战驱动验证方程,但 public_input 在它用于 public_eval MLE 之前未被吸收到交互式证明(transcript)中,使其未绑定。\ \ 验证流程:第一个 sumcheck(产生 $\gamma, r_j, r_s$),采样 inout_eval_point,采样 batch_coeffBUG: public_input 尚未被吸收,然后 public_eval = MLE(public_input, $r_j$, inout_eval_point),sum = $\gamma + \text{batch_coeff} \cdot \text{public_eval}$,第二个 sumcheck(验证批量求和)。

在验证期间:

  1. Sumcheck 产生挑战点 $r_j$(位索引)和 $r_s$(移位索引)
  2. 验证者从交互式证明(transcript)采样 inout_eval_point
  3. 验证者使用未绑定的 public 切片计算 public_eval = MLE(public, r_j, inout_eval_point)
  4. public_eval 进入后续验证方程

MLE 求值关于公共见证位是线性的:

$$ \text{public_eval} = \sum_{w,b} {\text{public}[w][b]} \cdot \text{eq}(b, r_j) \cdot \text{eq}(w, \text{inout_eval_point}) $$

由于挑战固定(独立于 public),攻击者可以找到一个替代见证 $\text{public}'$ 产生相同的求值。这是一个在数百位上的单一 128 位线性约束,产生高维二进制见证空间中的一个线性方程,通常在常见参数化下欠约束,允许许多替代见证。

状态: 于 2025 年 12 月 29 日通过 commit 86a515f 修复


为什么这种情况一再发生?

鉴于我们在六个独立实现中发现了相同的错误类别,在某个时刻我们不得不问:是否存在系统性原因使这个错误如此常见?

学术论文未指定 Fiat-Shamir

学术论文通常描述_交互式_协议:“证明者发送 $C$。验证者发送随机 $r$。证明者发送 $R$。”

它们通常省略使协议非交互式所需的步骤:“在采样 $r$ 之前哈希 $C$。还要哈希公共声明。还要哈希影响后续方程的中间值。”

因此,安全证明也分析交互式协议,其中绑定是隐式的。确定交互式证明(transcript)中应包含什么的责任落在实现者身上,而实现者可能对完整协议没有很好的理解。

烫手山芋问题

现代 zkVM 是模块化的:

每一层假设另一层绑定该值。zkVM 层传递声明,查找和 sumcheck 层假设它是交互式证明(transcript)绑定的,声明漏过,因此未绑定值到达验证者。\ \ zkVM 层传递声明/值 → 查找层假设_交互式证明(transcript)绑定_ → Sumcheck 层假设_交互式证明(transcript)绑定_ → 声明漏过:未绑定值到达验证者。

经常发生每层假设上一层/下一层处理一个值的交互式证明(transcript)绑定,所以最后它从未发生。

优化压力

性能对 ZK 至关重要。由于每次哈希操作都有成本,不断有压力排除那些“可能没问题”而省略的值。

确实存在可以安全地这样做的情况,但确定什么是安全的需要完全理解所有涉及的协议,并且排除某些东西的决定应由专家双重和三重检查。

测试无法捕获对抗性输入

单元测试运行诚实的证明者。集成测试运行诚实的证明者。模糊测试只随机扰动值,并且成功欺骗验证者的概率极低。识别 Fiat-Shamir 错误需要彻底的手动安全分析,有时即使这样也不够。


如何发现和修复这些错误

预防

Fiat-Shamir 长期以来一直是可靠性错误的已知来源,这推动了使实现更不易出错的原语的发展。

一种工具是将证明和交互式证明(transcript)合并,从而强制证明者发送的所有值自动被吸收到交互式证明(transcript)中。

证明者持有一个证明缓冲区,模拟证明者和验证者之间的通信通道。当证明者发送一个值时,它被添加到证明缓冲区并自动被吸收到交互式证明(transcript)中。当证明者随后需要从验证者读取一个挑战时,它只需从当前交互式证明(transcript)中挤压出挑战。

然后可以对验证者反向进行。它逐渐从证明缓冲区读取值,从而同步交互式证明(transcript)状态并推导出相同的挑战。

Halo2 遵循这种模式,Binius 也以交互式证明(transcript)为中心。

警告

即使有合并的证明/交互式证明(transcript),声明数据(例如公共输入)仍然必须在采样任何控制依赖于它们的方程的挑战之前被吸收——正如 Binius 所证明的,即使是以交互式证明(transcript)为中心的系统也可能遗漏这一点。


负责任的披露时间线

系统 报告时间 修复时间 响应时间
Jolt 2025年9月 2025年10月3日 <1周
Nexus 2025年10月 2025年10月24日 <1周
Cairo-M 2025年10月 2025年10月31日 <1周
Ceno 2025年11月 2026年3月5日 ~4个月
Binius64 2025年12月 2025年12月29日 <1周
Expander 2025年11月 2026年1月21日? 3个月

所有六个团队都收到了通知;响应从立即承认到延迟修复不等,所有报告的问题都已得到解决。


挑战

你认为你对这些错误有了很好的理解了吗?我们准备了挑战,让你练习实现其中两个利用。如果你解决了任何一个,按照标志中的说明操作。前 10 名解出者将获得一件 T 恤。

你的目标是找到费马大定理的一个反例,即你知道 $a, b, c$ 使得 $a^3 + b^3 = c^3$,$a,b,c \ge 1$。祝你好运!

Jolt

请参阅讲义了解服务器上运行的设置。 通过连接到 jolt.chal.osec.io:8960 提交你的证明。

Nexus

请参阅讲义了解服务器上运行的设置。 通过连接到 nexus.chal.osec.io:8950 提交你的证明。

现在你应该有足够的余地来证明费马是错误的。


总结

我们在六个独立的 zkVM 中发现了关键的可靠性漏洞。所有漏洞共享相同的根本原因:影响验证方程的证明者控制值在挑战派生之前未绑定到 Fiat-Shamir 交互式证明(transcript)。

每个案例的修复都很简单——一两行代码。但发现错误需要理解完整的验证流程并问:“如果证明者在看到挑战后选择了这个值会怎样?”

对 ZK 生态系统而言: Fiat-Shamir 变换看起来很简单。哈希一切,推导挑战。实际上,当你有数十个组件,每个组件都有自己的输入和输出,每个都期望别人处理绑定时,“一切”很难指定。

我们通过检查少数几个系统发现了六个实例。在当今部署的数十个 zkVM、证明系统和递归验证器中,还有多少?

对审计人员而言: 绘制数据流图。追踪交互式证明(transcript)。对照其相关挑战派生的时间检查每个证明者控制的值。

对构建者而言: 将交互式证明(transcript)视为神圣的账本。有疑问时,就吸收它。

脚注

  1. 文献中最常描述的类型。
  • 原文链接: osec.io/blog/zkvms-unfai...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~

相关文章

0 条评论