不实的断言：攻破 6 个 zkVMs

  • osecio
  • 发布于 21小时前
  • 阅读 28

这篇文章揭示了六个不同的zkVM（包括Jolt、Nexus、Cairo-M等）中存在的严重健全性漏洞。核心问题在于证明者控制的值未能在挑战生成前绑定到Fiat-Shamir记录中，从而允许攻击者通过求解线性或代数方程伪造证明，甚至证明数学上不可能的陈述。文章详细分析了漏洞原理、具体影响，并讨论了此类问题普遍存在的原因及防范措施。

不忠实的声明：攻破 6 个 zkVM

zkVM 验证者最重要的一点应该是忠实于其公共声明。然而，我们发现了六个系统，这个保证被打破了。了解一个微妙的顺序错误如何让攻击者完全绕过密码学并证明数学上不可能的陈述。

Unfaithful Claims: Breaking 6 zkVMs 的标题图片

zkVM 验证者最重要的一点应该是忠实于其公共声明。如果声明的输入/输出语句是假的，验证必须失败。

我们发现了六个系统，这个忠实性被打破了。在 Jolt、Nexus、Cairo-M、Ceno、Expander 和 Binius64 中，公共声明数据在挑战生成之前并非总是绑定到 Fiat-Shamir 记录中。这个微妙的顺序错误将语句值变成了验证者后续验证方程中攻击者可控的变量。

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

术语速查表

在我们深入探讨之前，这里是你将遇到的每个术语的一句话解释。ZK 生态系统尤其充满了行话和缩写，这可能会让新来者望而却步。请收藏此部分。

  • Fiat-Shamir：不是由真实的验证者发送随机挑战，而是哈希到目前为止的所有内容以获得“随机”挑战。使证明变为非交互式。

  • Transcript：运行中的哈希状态。你将数据“吸收到”其中，然后“挤出”挑战。

  • Polynomial Commitment：类似于哈希，但用于多项式。你承诺一个多项式，然后稍后证明“我的多项式在点 7 处评估为 42”，而无需透露整个多项式。

  • Sumcheck：一种协议，用于证明“该多项式在所有布尔输入上求和为 $H$”，而无需实际计算指数级的项。简化为检查一个随机点。

  • MLE (Multilinear Extension)：将值表转换为多项式。该多项式在 0/1 输入上等于该表，并在其他地方平滑插值。关键特性：评估它是表项的线性函数。

  • Lookup / LogUp：通过将成员关系编码为分数之和来证明“我的所有值都出现在此表中”。如果总和匹配，则集合匹配（以高概率）。

  • AIR：“代数中间表示”——一种将“有效执行跟踪”写成多项式方程的方法。如果方程成立，则跟踪有效。

  • STARK：使用承诺 + 随机采样 + FRI 证明 AIR 约束成立。无需可信设置。

  • FRI：“快速 Reed-Solomon IOP”——证明一个已承诺的函数实际上是一个低度多项式，而不是通过抽查的任意垃圾。

  • OODS：“域外采样”——在执行域之外的随机点检查约束多项式。将所有内容联系在一起。

  • GKR：使用 sumcheck 逐层验证算术电路。将“检查这个巨大的电路”简化为“检查几个随机评估”。

  • claimed_sum / opening_claim：证明者提供的值，用于验证方程。这些是绑定漏洞的常见嫌疑。

    • *

我们到底在攻破什么？

什么是 zkVM？

zkVM 证明声称程序在公共输入上正确执行，产生了声明的公共输出，同时隐藏了完整的执行跟踪。

形式上，验证者确信存在一个有效的跟踪 $T$，使得：

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

其中：

  • $P$ = 程序/电路描述（公共）
  • $X$ = 公共输入
  • $Y$ = 声明的公共输出
  • $T$ = 私有见证/跟踪（寄存器、内存历史、中间值）

验证者不会一步一步地重放执行。相反，它检查已承诺多项式上的代数约束。

本文中的某些系统是可验证计算系统，而不是完整的零知识系统，但关键属性仍然是健全性：

  • 完备性：诚实执行通过验证。
  • 健全性：虚假执行不应通过验证。

我们正在攻破所有六个系统的健全性。

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

  1. 确定公共声明数据。
  2. 解析证明负载（承诺、归约消息、开启）。
  3. 从记录状态重建 Fiat-Shamir 挑战。
  4. 在采样点检查约束方程。
  5. 检查 PCS/开启一致性。
  6. 仅在所有检查共同一致时才接受。

prover_verifier 流程图

不可协商的不变式是记录顺序：如果一个值影响验证者方程，它必须在该方程的门控挑战生成之前被吸收。违反这一点会给证明者一个攻击者可控的自由度。

构建模块

