Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs
summary
Tool QED2 performs semantic reasoning over Circom-generated polynomial equations by combining SMT solving with lightweight uniqueness inference in an interactive loop to prove whether each signal is uniquely determined by inputs. It evaluates 163 Circom circuits, solves 70% of benchmarks with ~18s average per case, either verifying uniqueness or producing a pair of witnesses, and uncovers 8 previously unknown vulnerabilities in widely used circuits.
AI-written summary · about
chapters (11)
- 0:00Under-constrained ZK circuits
- 1:48Zero-knowledge proofs applications
- 3:35Witness generation mismatch
- 5:45Under-constrained bugs consequences
- 6:48Real-world constraint bug
- 7:32SMT solvers vs static analysis
- 8:55QED Squared tool design
- 11:25ZK Bench overview
- 12:06Tool evaluation results
- 13:50Conclusion and open-source
- 14:35Q&A
related talks
23mZKBoo: Faster Zero-Knowledge for Boolean Circuits
48mProving UNSAT in Zero Knowledge
43mPushing the Limits of Zero Knowledge Applications
41mGKR based Zero-Knowledge Proofs
14mStatic Analysis for Zero-Knowledge Programming Languages
51mDistributed Zero-Knowledge Proofs and Applications to Secure Computation
01h 06mLattice-based Zero-knowledge Proofs
33mAn Introduction to Zero Knowledge Proofs