“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:
@inproceedings{OWB+23,
author = {Alex Ozdemir and Riad S. Wahby and Fraser Brown and Clark
Barrett},
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 = {https://link.springer.com/chapter/10.1007/978-3-031-37709-9_8}
}
(This webpage was created with bibtex2web.)