Halo2证明系统的安全性

引言

零知识证明（ZKPs）使个体能够证明自己知道或拥有某些信息，而无需透露实际数据。在此过程中，“证明者"基于对系统输入的知识生成证明，而"验证者"在不访问底层信息的情况下确认证明的有效性。

zk-SNARKs（简洁非交互式知识论证）是非交互式协议，允许证明者生成简洁的知识证明。它们通常用于证明对于给定函数f和公共输入x，证明者知道私有输入w（称为见证），使得f(x, w) = y。这一过程不泄露私有输入的任何细节，使zk-SNARKs在各种应用中极具价值，特别是在区块链技术中。

zk-SNARKs通过确保交易细节保密，促进了公共区块链（如Zcash）上的私有交易。它们还用于合规目的，例如证明私有交易符合银行法规，或在不泄露敏感信息的情况下证明偿付能力。此外，zk-SNARKs通过实现zk-SNARK Rollups中的隐私和支持通过zk-Bridges的区块链互操作性，有助于可扩展性。

在之前的文章中，我们介绍了Zekrom，一个面向算术化的zk-SNARK电路构建的开源库，包含Griffin、Neptune、Rescue Prime和Reinforced Concrete等哈希函数。该库旨在使用现代框架（如arkworks-rs和Halo2）分析新型电路构建的性能，同时为隐私保护应用提供即用型解决方案。

在本文中，我们探讨zk-SNARK证明系统中的常见漏洞，特别关注Halo2证明系统，并检查与不当实现相关的风险。此外，我们探索可用于Halo2的安全分析工具并评估其有效性。

Halo2

Halo2是Zcash生态系统的一部分，是一个zk-SNARK协议。它基于PLONK的算术化，特别使用称为UltraPLONK的扩展版本，支持自定义门和查找表，这些特性通常称为"PLONKish”。Halo2的关键优势之一是不需要可信设置，并且支持递归证明组合，使其特别适合在Zcash数字货币中使用。

除了在Zcash中使用外，Halo2还被各种其他组织广泛采用，包括Protocol Labs、以太坊基金会的隐私和扩展探索（PSE）、Scroll和Taiko等。这种广泛采用使Halo2成为当今行业中最流行的zk-SNARK构建之一。Halo2的高级概述如下所示：

UltraPLONK

PLONK是一个基于多项式IOPs（交互式预言证明）的zk-SNARK，由于其紧凑的证明大小（约400字节）和快速的验证时间，在行业中被广泛采用。UltraPLONK通过引入对自定义门和查找表的支持来增强PLONK，这进一步减少了计算轨迹的大小并提高了证明者的效率。

在PLONK中，门主要由乘法和加法操作组成。电路约束使用原始PLONK约束表示，该约束可以定义加法和乘法门。

其中qL、qR、qO和qM是预处理的选择器多项式。给定证明系统中的任何电路都可以通过这个原始方程表示，并辅以从布线派生的额外约束。

内积论证

多项式承诺方案（PCS）通常可以分为几类，包括单变量多项式承诺、多线性承诺、向量承诺和内积论证（IPA）。PLONK的一个关键优势是其灵活性，允许它与任何类型的PCS配对以创建SNARK。

PLONK通常使用单变量多项式承诺，如KZG多项式承诺方案，该方案依赖于通用可信设置。然而，PLONK的一个重大挑战是证明者的计算复杂性，因为它依赖于快速傅里叶变换（FFT），这需要拟线性运行时间，这是使用单变量多项式的直接结果。HyperPlonk依赖于多线性多项式承诺来消除对FFT的需求并支持高度自定义门。

Halo2通过采用基于Pedersen承诺方案的内积论证（IPA）来消除对可信设置的需求。尽管IPA通常导致比PLONK SNARK更大的证明，但Halo2通过使用累积来减轻这一缺点。该机制允许通过递归组合聚合多个证明开放，从而在证明大小和无信任设置的优势之间实现有效平衡。通过利用这些技术，Halo2实现了可扩展的零知识证明系统，而不损害安全性或效率。

Halo2证明系统中的常见漏洞

大多数零知识应用不是从头开发的；相反，它们通常依赖于第三方代码库或低级库的分支。因此，许多ZK开发团队主要专注于电路设计和业务逻辑，而不是构建自己的框架。因此，ZK审计往往 heavily 关注电路，因为它们是堆栈中最容易出错的组件。

