Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)

Alex Ozdemir; Riad S. Wahby; Fraser Brown; Clark Barrett

Paper 2023/778

Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)

Alex Ozdemir, Stanford University

Riad S. Wahby, Carnegie Mellon University

Fraser Brown, Carnegie Mellon University

Clark Barrett, Stanford University

Abstract

Zero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement with- out revealing any other information. Typically, statements are expressed in a high-level language and then compiled to a low-level representation on which the ZKP operates. Thus, a bug in a ZKP compiler can com- promise the statement that the ZK proof is supposed to establish. This paper takes a step towards ZKP compiler correctness by partially veri- fying a field-blasting compiler pass, a pass that translates Boolean and bit-vector logic into equivalent operations in a finite field. First, we define correctness for field-blasters and ZKP compilers more generally. Next, we describe the specific field-blaster using a set of encoding rules and de- fine verification conditions for individual rules. Finally, we connect the rules and the correctness definition by showing that if our verification conditions hold, the field-blaster is correct. We have implemented our approach in the CirC ZKP compiler and have proved bounded versions of the corresponding verification conditions. We show that our partially verified field-blaster does not hurt the performance of the compiler or its output; we also report on four bugs uncovered during verification.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. CAV'23
Keywords: zero knowledge compilers verification finite fields
Contact author(s): aozdemir @ cs stanford edu
History: 2023-05-30: revised; 2023-05-27: received; See all versions
Short URL: https://ia.cr/2023/778
License: CC BY

BibTeX

@misc{cryptoeprint:2023/778,
      author = {Alex Ozdemir and Riad S. Wahby and Fraser Brown and Clark Barrett},
      title = {Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/778},
      year = {2023},
      url = {https://eprint.iacr.org/2023/778}
}