Zero knowledge vulnerability disclosure trail of bits

The proposal (May 2020)

On 21 May 2020 Ben Perez of Trail of Bits published a proposal to change how software vulnerabilities are disclosed. A researcher would hand a vendor or bug-bounty program a zero-knowledge proof that they hold a working exploit, without handing over the exploit itself (Trail of Bits, 2020).

The problem it targets is a trust deadlock. A researcher who discloses too much can lose the reward. The post puts it this way: "Disclosing too much information about a vulnerability could ruin the reward for a third-party researcher." On the other side, a program cannot pay for a claim it has no way to check. A ZK proof of exploitability would let the program check the claim against a scope it defined, while the researcher keeps the details private.

The work was planned as a four-year effort with Matthew Green at Johns Hopkins University. It was funded by DARPA's SIEVE program (Securing Information for Encrypted Verification and Evaluation) (Trail of Bits, 2020).

The mechanism as proposed

The statement to prove is about a public binary. The post says the team wants "a circuit that accepts if the prover has some input to a program that leads to an exploit." The design follows the "SNARKs for C" approach and splits the check into two parts:

Instruction-by-instruction validity. A circuit models the processor and checks each step of an execution trace.
Memory consistency. The prover also supplies the trace sorted by memory address. A "permutation checker" circuit proves that this sorted trace is a permutation of the original (Trail of Bits, 2020).

The post names three obstacles:

Cost. With a naive design, circuit size grows linearly with both trace length and RAM size.
Scope of the processor model. Modelling all of x86 is impractical, so only the instructions a given binary actually uses would be modelled.
Loops. Data-dependent loops such as repz cannot be expressed directly in a combinatorial circuit. A static binary translator was planned to handle them.

The first target was the MSP430 microcontroller, because "the MSP430 is also the system the Microcorruption CTF runs on." The plan was to move to x86 afterwards (Trail of Bits, 2020).

Year one: the DARPA demonstrations (April 2021)

On 22 April 2021, about one year into SIEVE, DARPA reported results from two teams (DARPA, 2021).

Trail of Bits represented real instruction-set architectures as Boolean circuits. Results reported by DARPA:

ZK disclosure was demonstrated for stack and heap overflows, code injection, format-string bugs, and DEP and ASLR bypasses in MSP430 binaries.
Proof statements ranged from 86 MB to 1.1 GB.
Verification took 23 to 256 seconds on a desktop PC.
The team proved that an MSP430-based smart lock could be opened using an undisclosed exploit.
The next stated goal was binaries from DARPA's 2016 Cyber Grand Challenge, which run on the x86-based DECREE operating system.

Galois led the other team. It proved a known memory-safety vulnerability in the GBA Raster Image Transmogrifier (grit) and convinced a verifier in about eight minutes. Its prototype handled only a restricted set of C language features (DARPA, 2021).

The peer-reviewed result: PoPETs 2023

The MSP430 work was published as "Efficient Proofs of Software Exploitability for Real-world Processors." The authors are Green, Hall-Andersen, Hennenfent, Kaptchuk, Perez and Van Laer. It appeared on ePrint 2022/1223 on 15 September 2022 and in PoPETs 2023(1), pp. 627–640 (ePrint; PoPETs).

The paper's concrete choices (PoPETs PDF):

Proof system. The paper uses KKW (Katz–Kolesnikov–Wang) MPC-in-the-head, not a SNARK. The authors released Reverie, which they describe as the first publicly available general-use implementation of KKW.
- Reverie adds ring switching between Boolean and arithmetic representations.
- It proves 511 iterations of SHA-256 in 8 seconds. In the paper's comparison table, libsnark takes 1,387 s, Bulletproofs 2,555 s and Ligero 400 s for the same work.
- The trade-off is proof size: proofs grow linearly rather than staying succinct.
Statement. Every Microcorruption challenge ends in an UNLOCK syscall. The circuit checks that the witness trace is valid and that at least one step of execution was a call to UNLOCK.
Throughput. The toolchain proves 216 MSP430 instructions per second at about 119 KB of proof per instruction. Each instruction costs 10,691 AND gates. Benchmarks ran on a 32-vCPU, 256 GB machine.

Example benchmarks:

Challenge	Exploit type	Cycles	Prover	Verifier	Proof size
New Orleans	Password embedded in binary	2,392	22 s	7 s	295 MB
Addis Ababa	Format-string bug	5,360	23 s	17 s	296 MB
Vladivostok	ASLR bypass	50,823	454 s	152 s	6,048 MB

Stated limits.
- Only exploits that can be written as a predicate over processor states are in scope. Microarchitectural attacks (Spectre, Meltdown) and Row Hammer cannot be expressed this way.
- Choosing the right predicate is hard for researchers without ZK expertise. The authors call making this easier "important future work."

Trail of Bits also published the tooling for the x86 follow-on:

Circuitous ("binary->LLVM->circuits") builds circuits tailored to a binary. It currently supports "only a subset of x86 (both 32-bit and 64-bit)."
sholva is an experimental Tiny86 decoder and verifier for SIEVE.

Neither of these, nor Reverie, is archived. None has had commits pushed since 2024: Reverie since September 2023, Circuitous since February 2024, sholva since May 2024.

A parallel line of work came from Galois-affiliated authors. Cheesecloth (arXiv 2301.01321, 3 January 2023) is a proof-statement compiler. It produced ZK proofs of the Heartbleed information leak in OpenSSL and of a memory vulnerability in FFmpeg, both in older versions of those projects (arXiv).

Where it stands (October 2026)

The 2020 claim that proving exploitability is practical has been demonstrated. That holds for MSP430 CTF binaries and for selected C programs such as OpenSSL and FFmpeg. It has not been shown at x86 production scale in any primary reviewed here. The x86 tooling is public but has been quiet since 2024. No paper reporting proofs for Cyber Grand Challenge binaries turned up in this research.

The disclosure process the proposal aimed to change still runs the old way, including in ZK infrastructure itself. RISC Zero's and Succinct's 2025–2026 advisories credit reports made through conventional bug-bounty platforms: HackenProof (GHSA-g3qg-6746-3mg9), Immunefi (GHSA-p7v2-jjv3-8p8f) and Code4rena (GHSA-63x8-x938-vx33). The ZK-proof workflow played no part in them. Those advisories are covered in our zkVM security piece.

For teams that run bounty programs or ship circuits, the primaries point to three open problems:

Precise scope. The bounty must state the bad state precisely, as Microcorruption does with UNLOCK. The paper names this as the main barrier to use.
Proof size. Proofs run from hundreds of megabytes to gigabytes.
Unprovable bug classes. Hardware and microarchitectural bugs fall outside what the system can prove.

Timeline

2020-05-21: Trail of Bits proposal; DARPA SIEVE, with Johns Hopkins.
2021-04-22: DARPA reports Trail of Bits MSP430 and Galois grit demonstrations.
2022-09-15: ePrint 2022/1223 posted.
2023-01-03: Cheesecloth on arXiv.
2023: PoPETs 2023(1) publication.
2023-09 / 2024-02 / 2024-05: Last pushes to Reverie, Circuitous and sholva.