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.
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:
- 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.
- 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.
- 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.
- 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.
- 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.
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
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
- 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
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
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
- 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 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
- 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
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
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"
- 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
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
- isabelle theoreme prover
- discrete log done
- pederson ongoing
- not used in groth16
- 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
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
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
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
- 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
team right now
- ben, jon, james, denis
- 6 more ppl from the conf
refs
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
Google Drive
Gist
Clipboard
-
Any changes
Be notified of any changes
-
Mention me
Be notified of mention me
-
Unsubscribe
Subscribe