在我们理解这些漏洞之前，我们需要理解它们所打破的协议。每一个都是 zkVM 组合使用的工具。

Fiat-Shamir 变换

交互式协议（文献中最常描述的类型）需要实时通信。它涉及验证者发送随机挑战，证明者响应这些挑战。这不适用于区块链（你没有实时验证者）或当你希望任何人稍后验证你的证明时。

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

fiat_shamir 流程图

记录（哈希）必须包含所有在其中派生挑战被使用之前影响验证的内容。

如果某个值 $V$ 影响验证方程，但 $V$ 未在相关挑战被挤出之前被吸收，则该挑战完全独立于 $V$。这意味着证明者可以在选择 $V$ 之前“看到”（提前计算）挑战，这可能允许它精确地选择 $V$，从而使验证通过，即使它不应该通过。

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

Sumcheck 协议

Sumcheck 协议证明一个多项式在布尔超立方体（${0,1}^n$ 中的所有输入）上求和为一个声明的值，即声明：

$$H=\sum_{x1 \in {0,1}} \sum{x2 \in {0,1}} \cdots \sum{x_n \in {0,1}} g(x_1,x_2,\dots,x_n)$$

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

Sumcheck 协议是一个巧妙的交互式协议，它将指数级的多项式评估减少到只检查一个。

sumcheck 流程图

在每一轮中，证明者必须发送一个多项式 $g_i(X)$，使得 $g_i(0)+g_i(1)$ 等于先前的声明。如果证明者在原始和 $H$ 上撒谎，那么他们必须在某个地方撒谎关于 $g_i$。但由于验证者选择了一个随机的 $r_i$，以压倒性的概率，证明者将无法匹配原始多项式的评估。

压缩技巧

对于 1 次（多线性）多项式，$g_i(X)=a+bX$ 只有两个系数。由于验证者知道 $g_i(0)+gi(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 ri=a+(H{i-1}-2a) \cdot r_i=a(1-2ri)+H{i-1} \cdot r_i$$

这在 $H_{i-1}$ 中是线性的！通过归纳法，最终声明在原始 $H$ 中是线性的。如果 $H$ 不在记录中，我们可以求解它。

多线性扩展 (MLEs)

MLE 只是一个 ${0,1}^n$ 上的表的视图：它在布尔点上与表匹配，并将其扩展到域点。

对于本文，你唯一需要的属性是：

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

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

这种线性正是记录绑定缺失危险的原因：如果 $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 总和的贡献：

$$claimed_sum_i=\sum_j \frac{1}{z-emit_j} - \sum_k \frac{1}{z-consume_k}$$

全局检查：

$$\sum_i claimed_sum_i=0$$

为什么这容易受到攻击： $claimed_sum$ 值是由证明者提供的。如果它们在挑战被派生之前没有在记录中，证明者可以调整它们以使无效执行的总和为零。

通用攻击模式

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

攻击模式流程图

当值 $V$ 未绑定到记录时：

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

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

对于具有多个未绑定值的系统，我们得到一个线性方程组。高斯消元法在 $O(n^3)$ 域操作中求解它。对于非线性约束，我们可能需要使用更高级的技术，如合取（resultants）和 Groebner 基。

六个被攻破的系统

六个被攻破的系统图

现在让我们看看这在每个系统中是如何发生的。我们将深入探讨第一个（Jolt）以建立模式，然后重点关注每个后续系统的独特之处。

Jolt (a16z)

Jolt 是 a16z 构建的用于 RISC-V 程序的 zkVM。它广泛使用 sumcheck 来验证执行约束。

证明结构：

JoltProof {
    commitments: Vec<Commitment>,           // 跟踪的多项式承诺
    opening_claims: Map<OpeningId, Claim>,  // <- 易受攻击的值
    proofs: Map<Stage, SumcheckProof>,      // Sumcheck 和开启证明
    ...
}

验证流程：

Jolt 验证流程图

漏洞： 每个 sumcheck 实例都提供了一个 $input_claim$，这是多项式据称在布尔超立方体上求和的值。这些声明来自证明中的 $opening_claims$，但在批处理系数派生之前，它们从未被吸收到记录中。

Jolt 流程图

Sumcheck 如何使用 opening_claims：

在 Jolt 的批处理 sumcheck 中，验证者通过对各个声明 $H_i$ 进行随机线性组合来计算目标值 $BatchedClaim$：

$$BatchedClaim=\sum_i \alpha_i \cdot H_i$$

其中 $\alpha_i$ 是从记录中派生的随机系数。由于 $opening_claims$（包含 $H_i$）不在记录中，$\alpha_i$ 值独立于 $H_i$。

为什么它是线性的：

由于压缩优化（证明者每轮省略一个更少的系数），最终的验证方程通过各轮追溯，并在线性输入声明 $H$ 中变为线性

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

其中 $a,b$ 由记录决定（独立于 $H$）。验证者检查 $C_{final}=expected_eval$，这变为 $a \cdot H+b=expected_eval$。

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

这可以通过求解一个关于少数未绑定声明值的小型线性系统来利用，从而使所有受影响的检查同时通过。

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

Nexus

Nexus 是一个基于 Stwo 证明者（来自 StarkWare）构建的 zkVM。它使用带 LogUp 查找参数的 STARK。

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

每个组件发出和消费查找元组。组件的 $claimed_sum$ 总结了其净贡献：

$$claimed_sum_i=\sum_j \frac{1}{z-produced_j} - \sum_k \frac{1}{z-consumed_k}$$

所有 $claimed_sum$ 值必须总和为零（所有产生的都被消费）。

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

证明结构：

NexusProof {
    stark_proof: {
        commitments: [跟踪列的 Merkle 根]
        sampled_values: [多项式评估]
        fri_proof: [低度测试证明]
    }
    claimed_sum: [FieldElement; NUM_COMPONENTS]  // <- 易受攻击
    log_size: [组件大小]
}

$claimed_sum$ 值被检查长度是否正确，是否总和为零，并用于最终的组合多项式。但它们从未被吸收到记录中。

Nexus 流程图

OODS 检查计算组合多项式，其中包含 LogUp 边界约束。这些约束在 $claimed_sum$ 中是线性的：

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

$$C(x)=\sum_i \alpha_i \cdot constraint_i(x)$$

由于每个约束在其 $claimed_sum$ 中是线性的，因此整体组合多项式 $C(x)$ 在所有 $claimed_sum$ 值中是线性的。

验证者检查 $C(oods_point)=expected$

由于 $claimed_sum$ 不在记录中，组合多项式变为 $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 }, // output 修改
    },
    stark_proof: [...],
}

