零知识证明安全工具现状 - ZKSECURITY

零知识证明 (ZKP) 已经从提供隐私和可验证性的理论概念发展到具有实际的、现实世界的实现。一些最常见的用例包括区块链中的私有交易（例如，Zcash）、具有私有智能合约能力的区块链（例如，Aleo）、通过链下有效性证明实现可扩展性（例如，zk-rollups）、用于安全非托管身份验证的基础设施（例如，zkLogin）以及以隐私为中心的应用程序，如 ZKEmail。所有这些示例都构建在 SNARK 的基础上。

在过去的一年中，在 zkSecurity，我们一直在 审计 各式各样的使用 ZKP 的应用程序，甚至审计 ZKP 的实现。此外，我们一直在研究开发更安全的 用于编写电路的 DSL，并更好地理解 ZKP 中的安全问题 生态系统。最后，我们还 开发了工具，以帮助开发人员和审计人员在使用 ZKP 时。

在本文中，我们将简要讨论在使用 ZKP 时可能引入漏洞的地方，然后我们将讨论用于查找 ZKP 中漏洞的安全工具的现状。

SNARK 的层级

在我们最近的一项工作中，我们 系统化了 SNARK 中安全漏洞的知识，我们为 SNARK 提供了一个具体的系统模型。该模型的一部分是将 SNARK 的实现和使用分解为多个层级。下图描述了主要的层级。

我们有以下几个层级。对于每一层，我们还提供了 Semaphore 协议 的相应组件/工具。

• 电路层： 开发人员必须使用 DSL 或 eDSL（例如，Circom 或 Halo2）编写一个电路，该电路以 SNARK 友好的程序表示他们的逻辑。该电路具有双重目的：首先，计算值并填充 witness（证明者工作），其次，约束/断言 witness 是正确的（验证者逻辑）——例如，semaphore.circom。
• 前端层： 前端通常包括一个编译器，该编译器将电路作为输入，并在算术化（例如，R1CS）中提取约束。此外，前端还提供一个 witness 生成函数，该函数接受一些公共（和私有）输入，并根据电路中描述的逻辑生成 witness —— 例如，circom 编译器。
• 后端层： 后端实现了 SNARK 的三个主要功能，即 Setup、Prove、Verify —— 例如，snarkjs 工具链。
• 集成层： 除了电路和证明 witness 以及验证其证明所需的基础设施之外，应用程序通常还需要一些与 SNARK 组件交互的辅助代码。区块链世界中的一个典型例子是智能合约，该智能合约与链上验证器交互以验证提交的证明，并根据验证器的结果实现各自的逻辑。此代码可能需要执行一些重要的操作，例如在与 SNARK 交互之前强制执行某些断言，或实现对 ZKP 具有补充作用的关键逻辑，例如处理 nullifier —— 例如，semaphore.sol solidity 智能合约。

需要注意的是，任何层级的漏洞都可能破坏 ZKP 提供的属性。此外，前端或后端层级的漏洞可能会破坏构建在其上的任何应用程序，即使电路是正确的。

SNARK 中的漏洞

SNARK 中的漏洞可能会破坏 ZKP 提供的主要属性：

• 破坏可靠性： 证明者可以说服验证者相信一个错误的陈述。
• 破坏完整性： 无法验证有效陈述的证明，或无法生成有效陈述的证明。
• 破坏零知识： 关于私有 witness 的信息泄露。

用于检测电路 Bug 的安全工具

最近，从业者和研究人员都投入了大量精力来开发用于查找电路层漏洞的工具。这是意料之中的，因为大多数报告的与 ZKP 相关的漏洞都在该层，而且大多数审计都是电路审计。该层中可能发生的主要漏洞是：

• 约束不足漏洞： 由于约束不足而产生，通常会导致严重的可靠性错误。
• 约束过度漏洞： 电路可能被过度约束，导致诚实的证明者拒绝有效的 witness，或者诚实的验证者拒绝良性的证明。
• 计算/提示错误： 当电路的计算部分出现错误时发生。

到目前为止，几乎所有形式的形式化方法都已用于检测电路漏洞。下面，我们将简要描述用于检测电路漏洞的主要技术。

静态分析和符号执行

