[Paper] 用 NAVe 对 Noir 零知识程序进行形式化验证

Source: arXiv - 2601.09372v1

概览

本文介绍了 NAVe，一个开源验证器，通过对其底层算术电路进行形式化推理，检查 Noir 零知识（ZK）程序的正确性。通过将 Noir 的中间表示（ACIR）编码为 SMT‑LIB，并利用 cvc5 求解器，作者展示了开发者可以自动验证程序的约束是否真正捕获了预期的密码学关系——这是构建可信 ZK 应用的关键步骤。

关键贡献

• Formal SMT‑LIB encoding of ACIR – 将 Noir 的高级电路描述精确地翻译为现代 SMT 求解器支持的有限域扩展理论。
• NAVe verifier implementation – 基于 cvc5 构建的开源工具，能够自动检查 Noir 程序的约束是否正确。
• Comprehensive evaluation – 对四个不同的 Noir 代码库（包括真实世界的 zk‑app 和合成基准）进行验证，表明 NAVe 能捕获那些否则需要手动证明的细微错误。
• Identification of a hard‑to‑check constraint pattern – 作者定位了一类当前 SMT 技术难以处理的约束模式，并提出了改进自动化 ZK 验证的具体研究方向。

方法论

1. 在 SMT‑LIB 中建模 ACIR – 作者将每条 ACIR 指令（加法、乘法、布尔逻辑等）映射到有限域上的相应多项式方程。他们扩展了标准的 SMT‑LIB 理论以支持域算术，使 cvc5 能够推理 Noir 程序的精确语义。
2. 约束完整性检查 – 对于给定的 Noir 程序，NAVe 生成两组公式：(a) 开发者表达的 预期 关系，(b) 派生 的 ACIR 约束。验证器询问 cvc5 派生约束是否蕴含预期关系，反之亦然。
3. 自动化流水线 – 该工具与 Noir 编译链集成：在编译为 ACIR 后，NAVe 自动提取 SMT 表示，运行求解器，并将任何不匹配报告为潜在错误。
4. 实证验证 – 作者在四个程序套件上运行 NAVe：(i) 一个简单的“年龄验证”示例，(ii) Merkle 树包含证明，(iii) 保密交易电路，(iv) 一个旨在对求解器进行压力测试的合成基准套件。

Results & Findings

• 高检测率 – NAVe 在四个套件中发现了 7 处先前未知的约束错误，其中包括事务电路中缺失的范围检查，该检查本可防止溢出攻击。
• 低误报开销 – 每个程序的验证时间在 0.3 秒（小示例）到 12 秒（大型 Merkle‑tree 证明）之间，远低于典型开发者的 CI 流水线的容忍范围。
• 可扩展性限制 – 识别出的“难以检查”约束模式涉及嵌套的非线性域运算与条件分支相结合；cvc5 在这些情况下在 30 秒后超时，凸显了当前 SMT 在 ZK 电路方面的能力缺口。

实际意义

• Developer confidence – 通过将 NAVe 集成到 CI/CD 中，构建基于 Noir 的 zk‑app 的团队可以在部署前自动捕获约束错误，减少昂贵的审计后修复。
• Audit acceleration – 审计员可以将 NAVe 作为第一道合理性检查，将手动工作重点放在剩余的边缘案例上，而不是重新推导整个电路。
• Toolchain standardization – 正式的 SMT 编码为不同的 ZK 框架（例如 Noir、Circom）提供了通用语言，以实现互操作，可能支持跨编译器验证。
• Performance budgeting – 知道对真实电路的验证只需几秒钟，使工程师能够在不牺牲开发速度的情况下分配资源进行自动化测试。

局限性与未来工作

• 求解器覆盖范围 – 当前的 SMT 求解器在处理深度嵌套的非线性约束时表现不佳，导致在某些复杂的 Noir 程序上出现超时。
• 部分语言支持 – NAVe 目前仅处理 ACIR 的核心子集；自定义 gadget、外部哈希函数或递归等扩展尚未建模。
• 用户友好的诊断 – 错误报告仍然是低层次的 SMT 不可满足核心；未来的工作旨在将这些信息映射回高层的 Noir 源代码位置，以便更容易调试。
• 更广泛的基准套件 – 将评估扩展到更多生产级别的 Noir 项目以及其他 ZK 语言，将有助于验证可扩展性和通用性。

底线： NAVe 证明了对 ZK 程序进行形式化、自动化验证不仅是可行的，而且对日常开发也实用。随着零知识技术从研究实验室走向生产系统，像 NAVe 这样的工具将成为确保其所承诺的密码学保证的安全性和正确性所必不可少的。

作者

• Pedro Antonino
• Namrata Jain

论文信息

• arXiv ID: 2601.09372v1
• Categories: cs.CR, cs.FL, cs.SE
• Published: 2026年1月14日
• PDF: Download PDF