本文探讨了如何形式化验证零知识证明系统中使用的算术电路的特性,如完备性、可靠性和零知识性。文章介绍了使用证明辅助工具和不使用证明辅助工具的不同验证技术,并讨论了形式化验证在零知识电路中的应用,包括问题分解、语义设计以及代码的综合验证,同时概述了当前的研究进展和未来的研究方向。
由 Morgan Thomas 和 Ventali Tan 撰写
感谢 Kestrel Institute 的 Eric McCarthy 在本文档的某些章节提供的帮助,以及 Grigore Rosu (UIUC)、Shashank Agrawal (Delendum)、Daniel Lubarov (Delendum)、Tim Carstens (Risc Zero)、Bolton Bailey (UIUC)、Alessandro Coglio (Kestrel) 和 Mikerah 提供的许多有益建议。
我们如何形式化验证一个算术电路(正如 零知识证明系统 所使用的)具有所需的特性,例如可靠性、完备性和零知识性¹?
证明系统的可靠性意味着它不会证明错误的陈述。类似地,证明系统所使用的电路的可靠性意味着这些电路在应用于不真实的陈述时是不可满足的。
证明系统的完备性意味着它能够证明所有真实的陈述。类似地,证明系统所使用的电路的完备性意味着该电路在应用于真实的陈述时是可满足的。
电路的可靠性和完备性加在一起,等同于电路所表示的关系是预期关系这一陈述。
一个证明系统是零知识的,当且仅当一个证明没有揭示任何超出被证明陈述(即,证明过程的公共输入)的额外信息。任何被证明的陈述直接暗示的事实必然也被证明所暗示,但不应揭示未被陈述暗示的额外事实。额外的“非公共”见证数据(可以被视为秘密输入)不得被揭示。
一个可靠且完备的电路只能被在预期语义中为真的陈述所满足。如果底层证明系统是可靠且完备的,并且如果电路是正确的,那么整个系统提供了一种证明预期陈述的可靠且完备的方法。我们可以将主要问题分解为两个子问题:验证底层证明系统的所需特性,以及验证电路的可靠性和完备性。换句话说,电路表示预期关系,并且证明系统在应用于电路时将按预期运行。
我们这里的主要重点是第二个子问题,即验证系统的电路,同时假设底层证明系统的可靠性和完备性。
零知识证明系统经常使用数学约束系统(如 R1CS 或 AIR)来编码计算。零知识证明是一种概率密码学证明,证明计算完成正确。对零知识证明中使用的电路进行形式化验证需要(1)电路旨在编码的关系的形式化规范,(2)电路语义的形式化模型,(3)电路本身,(4)定理证明器,以及(5)关于(1)、(2)和(3)之间关系的定理的机械化证明。
要确定地证明一个通用陈述,它必须是一个纯粹的数学陈述,可以通过仅仅推理来知道它是真的,而不需要执行任何测试。推理必须从一致的假设(公理)开始,并通过保持真理的推论进行。
一种证明理论(有时也称为逻辑或元逻辑)编纂了一套一致的规则,用于执行保持真理的推论。证明理论可以用来手动构造证明,用笔和纸。
被称为证明助手的计算机程序通过帮助用户构造机器可检查的证明来减少劳动并降低人为错误的风险。
要使用证明助手来证明关于程序的陈述,有两种主要方法:
在这些方法中,(1)似乎更可取,因为证明是关于正在执行的(源)程序的确切证明,而不是转译器的输出,而后者被假定为与源程序具有相同的含义,从而提供了更大的信心。
当(由于任何原因)证明助手语言不适合作为开发应用程序的语言时,会激发方法(2)。
也有一些方法可以在不(直接)使用证明助手的情况下证明关于程序的陈述:
请注意,经过验证的编译器和验证编译器之间存在区别。CompCert 本身被证明可以生成始终在语义上等效于 C 输入的二进制文件。一个验证编译器生成一个二进制文件,以及一个正确性证明,证明该二进制文件在语义上等效于源代码。
当程序由验证或经过验证的编译器编译时,我们说编译器输出通过构造是正确的(前提是输入是正确的)。
经过验证的编译器不会检测或修复输入源代码中的错误;但是,它们也不会在编译期间引入任何新错误。
所有这些方法都有局限性:
概率证明系统(包括 ZK 证明系统)的形式化验证包括两个主要问题领域:
问题(1)通常被认为是一个非常困难的问题,并且尚未针对任何重要的证明系统完成。
问题(2)可以使用关系的形式化规范和电路语义的模型来完成。通常,它需要证明关系中定义的功能的功能正确性,以及每个函数参数的见证变量的存在。
请注意,有不同的方式来公理化一个问题以证明它。一些类别是指称语义、公理语义和操作语义。
_操作语义对于证明程序的属性特别有用。例如,在 ACL2 定理证明器中,形式化编程语言语义的常用方法是解释性操作语义,即用定理证明器的逻辑编写的高级解释器,它形式化了计算状态的可能形式,并描述了编程语言的构造(例如表达式和语句)如何操作计算状态。_
指称设计为思考一般和特定应用问题空间提供了一种有用的方式。
指称设计提供了一种方法论,用于定义系统(例如零知识证明系统)的需求,以便可以在形式系统中表达和证明需求。
电路表示一个集合:即,电路可满足的公共输入(即陈述)的集合(即,该陈述为真)。
例如,考虑一个哈希验证电路:
电路验证的目标是证明电路表示预期的关系。
通用证明系统验证的目标是证明它在电路的指称语义方面具有预期的属性:
图 1:指称设计
*该图的形式化版本在 Sigma 算术化 论文 (第 47 页的 288)中。这是一个 交换图 。电路编译器的可靠性和完整性都通过该图通勤的陈述来表达,这意味着通过它的同一对象之间的所有路径都是相等的,或者换句话说,编译电路的表示始终等于规范的表示。
如果你知道你的电路表示你想要的关系,并且你知道你的通用证明系统在上述意义上是可靠且完整的,那么你知道你的特定于应用程序的证明系统(即,电路加上通用证明系统)对于该应用程序具有预期的可靠性和完整性属性。
这表明,给定一个经过形式化验证的通用证明系统,以及一个从陈述到电路的经过验证的编译器,人们可以解决证明特定于应用程序的证明系统的正确性的问题,而无需特定于应用程序的正确性证明。
假设
然后,人们可以生成经过形式化验证的特定于应用程序的概率证明系统,而无需为其他应用程序编写任何额外的证明。这似乎是朝着一种可持续且具有成本效益的 ZK 电路形式化验证方法迈进的有希望的方法。
弥合我们可以证明的定理和我们可以执行的代码之间的差距通常是一个挑战。例如,我们可能能够证明关于规范的定理,并对该规范进行编码,但随后无法证明该代码实现了规范。或者,我们可能能够证明关于一些代码的定理,但无法将该代码编译为高效的机器代码。或者,我们可以做到这一点,但无法证明机器代码具有与源代码相同的语义。
以下是生态系统支持经过验证的代码高效执行的一些方式的摘要:
在现代计算的背景下,大多数计算密集型任务都处理向量数学和其他可以在专用硬件(如 GPU、FPGA 和 ASIC)上最有效地完成的令人尴尬的并行问题。
这通常适用于在概率证明系统中构建证明的问题。如果概率证明系统的证明器在专用硬件上实现,则它们将是最有效的,但在实践中,由于在 CPU 上编程更容易以及劳动力市场上更容易获得这些技能,因此它们通常在 CPU 上实现。
对于创建概率证明系统的经过形式化验证的高效执行的实现,正确的做法似乎不是优化 CPU 上的执行速度,而是针对专用硬件,如 FPGA、GPU 或 ASIC。
不幸的是,据我们所知,用于编译经过形式化验证的程序以在 FPGA、GPU 或 ASIC 上运行的工具几乎不存在。
在硬件验证的背景下,存在数十年关于算术电路形式化验证策略的研究。
存在数十年关于证明概率证明系统的可靠性、完整性和零知识性的研究。
例子:
Orbis Labs 正在进行:
Kestrel Institute 是一个研究实验室,已经使用 ACL2 定理证明器证明了许多 R1CS 小工具的功能正确性。(Kestrel 还做了很多其他的 FV 工作,包括在 Yul、Solidity、以太坊和比特币上。Kestrel Institute 拥有用于从使用 APT 工具包的正式规范中正确构建代码合成的工具,以及使用 Axe 工具包的事后验证,以将二进制文件、字节码和 R1CS 提升到逻辑中,以便根据正式规范进行验证。)
Aleo 正在开发诸如 Leo 之类的编程语言,这些语言可以编译为诸如 R1CS 之类的约束系统。
Nomadic Labs 是一家咨询公司,在 Tezos 上做了很多工作,并且在 Edo 升级时将 Zcash Sapling 协议的受保护交易构建到 Tezos 区块链中。Kestrel Institute 形式化验证了该协议中使用的一些 R1CS。 (Nomadic Labs 也做了很多其他的 FV 工作。)
Andrew Miller 和 Bolton Bailey 正在使用 Lean 定理证明器 在 代数组群模型 中对各种 SNARK 证明系统进行 形式化验证。
Starkware 正在编写 Lean 证明 以检查表示为 Cairo 程序的电路是否符合其规范。
Anoma 团队正在开发 Juvix 语言,作为创建比现有语言更健壮和可靠的,经过形式化验证的智能合约替代方案的第一步。
Veridise 正在进行:
Ecne 是一种专用自动证明搜索工具,可以证明 R1CS 约束系统定义了一个函数(全部或部分)。
来自斯坦福大学的 Alex Ozdemir 正在将有限域求解器添加到 cvc5 SMT 求解器。
来自以太坊基金会的 Lucas Clemente Vella 和 Leonardo Alt 正在研究 有限域上多项式方程的 SMT 求解器。
如果你喜欢我们在 “主要问题” 中构建的结构,你可以从以下几个方面分析每个研究工作/开发项目
关于约束系统形式化验证的项目的其他有趣属性是:
还有很多工作要做。在安全行业中,对形式化验证的重视程度不够。
基于这篇博文中提出的观察和论点,我们认为以下将是未来研究和开发的一些有趣方向:
1.为形式化验证零知识证明系统奠定基础
2. 改进的规范语言和规范语言之间的验证翻译器。
3. 了解如何创建经过形式化验证的程序以在矢量化硬件(例如,FPGA、GPU 和/或 ASIC)上运行。
4. 我们能否形式化验证旨在自动提高 ZK 电路效率的系统?例如:选择不同电路的系统,以便设置 MPC 更易于并行化,或者允许预先了解部分见证的证明者部分评估电路并使用此信息更快地计算证明的系统。
5. 使用 K 来证明关于 ZK 约束系统的陈述
¹我们在文章中没有描述零知识属性,并将撰写另一篇文章来描述它。要描述这一点,你需要深入了解私有输入的概念。(从隐藏明文中正确计算哈希的例子是理解这一点的绝佳例子。)零知识属性是从公共信息中确定私有输入的难度。如果你想使其具有零知识属性,你必须在约束系统中编码私有输入的某个难以反转的函数。零知识属性通常是一种概率度量。然而,如果计算过于简单且输出已知,则可能可以确定地确定输入。
²当存在一个与你想定义的新语言接近的形式定义的 DSL 时,转译器的想法最有意义,然后你可以从你的新语言转译到那个 DSL。然而,那个转译器也应该被形式化验证。
³在我们为具有一些密码组件的系统进行形式化验证的经验中,我们注意到了一些不同的事情:
(1)正式推理“整个”系统的安全属性极其困难。系统设计通常非常复杂,具有许多不同类型的依赖关系。即使是密码组件(从高层次上来说,可能非常小且简单(比如加密、MAC 等)),也可能以非常复杂的方式实现,并支持故障、恢复、备份等。因此,甚至以正式的方式对整个密码组件进行建模也极具挑战性。因此,我们得出的任何正式结论最终都只是针对整个系统的一小部分。我们的方法尚未发展到我们知道如何在形式证明中推理整个系统的程度。
(2)证明助手语言 —— 至少对于密码协议而言 —— 目前具有有限的表达能力。能够直接证明用 C 甚至 Rust 编写的密码协议的定理的工具有限。一般来说,协议开发人员需要处理多个线程和时间问题,而这些很难形式化。例如,Gallina(对于 Coq)没有这样的结构。从这个角度来看,Gallina 对开发人员不太友好,而使用线程的 Rust 则不然。未来正式推理并发软件系统的努力可能会受益于现有抽象的形式化,以便推理此类系统,例如进程演算,例如 π-演算。
⁴Common Lisp 可以被编译成相当高效的代码,非常接近 C 或 Rust。(但是,不如 GPU 高效。此外,并发编程虽然在 Common Lisp 中可用,但不是在其中定义形式逻辑的 ACL2 子集的一部分。)如果你编写了一个可执行的形式规范,那么它通常可以被编译成相当高效的代码,所有这些都发生在定理证明器的语言中。
术语:
如果你使用经过验证或验证的编译器用高级形式语言编写计算的规范并将编译到约束系统,则称为按构造正确。如果你采用现有的约束系统,并尝试证明关于它的属性(最多包括功能正确性),相对于高级形式语言的规范,则称为事后验证。
如果你有兴趣进一步讨论这个话题,或者在这个话题上进行合作,请考虑加入我们的 群聊 或通过 ventali@delendum.xyz 联系我。
- 原文链接: medium.com/delendum/form...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!