然而，ZKP堆栈远不止电路设计，如下所示。全面的ZK审计因此应检查ZK堆栈的所有方面，包括协议的正确性、密码算法的安全实现、参数的正确使用以及所涉及的依赖关系。

下面，我们提供一些零知识证明系统中公开披露的漏洞示例。有关更全面和最新的列表，我们建议参考ZK Bug Tracker，这是一个社区维护的资源，专门跟踪与ZKP技术相关的漏洞。

Fiat-Shamir转换

Fiat-Shamir（FS）转换使证明者能够无需交互地生成挑战值，取代了验证者提供的挑战。这是通过使用确定性方法（通常是密码哈希函数）来产生挑战值来实现的。虽然这种转换简化了交互式证明过程，但其实际实现可能非常复杂。

Fiat-Shamir转换的一个关键方面是仔细选择密码哈希函数的输入。证明系统的安全性在很大程度上取决于这些输入的正确选择。使用不正确或不完整的输入可能导致漏洞，通常导致证明系统被破坏。例如，如果公共输入的部分被省略在FS转换中，可能会出现Frozen Heart漏洞。类似地，如果在计算最终FS转换挑战时除了公共输入之外的部分转录本被排除，则可能发生Last Challenge Attack。因此，需要仔细考虑和严格分析以确保转换安全实现。

KZG'10承诺方案

KZG'10承诺方案在计算任何KZG承诺之前需要一次可信设置。一旦这个可信设置完成，它可以被重用来承诺和揭示尽可能多的不同多项式。然而，这个过程的一个关键方面是在设置期间生成的秘密参数。这个参数必须在可信设置仪式后安全丢弃，以确保没有人能够确定其值。

可信设置仪式通常使用 established 方法进行，这些方法依赖于弱信任假设，例如1-out-of-N信任假设，可以通过多方计算（MPC）实现。这些方法有助于确保即使所有但一个参与者被破坏，设置仍然安全。有关可信设置如何工作的更多信息，您可以参考Vitalik Buterin的这篇文章。

KZG方案中的另一个潜在漏洞涉及由于省略完整转录本的非输入部分而导致的Fiat-Shamir转换的错误计算。有关更多细节，请参见这篇论文。

尽管在Zcash中实现的原始Halo2协议不使用KZG承诺，但一些Halo2变体由于需要在资源受限的硬件上更小的证明和更快的验证而使用KZG承诺方案。例如，Aleph Zero证明系统采用这种方法。

Circom电路

根据一份调查论文，ZK审计报告中超过80%的发现可追溯到电路层。电路审计的一个关键方面是确保所有输入在证明生成过程中被正确使用和约束。在Circom电路中，这意味着每个输入必须参与约束的创建以确保证明的完整性。

约束不足的电路可能导致验证者错误地接受无效证明，损害系统的正确性。相反，过度约束的电路可能导致诚实证明者或良性证明被不公正地拒绝，这影响系统的完备性。

Circom中的约束仅使用===或<==运算符生成。然而，可能会错误地使用<–运算符，该运算符不创建约束。未约束的<–信号可以被恶意证明者自由设置为任何值，可能损害证明的安全性。尽管这种方法有时可能用于电路优化——例如将三元运算符从两个约束减少到一个——但如果不仔细管理，会带来风险。

如果您在Circom中遇到<–，必须确保后续信号被正确约束，以防止恶意证明者插入任意值同时仍通过证明验证。

算术溢出/下溢

在ZKPs中，Circom电路在标量场上运行，所有算术操作都在场的阶数下模运算执行。这种模运算经常导致溢出或下溢问题，由于固有的包装行为，这些问题并不立即明显。

为了减轻这些风险，开发人员可以利用Circomlib提供的LessThan和Num2Bits模板。这些模板有助于强制值保持在指定范围内，有效防止溢出和下溢。

缺失约束

在zk电路中，赋值用于在证明生成过程中为变量分配值，但与约束不同，它们本身不强制执行证明有效性。如果在配置函数中省略了必要的约束，恶意证明者可能通过修改赋值函数来绕过或操纵缺失的约束来利用此弱点。

