One-Pager: Formal Verification of GROTH16 Zero-Knowledge Proof Scheme

Introduction

The formal verification of the GROTH16 zero-knowledge proof scheme is a central effort under the zkproof.org standardization workshop (stream, slides), endorsed by prominent researchers including Professor Shafi Goldwasser and Professor Dan Boneh. This initiative aims to ensure the reliability and security of cryptographic protocols widely used in blockchain applications.

This one-pager addresses critical questions and aspects that arise in this context, providing a detailed framework for understanding the scope, approach, challenges, and deliverables. Insights from experts in the field have been synthesized to guide this effort, ensuring it is both comprehensive and actionable.

Our motivation is end-to-end trust in deployed schemes

Summary: Verifying GROTH16 is a strategic starting point due to its simplicity and widespread use. The effort is motivated by the need to provide strong guarantees of correctness, which can enhance trust in the ecosystem. The Ethereum Foundation's interest in funding this effort underscores its importance.

Discussion:
Carla agreed with Matter Labs that verifying GROTH16 is a good starting point, given its simplicity and widespread use. Marco also highlighted that formal verification of GROTH16 is a good use case, providing strong guarantees of correctness. Denis emphasized the importance of motivating formal verification people to work on the effort, noting that the Ethereum Foundation's interest in funding this project underscores its significance.

We selected the Groth16 scheme, but still need to pick a variant

Summary: Given the multiple variants of GROTH16, the focus should be on the most popular and widely used implementations, such as those in Circom, Semaphore, TornadoCash, GNARK in ConsenSys, Worldcoin, Succinct SP1, and BNB. Starting with Plonk might also be considered due to its increasing usage. The goal is to select a variant that maximizes impact and community adoption.

Discussion:
Marcin noted that GROTH16 is used in various implementations like Circom and GNARK, but these differ from each other. He highlighted the importance of selecting the most popular variant to maximize impact. Carla mentioned that GROTH16 is the most "standard" and simplest to verify, making it a good starting point. Justin pointed out that there are multiple variants of GROTH16, suggesting the need for careful selection. Marcin also suggested considering Plonk due to its growing popularity.

The scope of the Verified Verifier is deep before we expand

Summary: The formal verification effort for the GROTH16 zero-knowledge proof scheme should encompass both Solidity and EVM implementations. The scope should include verifying the precompiles and elliptic curves used in the protocol. This comprehensive approach ensures that all critical components are covered, providing a robust verification framework.

Discussion:
Marcin raised the question of whether the formal verification should be done in Solidity or EVM, highlighting the importance of covering both implementations. He also emphasized the need to include precompiles and elliptic curves in the scope, as these are critical components of the protocol. Ben echoed the importance of defining the scope clearly, questioning whether the verified verifier should only focus on blockchain uses, given the broader applicability of the technology.

Full Verification encompases the paper, the protocol, the implementation

Summary: The formal verification process should begin with a high-level description of the proof system, capturing families of proof systems that include GROTH16. This approach allows for a reusable framework that can be instantiated for specific variants like GROTH16. The verification should cover both the correctness of the protocol and the precompiles, ensuring that the implementation aligns with the theoretical proofs.

Discussion:
Marcin discussed the need for a part that shows GROTH16 does the correct thing and another part that looks at the precompiles. He also mentioned the importance of connecting a proof of the paper to the implementation. Denis suggested capturing families of proof systems, including GROTH16, to create a reusable framework. This approach ensures that the verification effort is broad enough to be useful for other proof systems as well.

The process: build momentum then get commitment

Summary: The process should be well-organized, starting small and finishing fast to build momentum. It involves getting commitments from key stakeholders and experts, defining clear tasks, and setting up a structured approach. Public challenges and competitions can be used to engage the community and validate the verification efforts.

Discussion:
Carla suggested getting organized and committing to the effort, asking about the process for the formal verification. She preferred starting small and finishing fast to build momentum. Marco outlined a plan to work on the formal verification effort, emphasizing the need for a structured approach. Ben proposed a format for the effort, including tasks and a process for engaging the community through public challenges and competitions.