静态分析涉及在不执行代码的情况下检查代码，以识别潜在的漏洞。此方法依赖于模式和启发式方法来检测可能导致漏洞的常见问题。例如，Circom 的 Circomspect 和 ZKAP 以及 Halo2 电路的 halo2-analyzer。当前的方法是有限的，因为它们只能检测非常特定的漏洞模式，并且只能分析用特定 DSL 或 eDSL 编写的程序。原则上，某些技术可以在多个 DSL 上工作。这些工具通常在开发期间或审计的初始阶段使用，以检测潜在的漏洞。与其他行业相比，我们仍处于开发 ZKP 静态分析工具的初步阶段。例如，智能合约的静态分析器已经变得非常复杂，能够有效地检测关键漏洞。

符号执行 是一种程序分析技术，它通过将输入视为符号变量而不是具体值来检查程序可能的执行路径。此技术系统地探索程序可以采用的所有潜在路径，通过分析不同的变量如何影响程序行为来查找错误和漏洞。用于查找错误的符号执行与形式验证不同，在这一领域中仍未得到充分利用。此方法对于检测电路中约束不足和约束过度的错误特别有用。尽管它具有潜力，但除了最初的一些形式验证工作（我们将在下面看到）之外，符号执行尚未被广泛用于检测电路漏洞。

动态分析和模糊测试

动态分析涉及执行代码并实时观察其行为，以识别潜在的漏洞。模糊测试是动态分析的一个子集，它涉及向程序提供各种随机输入，以查看其如何处理意外或极端情况。用于动态分析的唯一现有工具是 SnarkProbe，这是一个用于 SNARK 的安全分析框架，可以分析基于 R1CS 的库和应用程序，以检测各种问题，例如边缘情况崩溃、密码操作错误和/或与协议描述不一致。此工具需要用户提供一些理想的功能文件，然后它尝试检测不一致之处。尽管 SnarkProbe 是一个有趣的初步方法，但在使用动态分析工具查找此空间中的错误方面，仍然存在错失的机会，类似于其他领域。请注意，已经进行了一些努力来应用传统的模糊器来检测 SNARK 中的问题，但通常这些工具会遇到困难，因为它们无法解决检测 SNARK 的重要漏洞所需的 oracle 问题，例如可能破坏应用程序可靠性的约束不足的错误。

形式验证

形式验证涉及以数学方式证明系统符合某些属性。此技术通过严格检查形式规范或某些规则来提供关于系统正确性和安全性的保证。具体来说，形式验证是一个使用数学和逻辑推理来确保系统设计满足某些正确性属性的过程。与传统的测试方法不同，传统的测试方法只能检测到错误的存在，而形式验证可以证明不存在特定类型的错误。这使其成为确保系统安全的有用工具。但是，形式验证通常会带来重大挑战，因为它需要准确的形式规范，并且它可能难以有效地扩展，通常会导致超时。有关 ZKP 形式验证的全面概述，你可以参考这篇 文章。下面，我们将简要讨论电路形式验证的当前状态。

不同的方法：使用证明助手与不使用证明助手

• 使用证明助手： 像 Coq 和 Lean 这样的证明助手提供了一个交互式环境，用于开发形式证明。这些工具允许用户使用形式语言编写规范和证明，然后证明助手会检查其正确性。使用证明助手需要大量的专业知识和努力才能有效地使用。最近，已经有人尝试通过程序转换来自动化该过程。
• 不使用证明助手： 此方法涉及使用自动工具（如 SMT 求解器（例如，Z3 和 CVC4）和其他自动推理工具）来验证系统的属性。

电路的形式验证

在 ZKP 电路的上下文中，形式验证确保电路正确地实现预期的逻辑，而不会引入漏洞。这涉及验证约束是否已正确实现，以及电路在所有可能的输入下是否按预期运行。

几个现有的开源端到端工具和电路形式验证技术包括：

• Picus：使用高级符号执行方法来验证 Circom 电路是否未被过度约束。此工具利用静态分析和 SMT 求解器来确保电路的每个部分都得到充分约束。
• CIVER：采用一种基于应用转换和演绎规则的模块化技术，以使用前置和后置条件验证 Circom 电路的属性。此方法提供了一种结构化的方式来推理电路组件的正确性。
• horus-checker：使用 SMT 求解器对带有语言注释的 Cairo 智能合约执行形式验证。
• Medjai：Cairo 的符号求值器，用于检查 Cairo 程序是否持有某些属性。
• DSL（如 Coda 和 Leo）：这些特定于领域的语言支持使用综合来形式验证电路，从而帮助开发人员创建更安全的电路。它们将形式验证技术直接集成到开发过程中，从而更容易从一开始就确保正确性。
• 从 Gnark 到 Lean 的转换器：一个库，用于将零知识电路从 Gnark 编译到 Lean 定理证明器，以形式化验证电路。

