Welcome to the resource topic for 2023/778
Title:
Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)
Authors: Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark Barrett
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.
ePrint: https://eprint.iacr.org/2023/778
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .