Formal verification of zero knowledge gadgets

[EricM]

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

metastatedev/tezos/-/blob/sapling-integration/docs/developer/sapling.rst

Private Assets

As of recent weeks, Tezos for the first time has a public testnet running a protocol that allows users to take part in privacy-preserving transactions. Along with this comes a client hardcoded to work with an example contract making use of new Michelson primitives that verify zkSNARKs with Zcash’s Sapling cryptography. The client currently only works with this one contract, although multiple versions of the contract may be originated on-chain. This contract represents a simplistic version of som…

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.5), 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

[rafoo]

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)?

[EricM]

@rafoo

high-assurance field inversion for pairing-friendly primes

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.