用NAVe形式验证Noir零知识程序
Formally Verifying Noir Zero Knowledge Programs with NAVe
AI总结：
本文提出使用NAVe形式化方法验证Noir零知识程序，通过SMT-LIB和cvc5求解器检查程序是否正确约束关系。
摘要：
零知识（ZK）证明系统是密码学协议，可以（以极高的概率）证明一对（X，W）处于关系R中，而无需暴露关于私有输入W的信息。这种成员检查通过复杂的算术电路捕获：一组在有限域上的多项式方程。像Noir这样的ZK编程语言已被提出，以简化这些电路的描述。开发者可以使用传统高级构造编写Noir程序，将其编译为更底层的ACIR（抽象电路中间表示），这本质上是对算术电路的高级描述。在本文中，我们使用SMT-LIB及其扩展的有限域理论形式化了一些ACIR语言。我们利用这种形式化来创建一个开源的形式验证器，用于Noir语言，使用SMT求解器cvc5。我们的验证器可用于检查Noir程序是否行为适当。例如，它可以用来检查Noir程序是否被正确约束，即生成的有限域多项式方程确实捕捉了预期的关系。我们对4个不同的Noir程序集进行了评估，证明了其实际应用性，并识别出一种难以检查的约束类型，这为我们的验证框架改进指明了方向。
英文摘要：
Zero-Knowledge (ZK) proof systems are cryptographic protocols that can (with overwhelming probability) demonstrate that the pair $(X, W)$ is in a relation $R$ without revealing information about the private input $W$. This membership checking is captured by a complex arithmetic circuit: a set of polynomial equations over a finite field. ZK programming languages, like Noir, have been proposed to simplify the description of these circuits. A developer can write a Noir program using traditional high-level constructs that can be compiled into a lower-level ACIR (Abstract Circuit Intermediate Representation), which is essentially a high-level description of an arithmetic circuit. In this paper, we formalise some of the ACIR language using SMT-LIB and its extended theory of finite fields. We use this formalisation to create an open-source formal verifier for the Noir language using the SMT solver cvc5. Our verifier can be used to check whether Noir programs behave appropriately. For instance, it can be used to check whether a Noir program has been properly constrained, that is, the finite-field polynomial equations generated truly capture the intended relation. We evaluate our verifier over 4 distinct sets of Noir programs, demonstrating its practical applicability and identifying a hard-to-check constraint type that charts an improvement path for our verification framework.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