验证流程：

Cairo-M 验证流程图

查找挑战在 $public_data$ 未混入记录之前被派生。

$public_data$（程序 I/O、边界寄存器、内存根）通过元组的挑战加权编码进入分母内的查找关系。抽象地讲，验证者检查以下形式的关系：

$$L(public_data)+(\text{其他记录绑定项})=0$$ $$L=\sum_i \left(z+\langle\alpha,t_i(public_data)\rangle+\beta_1\right).$$

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

在挑战固定的情况下，这是一个关于公共数据的有理方程。这不是线性的，但仍然可以通过代数求解。

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

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

Ceno (Scroll)

Ceno 是 Scroll 的 zkVM，使用 GKR 和塔式 Sumcheck 结构。

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

许多每条记录的值（读取、写入、查找）被批处理成一个二叉树结构。每层用随机挑战折叠成对的值；这就是塔式 Sumcheck。

所有读取记录必须与所有写入记录（加上初始/最终状态）匹配。这通过多重集相等性检查，这次使用乘积而不是 LogUp：

$$\prod_i r_out_evals_i=\prod_j 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_evals$、$w_out_evals$ 和 $lk_out_evals$ 用于初始化塔式 Sumcheck 声明，但它们从未被吸收到记录中。这给我们留下了两个方程：

  1. GKR/塔式方程（在 $out_evals$ 中线性）：

塔式 Sumcheck 声明是

$$claim=\sum_j \alpha_j \cdot out_evals_j$$

此检查在 $out_evals$ 中是线性的。

  1. rw-乘积一致性（在 $out_evals$ 中双线性）：

$$\prod_i r_out_evals_i=\prod_j w_out_evals_j \cdot (\text{状态因子})$$

如果我们改变 $x_0=r_out_evals[0][0]$ 和 $x_1=r_out_evals[0][1]$，我们得到以下约束：

