Attacker can bypass cryptography and prove mathematically impossible statements
8 hours ago
- #Cryptography
- #Fiat-Shamir
- #zkVM
- A zkVM verifier must ensure its public claims are faithful; if false, verification must fail.
- Six systems (Jolt, Nexus, Cairo-M, Ceno, Expander, Binius64) had vulnerabilities where public-claim data wasn't bound into Fiat-Shamir transcripts before challenge generation.
- This bug allows attackers to bypass cryptography and prove impossible statements, like counterexamples to Fermat's Last Theorem.
- Key terms explained: Fiat-Shamir, Transcript, Polynomial Commitment, Sumcheck, MLE, Lookup/LogUp, AIR, STARK, FRI, OODS, GKR.
- A zkVM proof claims correct program execution on public inputs with hidden execution traces, verified via algebraic constraints over committed polynomials.
- Soundness is critical: honest execution must verify (completeness), and false execution must not (soundness).
- The universal attack pattern: if a value isn't transcript-bound, challenges become independent, allowing attackers to solve for manipulated values.
- Detailed vulnerabilities in each system (Jolt, Nexus, Cairo-M, Ceno, Expander, Binius64) due to unbound values in verification equations.
- Systemic issues: academic papers omit Fiat-Shamir specifics, modular designs lead to missed bindings, optimization pressure excludes hashes, and testing misses adversarial inputs.
- Prevention: merge proof and transcript to auto-absorb values, ensuring statement data is bound before challenge sampling.
- Responsible disclosure timeline shows fixes for most systems, with one issue remaining open.
- Challenges provided to practice exploits, e.g., finding a counterexample to Fermat's Last Theorem.
- Takeaways: Fiat-Shamir bugs are widespread; auditors must trace data flow and transcript bindings; builders should treat the transcript as sacred.