Zero Knowledge at DARPA
Defense Advanced Research Projects Agency (DARPA) is a research and development agency of the United States Department of Defense(DoD).
Cryptographic Programs at DARPA
Proceed - Computation on encrypted data (Completed)
Fully Homomorphic Encryption, MPC SAFER - Safe, resilient communications over the Internet (Completed)
Pluggable Transports, Decoy Routing, Three-Party MPC Brandeis - Build privacy-aware systems (~ Completed)
MPC, Differential privacy, human factors SAFEWARE - Provably-secure software obfuscation (Completed)
Indistinguishability Obfuscation RACE - Secure, distributed messaging in contested network environments (Ongoing)
MPC, Obfuscated Communications SIEVE - Zero knowledge proofs for DoD applications (Ongoing)
Translate DoD-relevant problems into NP, ZK for large circuits Cooperative Secure Learning - Privacy-preserving machine learning (Ongoing)
FHE, MPC, Differential privacy DPRIVE- HW accelerator for FHE (Ongoing)
MTO program
Securing Information for Encrypted Verification and Evaluation (SIEVE)
Develop computer science theory and software to create mathematically verifiable public statements derived from hidden, sensitive information in order to publically yet securely communicate about DoD capabilities. Enable verification while keeping secrets
How it's done today and why it matters to DoD
Currently, sensitive information must be revealed in order to prove assertions in the real world. SIEVE will enable a fundamental change in capability in three key areas:
Statements about software Prove that a system is vulnerable without ever revealing the vulnerability/exploit Statements about computation (Algorithm) Proving data provenance without ever revealing its source or how it was processed (Inputs) Prove that a machine learning classifier was created following appropriate regulations without ever revealing any of the training data Statements about socio-technical interactions Prove that the North Koreans have exploited a particular system without ever revealing USG intelligence on North Korean capabilities
Challenge: Efficient ZK Proofs for Complex Problem Statements
Note: not interested in Succinctness in DARPA, really cares about what can describe that would be amenable to a zero knowledge proof.
SIEVE Program Vision
Proof of Exploit in MSP430 microcontroller (Binary) (ZKPoE)
Demonstration built on microcorruption CTF challenge. Proved that team could unlock a smart lock without showing how.
Demonstrated the protected disclosure for a wide variety of common vulnerabilities binaries, including stack and heap overflows, code injection, format string vulnerabil bypassing memory protections such as DEP and ASLR. Exploits taken from http://microcorruption.com/ For more on approach, see https://blog.trailofbits.com/2020/05/21/reinventing-vulnerabilitydisclosure-using-zero-knowledge-proofs/
Proof of Exploit in C Code (Source)
Vulnerable program: Image file converter in GameBoy Advance 11 k lines of C++ code Vulnerability: Buffer overflow (memory misallocation) Demonstrate the vulnerability: Concrete simulation of program (LLVM), identifying illegal memory access as it occurs Prove it in Zero Knowledge: Prover proves she ran a consistent execution of program... With this specific input... Resulting in this specific error condition...... Without revealing the input used or anything about program flow Protocol Statistics: 57M multiplications, 9GB memory, 9 minutes to prove, 8 minutes to verify Implications of the proof: A correct compiler C/C++ can legally compile the program to a binary that, given the input, could do anything (including executing attacker-provided code)
Exploring Potential Uses of ZKP in Legal Settings
Challenges:
Explain the basic idea to a legal audience (highly sophisticated but non-technical): Tie down (or at least expose) loose ends: What is the public input? the witness? the statement? Who decides? How to connect the bits to the real world? To the ground truth? Need to encode complex decision processes ahead of time, cover all cases Single Prover vs. Many Provers (witness split across parties) Who would initiate the use of ZK? Who would vet it? (the parties? The court?) Promise:
Make law more efficient Allow for greater privacy and greater accountability Allow for new & nimble (expressive, precise) legal tradeoffs between verification and exposure New legal landscape: Co-design of law and technology New legal landscape: Co-design of law and technology
For more, see: "Verification Dilemmas, Law, and the Promise of Zero-Knowledge Proofs" Kenneth Bamberger, Ran Canetti, Shafi Goldwasser, Rebecca Wexler, Evan Zimmerman (To appear in Berkeley Technology Law Journal, Vol. 37, No. 1, 2022)
High Performance ZK proofs
Stealth: Wolverine (S&P'21, https://eprint.iacr.org/2020/925)
Using 5 threads, 400MBof memory, and a 200 Mbps network Communication: 9 bits/gate (Boolean), 2-4 field elements/gate (arithmetic) Computation: gate in the Boolean case, and gate for an arithmetic circuit over a 61 -bit field. (basically hitting phase 2 metrics) Live demo at PI meeting (wolverine) 54 million gates 23 seconds. Stealth: Trillion gate ZK proof via a variant of Quicksilver (CCS'21, https://eprint.iacr.org/2021/076)
Ran Wolverine algorithm on SHA computations using a c5.4xlarge AWS instance 1T AND gates, 4.1T XOR gates, 98B NOT gates Communication: ~1.12TB (50Mbps network connectivity) Computation: 67 ns per AND gate 18.6 hours total computation time Galois: Mac'N'Cheese (https://eprint.iacr.org/2020/1410)
For a disjunctions of (sub)circuits, sends total communication proportional to only the biggest subcircuit. ~1 billion gate circuit in 1 hour total time, 200MB total memory, 48GB communicated the point here is the tiny amount of memory
High-Assurance ZK proofs
SRI: First-ever formally verified ZK proof software pipeline (https://arxiv.org/abs/2104.05516) Synthesized a formally verified implementation of an MPC-in-the-head ZK proof system from a formalization in the Easycrypt proof assistant. Outputs implementation in OCaml code
Major Theoretical Results (TA3) + Some other fun results
Instantiating Fiat Shamir via LWE Bounded depth circuits, GKR (STOC'21, https://eprint.iacr.org/2020/980) Parallel repetition of "commit and open" (e.g., GMW, IKOS) (STOC'21 https://eprint.iacr.org/2021/286.pdf) First-ever quantum proof of knowledge using only classical communication, verifier, quantum prover. (EUROCRYPT'21, https://arxiv.org/abs/2005.01691) Previous ZK results were not proofs of knowledge Encryption and the Law Protecting Cryptography Against Compelled Self-Incrimination (USENIX'21, https:///eprint.iacr.org/2020/862.pdf) Abuse Resistant Law Enforcement Access Systems (EUROCRYPT'21,https://eprint.iacr.org/2021/321)
SIEVE Metrics