尽管取得了这些进展，但仍然存在重大限制。依赖于 SMT 求解器的工具（如 Picus）面临着有限的支持和处理有限域算术的效率方面的挑战，从而导致性能瓶颈。这些工具虽然功能强大，但通常受到底层求解器能力的限制，这可能会限制它们对更复杂电路的适用性。Ozdemir 等人 最近的工作试图改进 ZKP 的 SMT 求解器。 证明助手语言，特别是对于密码协议，在表达性方面仍然面临限制。很少有工具能够直接证明关于密码协议的定理。已经进行了多次努力来克服这些障碍，但形式化验证 ZKP 电路仍然是一项具有挑战性的任务。尽管为 ZKP 形式验证做出了令人印象深刻的努力，但它应该伴随着整体安全方法来确保安全。端到端的形式验证是一项复杂的任务，并且通常依赖于用户输入和其他软件，这意味着在实践中很难确定是否存在错误。

测试工具

此外，在电路开发过程中，我们发现了一个主要问题：缺乏强大的测试框架。开发人员通常在 eDSL 中使用来自宿主语言的测试框架，或者在使用 DSL 时创建自定义工具链。但是，对于有效地为电路编写单元测试和集成测试（特别是对于测试可靠性漏洞）的支持有限。基础设施中缺少的一个关键部分是基于属性的测试，类似于 QuickCheck 或 Foundry，这对于彻底的属性测试至关重要。

此外，在大多数 DSL 中调试电路是一项具有挑战性的任务，这是另一个需要改进的领域。为了解决这个问题，我们开发了 Circomscribe，这是一个用于调试 Circom 电路中约束的工具。展望未来，我们计划发布更多工具来帮助开发人员和审计人员测试和调试电路，从而增强整体开发过程并确保 ZKP 实现的更高安全性和可靠性。

概述

在下表中，我们提供了现有开源工具的概述：

UC：约束不足，OC：约束过度，CE：计算错误，SA：静态分析，FV：形式验证，DA：动态分析

前端和后端

基础设施层（包括 SNARK 系统的前端和后端）在很大程度上被安全研究人员所忽视。Ozdemir 等人 认识到 ZKP 编译器中的缺陷可能会破坏 ZKP 的完整性，并采取了初步措施，通过部分验证 CirC 编译器 中的关键编译器过程来减轻此类风险。SNARKProve 实施了一个模糊测试框架，可以使用自定义文件（即理想文件）进行配置，以测试后端和前端的特定密码属性。在其初始版本中，它已成功检测到后端 Setup 阶段中的问题。

一些初步工作 已经完成，用于验证验证器，即确保验证算法的实现是正确的。此外，从业者已使用 AFL 等模糊测试工具来识别这些层中的错误。但是，这些工具在范围上有些有限，通常只能检测到崩溃，并且可能会遗漏更微妙但关键的漏洞，例如错误编译。 检测这些层中的错误至关重要，因为任何可利用的错误都可能影响整个堆栈。例如，即使对电路进行形式化验证，前端漏洞也可能导致其部署不健全。因此，确保前端和后端层的安全性和正确性对于 ZKP 系统的整体完整性至关重要。

接下来是什么

用于 ZKP 的安全工具正处于开发的早期阶段，但它们对未来充满希望。这些工具可以极大地帮助开发人员，并且理想情况下应成为开发生命周期的组成部分，在审计之前使用。审计仍然主要是一项手动工作，因为大多数使用 ZKP 的协议都需要领域专业知识来理解它们的逻辑和实现。

在 zkSecurity，我们致力于开发和公开共享工具，以帮助审计人员和开发人员。像 Circomspect 这样的工具是我们改进 ZKP 电路调试工作的一部分。我们还致力于对 ZK 漏洞进行分类，并提供见解以改进和开发新的工具来检测它们。查看我们关于 回旋镖漏洞 的博客文章和我们 关于分析 SNARK 漏洞的论文以获取更多信息。

如果你对零知识证明和安全充满热情，请考虑加入我们这个激动人心的旅程。你可以通过参加我们的 zkBank 挑战 这里 来申请！对于那些对 ZKP 安全工具感兴趣并正在寻找实习机会来解决有趣问题的人，请考虑 这里 申请。

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