$x_0 \cdot x_1 \cdot (\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$

替换可将其简化为关于一个变量的二次方程，这可以通过二次公式求解。

状态： 自 2025 年 11 月 10 日以来问题仍未解决：#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$ 从未被吸收到记录中。记录是从 PCS 承诺和 Sumcheck 轮次消息初始化的，但公共输入是单独传递给验证者的。

Expander 流程图

$eval_cst$ 函数计算一个线性组合：

$$eval_cst=\sum_i public_input[i] \cdot eq(i,r)$$

其中 $r$ 包含挑战。由于挑战在语句数据绑定之前派生，它们独立于 $public_input$。这使得攻击者可以选择任意虚假语句（例如，伪造的输出），然后求解由此产生的线性约束，以获得修改后的 $public_input$，从而使验证者的检查通过。

状态： 已于 2026 年 1 月 21 日通过 commit 4a8c2be 修复。

50 万美元的漏洞赏金奖励待定。

Binius64

Binius64 是一个为二进制域优化的证明系统，旨在在 64 位 CPU 上高效运行。Binius 使用 $F_{2^{128}}$（或其变体），其中加法是异或。这使得某些操作非常快。

Binius 的一个关键特性是其用于位操作的专用协议。Shift 协议有效地处理位移和旋转（对于 SHA-256 等哈希函数至关重要），而没有其他证明系统中常见的大量开销。

漏洞：

验证者将公共见证（程序输入/输出）作为单独的参数接收：

pub fn verify<F, C>(
    constraint_system: &ConstraintSystem,
    public: &[Word],    // <- 从未被吸收
    // ...
) -> Result<VerifyOutput<F>, Error>

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

验证流程：

Binius 流程图

在验证期间

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

MLE 评估在公共见证位中是线性的：

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

由于挑战是固定的（独立于 $public$），攻击者可以找到一个替代见证 $public'$，产生相同的评估。这是一个单一的 128 位线性约束，涉及数百位，在高维二进制见证空间中产生一个单一的线性方程，这通常是欠约束的，并且在常见参数化下允许许多替代见证。

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

为什么这种情况会一再发生？

鉴于我们在六个独立的实现中发现了相同的漏洞类别，我们不得不问是否存在导致这种错误如此普遍的系统性问题。

学术论文未指定 Fiat-Shamir

学术论文通常描述交互式协议：“证明者发送 $C$。验证者发送

随机 $r$。证明者发送 $R$。”

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

因此，安全证明也分析了绑定是隐式的交互式协议。因此，确定要包含在记录中的内容责任落在了实现者身上，而实现者可能对完整协议没有很好的理解。

烫手山芋问题

现代 zkVM 是模块化的：

烫手山芋问题图

通常情况下，每一层都假定上一层/下一层处理某个值的记录绑定，因此最终它从未发生。

优化压力

性能对于 ZK 而言至关重要。由于每次哈希操作都有成本，因此总是存在排除“可能没问题”的值的压力。

确实存在可以安全地进行此操作的情况，但确定什么是安全的需要对所涉及的所有协议有充分的理解，并且排除某些内容的决定应由专家进行双重和三重检查。

测试未捕获对抗性输入

单元测试运行诚实的证明者。集成测试运行诚实的证明者。模糊测试只随机扰动值，欺骗验证者的概率非常低。识别 Fiat-Shamir 漏洞需要彻底的手动安全分析，有时甚至这也不足。

如何发现和修复这些漏洞

预防

Fiat-Shamir 长期以来一直是已知的健全性漏洞来源，这推动了使实现更不易出错的基本原语的开发。

一种这样的工具是将证明和记录合并，以强制证明者发送的所有值自动吸收到记录中。

证明者持有一个证明缓冲区，它模拟证明者和验证者之间的通信通道。当证明者发送一个值时，它被添加到证明缓冲区并自动吸收到记录中。当证明者需要从验证者读取挑战时，它只需从当前记录中挤出。

然后，验证者可以反向执行此操作。它逐步从证明缓冲区读取值，从而可以同步记录状态并派生相同的挑战。

Halo2 遵循这种模式，Binius 也以记录为中心。但即使合并了证明/记录，语句数据（例如，公共输入）仍必须在采样任何控制依赖于它们方程的挑战之前被吸收——正如 Binius 所展示的，即使以记录为中心的系统也可能遗漏这一点。

负责任的披露时间表

系统 报告日期 修复日期 响应时间
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 月 开放中 问题开放
Binius64 2025 年 12 月 2025 年 12 月 29 日 <1 周
Expander 2025 年 11 月 2026 年 1 月 21 日？ 3 个月

所有六个团队都收到了通知；响应从立即确认到延迟修复不等，其中一个问题仍未解决。

挑战

你认为你对这些漏洞有了很好的理解吗？我们准备了挑战，让你练习实现其中两个漏洞。如果你解决了任何一个，请按照 Flag 中的说明操作——前 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 记录。

在每种情况下，修复都微不足道——一两行代码。但要找到这个漏洞，需要理解完整的验证流程并提出问题：“如果证明者在看到挑战后选择了这个值会怎样？”

对于 ZK 生态系统： Fiat-Shamir 变换看起来很简单。哈希所有内容，派生挑战。实际上，当你有几十个组件，每个组件都有自己的输入和输出，每个组件都期望别人处理绑定时，“所有内容”很难指定。

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

对于审计人员： 绘制数据流图。跟踪记录。对照其相关挑战派生时间，检查每个证明者可控值。

对于开发者： 将记录视为神圣的账本。如有疑问，请吸收它。

  • 原文链接： osec.io/blog/2026-03-03-...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
osecio
osecio
Audits that protect blockchain ideas.

osecio

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！