The tools dictate some of the challenges

Summary: Key challenges include the complexity of proving elliptic curves, ensuring the protocol holds water, and addressing the malleability of GROTH16. The verification process must also handle the compilation from circuit to constraints and ensure that the prover is correctly implemented. Collaboration with experts and leveraging tools like EasyCrypt can help mitigate these challenges.

Discussion:
Marcin mentioned that proving elliptic curves are correct is not easy, involving Rust and Golang. He also noted that it's not enough to have the verifier; the protocol must hold water, as it can forge proofs. Carla highlighted the malleability of GROTH16 and the need for changes to lock it down. Eli discussed the challenges of formal verification, including the need to be in touch with EasyCrypt people and spending a lot of time on simple math. Denis emphasized the need for a structured approach to address these challenges.

We should produce useful deliverables such as EVM elliptic curves proofs

Summary: The deliverables should include a formal proof of GROTH16 soundness, focusing on both the circuit and prover. Verification of elliptic curves in Geth and pairing verification as a precompile are critical components. The effort should also produce a verified verifier that is efficient and can be used by the community.

Discussion:
Marcin mentioned the formal proof of GROTH16 soundness, noting that it involves both the circuit and prover. He proposed formal verification of elliptic curves in Geth, as it gives the most value to the community. Carla highlighted the efficiency of the verifier, mentioning public input exponentiation and three terms. Marco outlined the deliverables, including writing polynomials for proof of GROTH16 proof itself. Denis provided a timeline and deliverables for the effort, while Ben asked how to appreciate complete, difficult, or incomplete formal verification efforts.

Thoughts on budget sources focus on the Ethereum ecosystem

Summary: The Ethereum Foundation has indicated a willingness to fund up to $20M for a general formal verification effort, which includes proving zkEVM correctness and formal semantics for RISC-V. A detailed budget should be prepared to outline the costs associated with the verification tasks, expert consultations, and community engagement activities.

Discussion:
Marcin noted that Ethereum wants to fund $20M to prove zkEVM correct and formal semantics for RISC-V. Denis mentioned the budget for the formal verification effort, emphasizing the need for a detailed budget to outline the costs associated with the tasks, consultations, and community engagement.

Create public challenges to mitigate risk of low participation

Summary: Risks include the potential for incomplete or incorrect formal verification and lack of participation or engagement. Mitigation strategies involve conducting the effort as a public activity, organizing challenges, and ensuring expert review. Incremental progress and clear milestones can help manage these risks.

Discussion:
Marcin expressed uncertainty about the interest in verifying the verifier, as it's hard to get the verifier wrong. Ben mentioned the risk of incomplete or incorrect formal verification and suggested mitigation strategies, including public challenges and expert review. He also highlighted the risk of lack of participation or engagement, emphasizing the need for incremental progress and clear milestones.

From families of proofs around Groth16 to other schemes

Summary: The effort should also consider the broader implications and lessons learned from the verification process. This includes understanding the complexities of formal verification, the need for a structured approach, and the potential for generalizing the results to other proof systems. Engaging with the community and leveraging existing resources and expertise will be crucial for the project's success.

Discussion:
Marcin explained that GROTH16 is simple, just passing points to a pre-compile, and gave GNARK as an example of a zkSNARK implementation. Carla mentioned her work on making GROTH16 simulation extractable and commit and proof extension for relaxed R1CS. Eli shared his experience with formal verification and mentioned a DSL for MPC programs. Marco discussed writing correct circuits and using a typical approach for verification. Denis emphasized the importance of capturing families of proof systems and suggested talking to experts in the field. Ben referenced ZPrize activities and mentioned the team involved in the effort.

Conclusion and Next Steps

To successfully verify the GROTH16 zero-knowledge proof scheme, the following concrete steps are recommended:

