Formal verification of zero knowledge gadgets

As you likely know, zero knowledge proofs are coming to Tezos.
Here are some links:

But how can you be sure that the R1CS gadgets are correct? R1CS gadgets serve to define zero-knowledge computations, but they can be hard to audit and it is easy to make mistakes.

At Kestrel Institute (www.kestrel.edu) we are working on formal verification of R1CS gadgets, in order to help bring formally verified zero knowledge proofs to Tezos.

To formally verify R1CS gadgets we (1) write a specification in the theorem prover, (2) lift the R1CS into logic, and (3) connect the two with a mechanized formal proof of functional equivalence. The proof effectively tests the gadget with every possible input.

We are using the ACL2 theorem prover (ACL2 Version 8.3), which is based on a subset of Common Lisp for which a formal logic is defined. This means programs can be both executed and reasoned about in the same language, which can also express high-level declarative specifications.

If you would like to check out the work please see
R1CS:
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=R1CS____R1CS
Some specifications:
https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ZCASH____ZCASH

6 Likes

Hello, I think formal verification of cryptography is very important. How does your work compare to the Fiat-Crypto project and in particular to their recent work entitled “High-assurance field inversion for pairing-friendly primes” (paper, presentation)?

The work we are doing for Tezos is post-hoc verification of R1CS code. The Fiat-Crypto work is synthesis of C code. The C code will be part of the codebase used to generate zero-knowledge proofs that someone ran the R1CS code correctly on their secret inputs, but does not address correctness of the R1CS code.