Formally Verifying Noir Zero Knowledge Programs with NAVe

TL;DR

This paper introduces a formal verification framework for Noir zero-knowledge programs by formalizing the ACIR language with SMT-LIB and developing an open-source verifier using cvc5, enhancing correctness assurance.

Contribution

It formalizes the ACIR language in SMT-LIB, creates an open-source verifier for Noir programs, and demonstrates its practical effectiveness on diverse program sets.

Findings

Verifier successfully checks Noir program constraints

Identification of a hard-to-check constraint type

Framework shows practical applicability across multiple programs

Abstract

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.