1. Define Scope: Clearly outline the components to be verified, including Solidity, EVM, precompiles, and elliptic curves. This ensures all critical parts of the protocol are covered.
2. Select Variant: Focus on the most widely used variant of GROTH16, such as those in Circom, Semaphore, and GNARK. This maximizes community impact and relevance.
3. Develop Approach: Start with a high-level description of the proof system and capture families of proof systems that include GROTH16. This creates a reusable framework for future verification efforts.
4. Organize Process and Budget: Establish a structured process with clear tasks and milestones. Engage key stakeholders and experts. Interested parties, including those who want to secure their zero-knowledge proof implementations, should be involved. The Ethereum Foundation's interest in funding this effort underscores its importance.
5. Tool Selection and Expert Consultation: Identify and evaluate tools like EasyCrypt and Lean for the verification process. Discuss with experts the pros and cons of each tool to determine the most suitable one for the effort. Teams may present their preferred toolsets, which should be taken into account.

By following these steps, the formal verification of GROTH16 can provide strong guarantees of correctness, enhancing trust in cryptographic protocols and benefiting the broader blockchain ecosystem. This effort, blessed by leading researchers and supported by the Ethereum Foundation, aims to set a new standard in zero-knowledge proof verification.

ANNEX - Interviews on Formal Verification of a zkSNARK Verifier

MARCIN start

fv of verifiers

in solidity? / evm

groth16 on evm

what happens is simple

• points in input
• do nothing to them
• pass to pre-compile
• doesn't do much

gnark is example

if evm has formal

scope

• precompiles are part of the effort?
• curves are part of the effort?

with evm

part that shows groth16 does the correct thing

part that looks at the precompiles

• prove ec are correct
• not easy rust + golang

eth want fund 20M

• prove zkEVM correct
• correct formal semantics for risc-V
• could have that as a target

formal proof of f16 soundness

• but then circuit AND prover

not sure verif very interesting

• hard to get verif wrong
• whole prot is interesting

not enough to have verif

• talk from oana
• protocol doesnt hold water
• can forge proofs in the prot
• the verif doesnt do anything
• compilation from circuit to constraints
• proto talks about the constraints

the protocols are the dragon

• prover is part of it

connecting a proof of the paper to implementation

• this implem does what the paper says
• issue groth16 doesnt exist anymore
• g16 in circom = paper
• in gnark = different proto
• lego stuff, committing 2
• implement lut for g16
• vanilla g16 doesnt get much
• unsafe when modified e.g. gnark was unsafe

which g16 to pick

• most popular + get funding
• all use ec precompiles

wheere do you stop the proving

• trust rust compiler?
• do right thing in risc5, then other architecture?
• do you trust llvm

g16 used

• circom but not future proof maybe?
• semaphore, "tornadocash"
• gnark in consensys, worldcoin, succint sp1, bnb

maybe first plonk?

• probably more used?
• scattering worse

proposal

• fv ec in geth gives most value to community
• pairing verification is a precompile too
• everyone uses these precompile
• some evm verifier
• the protocol itself

MARCIN END

Carla START

Why do it

• agree with ben / matterlabs
• zkp built such
• if verified correct, lots of guarantees
• verifying is good starting point
• groth16 not even with fiatshamir, simplest to verif
• groth16 most "standard" used, simple, there for while

next

• need to get organized
• happy to commit IF team
• cant push this
• share who's part of the effort

who are the people

• 11 ppl

whats the process

• are there extensions to groth16?
• very concrete problem
• what does it mean family
• universal?! more complex

preference

• start small finish fast
• then can continue
• if you go for generalization, what you get out of it

worked on groth16

simulation extract

• paper on making g16 simulation extractable
• needs changes, because g16 malleable
• only allows to randomize proofs, for same statement
• lock it down with e.g. extra group element + hash functions
• other ways by gabizon
• how to minimize comm complexity

commit and proof extension

• (works for relaxed r1cs)

works on high level, not implementation

what could be a roadmap

verifier very efficient

