Bounded Verification for Finite-Field-Blasting

Bounded Verification for Finite-Field-Blasting” by Alex Ozdemir, Riad S. Wahby, Fraser Brown, and Clark Barrett. In Proceedings of the 35^th International Conference on Computer Aided Verification (CAV '23), (Constantin Enea and Akash Lal, eds.), July 2023, pp. 154-175. Paris, France.


Zero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement without 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 compromise the statement that the ZK proof is supposed to establish. This paper takes a step towards ZKP compiler correctness by partially verifying 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 define 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.

BibTeX entry:

   author = {Alex Ozdemir and Riad S. Wahby and Fraser Brown and Clark
   editor = {Constantin Enea and Akash Lal},
   title = {Bounded Verification for Finite-Field-Blasting},
   booktitle = {Proceedings of the {\it 35^{th}} International Conference
	on Computer Aided Verification (CAV '23)},
   series = {Lecture Notes in Computer Science},
   volume = {13965},
   pages = {154--175},
   publisher = {Springer},
   month = jul,
   year = {2023},
   doi = {10.1007/978-3-031-37709-9_8},
   note = {Paris, France},
   url = {}

(This webpage was created with bibtex2web.)