Formally Verifying Noir Zero Knowledge Programs with NAVe
本文介绍了 NAVe，这是一个开源形式化验证器，它通过将 Noir 零知识程序的 ACIR 中间表示转换为有限域多项式方程，并利用 SMT-LIB 和 cvc5 求解器来形式化验证其正确性和属性约束。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下你正在建造一个高安全性的保险库。你想向银行经理证明你知道保险库的组合密码，但又不想直接告诉他组合到底是什么。这就是**零知识证明（Zero-Knowledge Proofs, ZK）**的魔力。
然而，建造这些保险库非常棘手。这些证明的“蓝图”是复杂的数学谜题，被称为算术电路（arithmetic circuits）。如果蓝图中哪怕只有一行错了，保险库可能就不安全，或者证明会失败。
这篇论文介绍了一个名为 NAVe（Noir Acir Verifier）的新工具，旨在这些蓝图投入使用之前检查其中的错误。以下是其工作原理的简单解释：
1. 问题所在：“秘密配方”与“食谱”
作者关注的是一种名为 Noir 的编程语言。你可以把 Noir 看作是一本高级“食谱”，它让编写这些保险库的“配方”变得简单易行。
- 厨师（开发者）： 用易于阅读的 Noir 编写配方。
- 翻译官（编译器）： 将该配方转化为一份严格的低级指令手册，称为 ACIR。这份手册是一系列计算机必须求解的数学方程列表。
- 危险之处： 有时，翻译官会犯错，或者厨师忘记包含某个关键步骤。在零知识证明的世界里，这被称为“约束不足”（under-constrained）。这就像是在写一份配方时写了“加盐”，却忘了说明要加“多少”。结果可能勉强能吃，但并不是你原本想要的那道菜。
2. 解决方案：“数学侦探”（NAVe）
作者创建了 NAVe，一个形式化验证器。你可以把 NAVe 看作是一个超级聪明的数学侦探，它通过阅读低级的指令手册（ACIR），来检查数学逻辑是否真的符合厨师的初衷。
NAVe 使用一个强大的逻辑引擎（称为 SMT 求解器）来提出问题，例如：
- “如果我输入一个秘密数字，数学运算是否始终能得出正确的公开证明？”
- “是否有任何方法可以用一个假数字来欺骗系统？”
如果数学逻辑出了问题，NAVe 不仅仅是显示“错误”。它会像侦探发现线索一样：它会向开发者展示他们可以使用哪个数字来破解系统。这有助于他们立即修复蓝图。
3. 两种解题方式
论文描述了 NAVe 将数学谜题转化为求解形式的两种不同方式：
- 整数方式： 它将数字视为普通的整数（1, 2, 3...），并使用标准的算术规则进行检查。
- 有限域方式： 它将数字视为在一个循环时钟上的数值（当达到某个数值后，会绕回零）。这就是实际零知识证明运作的方式。
作者发现，没有哪种方法对所有情况都完美适用。有时，“整数”侦探速度更快；有时，“有限域”侦探表现更好。他们建议同时使用这两位侦探以获得最佳结果。
4. “约束不足”的陷阱
Noir 有一个独特之处，即“无约束代码”（unconstrained code）。想象一下，在配方的某个部分，厨师被允许在不经过检查的情况下“猜测”食材。这对于提高速度很有用，但如果厨师猜错了，就会非常危险。
- 风险： 开发者可能会编写看起来在检查食材的代码，但由于这段代码处于“无约束”部分，计算机实际上并不会强制执行检查。
- NAVe 的职责： NAVe 会专门寻找这些“幽灵检查”。它会验证即使开发者使用了“猜测”部分，他们是否也添加了一个独立的、严格的规则（
assert），以确保这个猜测确实是正确的。
5. 他们的发现
作者在各种现有的 Noir 程序上测试了 NAVe：
- 有效性： 在程序数学逻辑与意图不符的情况下，NAVe 成功捕捉到了错误。
- 瓶颈： 他们发现，检查“范围约束”（确保一个数字落在特定的位数范围内，例如检查一个数字是否在 0 到 255 之间）对数学侦探来说非常困难。这有时会导致耗时过长或陷入停滞。
- 未来方向： 他们计划构建更好的“捷径”（抽象层），以帮助侦探更快地解决这些棘手的范围谜题。
总结
简而言之，NAVe 是为构建隐私保护应用的开发者提供的一道安全网。它将开发者的代码转化为一种严格的数学语言，并利用强大的求解器来确保代码确实实现了它声称的功能，从而捕捉到那些可能导致安全失效的细微漏洞。这就像是在任何人允许开车通过之前，都有一个严谨的检查员来检查桥梁的结构完整性。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。