• public input exponention
• three terms
• no hash

other critical parts that could be attacked

• trusted setup of course ultra-sensitive
• any leakage will lead to failure
• circuit

proof of groth16 proof itself

• wrote polynomials
• typical algebraic proof
• lends itself
• almost symbolic
• "this coef needs to be zero here, there"
• can be verified by computers

Carla END

ELI START

took fv class

• fresh on mind
• understand verif doing
• candidate for fv

phd in mpc

• cryptography adv varia @ bu
• fv of mpc, fv secure computation

good application

• can fv mpc
• lotts of moving part
• spec mpc protocol
• proofs in paper hold
• long way to implementtaion is secure
• long way to a prog you write in my impl is secure
• mpc allows you to write mpc prog easily
• when its done, proof went thru

tool

• easycrypt
• talked to Denis
• good tool maybe not best
• why not use coq, lean (heard arguments)
• rough around edge, works, not ergonomic
• concerned do for huge proj
• easycrypt good bceause authors wanted those things
• similar to already been done
• like learning language, map mental model on other
• got lots easycrypt at bu

early dec 24 @ bu

• conf
• knows eran

from experience

• proj in easycrypt, need to be in touch w/ easycrypt ppl
• need to add features to system
• lots of time on very simple math
• a + b + c = c + b + a, but field mod prime not in lib
• ppl writing verif paper dont want to do it
• probablistic is baked into easycrypt, well suited

suspicion

• coq lean can get 90% very well
• easycrypt 90% was impossible, 10% was already there
• prof was easycrypt contributors
• denis is contrib

dsl for mpc programs

• today write in c++ and compile
• if you got dsl, easy to fv

ELI END

JUSTIN START

There's more than 1 Groth16

• https://hackmd.io/@nebra-one/Bk2E3JfJA

JUSTIN END

marco START

• surprised by excitement verif verif
• been around alot
• very hard to sell
• refreshing
• disusional thats its easy

use-case

• in gen security is good home for fv
• expensive, has to be worth it
• here nice reducible piece
• supercritical, not huge
• used, easy to share cost, risk

plan to work up

prob

• crypto engineer add layers to the cake
• then impossibleto sell
• g16 wrapper over plonkish fri over snark

work

• writing correct circuits
• eprint CLAP: producing correct circuit
• not under/over constraint
• step afetr verif verifier
• usetypical apporach fri verif that checks other proof
• use circuit langauge plonkish arithmetiszation
• different from x86/risc5/llvm target

deliverable

onchain

• groth16 for onchain use
• smart contract in yul for the evm
• yul - low level assembly
• bn curve, first deliverable, used for lots of other things
• if we do bncurve its useful for plonk-kzg

cpu version

• fast verifying bn curve
• g16 ontop
• might get "explosion", i want the portable version
• i want avx512, arm version
• portable?
• risc v? not many actually run?

people & companies

hacl*

• specify in f* (not super common)
• outputs c code maybe also rust
• cryptotgraphers want to look at the actual code
• easy to integrate into existing proj
• google using for parts of proof chains
• very portable
• BUT: trust compiler to not introduce bugs
• speculative exec attacks, low level, not covered unless
• using full blown compcert, and then even.
• doable, proj hacl* connected to ms research + INRIA
• (compcert did work in coq then equivalence in each layer)
• hacl* -> https://www.inria.fr/en/karthikeyan-bhargavan
• https://cryspen.com/
• instead of waiting for phd student, they pay the person
• have experience for elliptic curves
• "industrial support"

fiatcrypto - http://adam.chlipala.net/

• coq
• good example of success
• produce low level code
• have examples of ec
• convince that enough dev time behind

easycrypt

• jasmin language, low level assembly
• from spec down to assembly
• security proof in easycrypt down to lowest level
• no compiler to trust

bas spitters

• https://users-cs.au.dk/spitters/
• smart contracts

clients today

cpu

• aleo
• mysten labs
• zcash forks

evm