赋值和约束定义之间的这些差异创建了漏洞，允许恶意行为者分叉代码并调整赋值函数以利用缺失的约束。这种操纵可能导致生成看似有效的无效证明，破坏zk电路的安全性和完整性。

安全分析工具

静态分析

• Circomspect：由Trail of Bits开发，Circomspect是Circom编程语言的静态分析器和linter。它利用iden3构建的基于Rust的Circom编译器的代码，提供对Circom代码中潜在漏洞和最佳实践的见解。
• ZKAP：一组静态分析检测器，旨在识别零知识证明（ZKP）实现中的错误。该工具专注于在ZKP框架内查找常见陷阱和错误。
• Korrekt (Halo2-analyzer)：由Quantstamp创建，该工具自动验证Halo2证明系统的正确性，该系统采用PLONKish算术化。它有助于确保在Halo2框架内生成的证明的完整性。
• Ecne：Ecne将函数转换为Rank-1约束系统（R1CS）形式，并用于验证某些R1CS约束集唯一地表示函数。这确保密码约束准确反映预期逻辑。
• Picus：Picus实现QED工具来检查各种正确性概念，特别专注于检测结果系统是否约束不足。这有助于识别zk-SNARK电路中的潜在安全漏洞。
• Circomscribe：一个在线工具，显示哪些Circom代码行生成特定约束（如果有）。Circomscribe是Circom编译器的修改版本，在WebAssembly（WASM）中运行，并在编译过程中发出详细的JSON格式信息。

动态分析

• SNARKProbe：SNARKProbe提供两个子工具：ConstraintChecker和SnarkFuzzer。ConstraintChecker识别约束扁平化或小工具使用中的错误，而SnarkFuzzer是一个智能模糊测试工具，旨在发现zk-SNARK库中的潜在逻辑或软件错误。这些工具有助于动态测试和验证zk-SNARK实现的鲁棒性。

后量子HALO2

许多现有的zk-SNARK，包括广泛部署的系统如Groth16、PLONK、Marlin和Bulletproofs，基于离散对数和对基于的密码假设，这些假设容易受到量子攻击。为了应对这一风险，正在付出大量努力来集成后量子（PQ）密码方案，特别是为了减轻"现在拦截-以后解密"威胁。然而，将zk-SNARKs转换为量子抵抗构建的紧迫性不如公钥密码方案那么紧迫。这是因为与SNARKs相关的安全风险不同于加密，其中主要关注点是对拦截数据的回顾性解密的潜在可能性。

尽管如此，在开发后量子zk-SNARKs方面已经取得了重大进展，这些SNARKs依赖于密码哈希函数或基于格的密码学。这些方法通常伴随着证明大小更大的 trade-off，这可能导致区块链上更慢的验证时间和增加的燃气成本。几个后量子SNARKs已经使用基于哈希的Merkle承诺构建，如STARKs、Ligero、Aurora和Brakedown。虽然这些系统提供量子抵抗，但它们往往具有相对较大的证明大小，并在处理大语句时需要大量内存资源。

基于格的zk-SNARKs也在进步，并显示出更高效、量子弹性证明的潜力。尽管尚未像基于哈希的系统那样具有竞争力，但最近的构建如SLAP和LatticeFold表明了基于格承诺在zk-SNARKs中的前进道路。

尽管有这些进步，一个重大挑战仍然存在：后量子zk-SNARKs的证明大小仍然比其前量子对应物大得多。例如，Groth16可以产生小至128字节的证明，而最简洁的后量子证明可能大到1000倍。这种显著差异强调了实现量子弹性所涉及的效率 trade-offs，并突出了持续研究和开发以弥合这一差距同时保持区块链应用实际性能的需求。

对于量子抵抗的Halo2，一个逻辑起点是用后量子替代方案替换基于离散对数的承诺方案，可能利用最近进展中的基于格承诺方案。我们将在下一篇文章中回顾后量子zk-SNARKs的现状以及它们如何应用于Halo2。

结论

零知识证明（ZKPs）和zk-SNARKs的最新进展带来了一系列令人兴奋的应用，特别是在区块链行业。然而，尽管工具和方法论取得了进步，漏洞仍然可能出现，特别是考虑到zk-SNARK系统固有的复杂性。

通过在开发生命周期中整合这些实践，我们可以增强零知识证明系统的安全性，从而推进其在区块链中隐私保护计算的有效性。