• all of ETH using g16 to recurse
• risc0
• polygon
• "tornadocash"-like
• g16 and plonk-kzg are the only cost-effective ones

who runs?

• digital wallet for europe, verif identity on phone?
• outside of blockchain bn curve not top top top

note on bn

• outside of evm e.g. bls is better

MARCO END

tobias tu munich START

formalizing kzg

• isabelle theoreme prover
• discrete log done
• pederson ongoing
• not used in groth16

isabelle comments

• math library, not as extensive as Lean
• has nice framework for game based proof
• sequences of games
• negligeability issue
• easycrypt might be better fit negligeability statemnts
• extracted one negligeability for kzg, so ok

good in isabelle / lean vs easycrypt

• Schwarz Zippel lemma:
• poly distinct enough on big domain, wont evaluate same (negligeable)
• used in plonk

acaedmic recognition

• prob not

TOBIAS END

DENIS START

Pitch to EF

Motivation

• start with something concrete
• but limited value from fv pov
• how can we be useful for more than just Groth16
• binary blessed secure version of just groth 16

Challenges back & forth

• fitting ZKProof is its own reward
• 12mo worked on it, but i dont use g16,
• i get discuraged, unless you structured correctly
• i only get a boolean "yes its possible"
• a better way is reusable for me

Motivate FV ppl, it's a bar

• broad enough result
• start with family of proof systems that contains Groth16
• high level ingredients mixed together to get G16
• high level description
• later instanciate to e.g. groth16
• proof that this generic descr is reasonable
• e.g. if you prove security of schnorr, you still need to formalize sigma-protocols

Capture families

• reasonable approach from community
• do 1 and move on
• e.g. we captured sigma-protocols, then schnorr
• this exercise we solved issues
• if we had approached schnorr but not sigma, we would actually
• get sigma but not recognizable form, so useful to
• we then did schnoor, hamilton, fiat-shamir, useful for more
• hamilton would not have been achieved without the theory effort

It's a waste

• to do all this theory for just one tiny groth16 result
• it's discouraging, all this work for just 1 result
• e.g. specifying for sorting function, not bubble sort

Ressources

• [1] https://eprint.iacr.org/2023/656.pdf

Talk to

• Matteo Companelli: what's the family that groth16 belongs that contains others
• Tight family, interesting
• Broad family is the proof system itself
• in [1] they designed in a reusable way

Tech description

Timeline and deliverables

• 12mo

Budget

Cautionary tale

• CompCert so complicated, Heroic effort
• C compiler
• Human effort too much
• Instead of encouraging with "playbook"
• We discourage from all the hard work

Lots to learn

• describing distrib low level and reasoning high level not easy
• not the boolean result but the lessons and generalizations
• example: boost sort function ojava had 3 bugs discovered in master thesis
• modulo sum equivalence considered equal

Denis END

Ben START

Verified Verifier

risk

• half proofs for the statement of its verified
• cut corners

mitigation

• do as public activity
• need public challenge
• "fraud proof" :) gamify it

format

• first a call for paper
• focused zkproof track on verified verifier
• then a competition

joker

• "present to Shafi and Dan"
• intrisic reward
• not show inprogress but more baked

how to appreciate complete / difficuly / incomplete

• easycrypt and compare progress
• cant do from sidelines

tasks

• recruit fv "known figures"
• budget for 12mo, whats the spend
• fundraise small focused budget
• experienced tech pm type
• concrete proposals, spelled out

targets

• ef
• a16z

team right now

• ben, jon, james, denis
• 6 more ppl from the conf

refs

• zprice activities: https://www.zprize.io/blog/announcing-zprize-results
• public discussion period

succeed. / fail

• lack of perticipation?
• not engaged enough
• top univ gallois castrel great outcome
• not if half assed by tangent ppl

process

• long list of teams
• not only blockchain its very small
• marcin galois veridice
• outside ppl verif general sense

target time to ef

BEN END

Work document compiled by Jonathan Rouach, June 2024, for ZKProof.org