Zero-knowledge Proofs of Binary Exploitability

Presented as part of the 2021 HCSS conference.

ABSTRACT

Background: We introduce the first use of zero-knowledge (ZK) proofs to prevent proprietary knowledge and techniques from leaking during software vulnerability disclosures. These proofs allow researchers to prove that they possess a software exploit in a known program binary without disclosing information about the nature of the vulnerability or the structure of its corresponding exploit. Our work builds on the techniques of Ben-Sasson et al., which demonstrate how to efficiently represent statements about program execution on Von Neumann architectures in a ZK context. Unlike previous work, ours supports real-world microprocessor architectures such as the MSP430. We also provide a ZK proof system which reduces proving time by several orders of magnitude compared to the one used by Ben-Sasson et al.

Methods: We equip vulnerability researchers with tools that allow them to unambiguously demonstrate they possess a binary exploit against a program on a real-world processor architecture, without sharing the exploit itself. Since the underlying ZK proof systems reason about statements represented as Boolean or arithmetic circuits, we develop techniques for creating circuits that accept if and only if they are provided with a valid software exploit. This is done by adapting and optimizing prior work on reducing the correctness of RAM program execution to circuit satisfiability. Our approach to representing statements about program execution as circuits eliminates a logarithmic factor present in previous work by replacing the routing network used during input validation with a pseudorandom function (PRF). This PRF requires the proof system to facilitate switching between Boolean and arithmetic circuits mid-proof. While field switching incurs some slight overhead per conversion, it is still substantially more efficient than a quasilinear reduction with large constant factors.

Prior work on ZK proofs of program execution focuses on a specific subclass of proving systems known as Succinct Non-Interactive ARguments of Knowledge (SNARKs), which require a trusted setup phase and optimize proof size and verification time at the expense of prover complexity, which is quasilinear in the circuit size. To optimize our techniques for practical software exploits, we have implemented a prover-optimized ZK proof system based on the MPC-in-the-head paradigm of Ishai et al. This system produces larger proofs than SNARKs, but its prover runtime is several orders of magnitude faster and supports proof streaming so that the verifier never needs to load the entire proof into memory. For example, libSNARK takes roughly 23 minutes to compute 511 iterations of the SHA256 hash function, whereas our proof system only takes 23 seconds. Due to the asymptotically worse prover complexity of SNARKs, this performance gap becomes untenable for circuit sizes relevant to vulnerability disclosure.

Results: We focus on practical software exploits by demonstrating that our tools can be used to prove knowledge of solutions to the Microcorruption CTF, a series of binary exploit challenges that involve breaking into a smart lock controlled by an MSP430 processor. Microcorruption covers many common binary exploits such as stack and heap overflows, bypassing memory protections such as ASLR, and the use of return-oriented programming (ROP) gadgets. To validate our techniques we have developed an efficient RAM reduction for MSP430 programs and ported the challenge set into our framework.

Since both prover time and proof size scale linearly with the size of the execution trace, performance depends exclusively on the processor circuit size and the number of instructions required to trigger the exploit. For a simple stack-based buffer overflow bug with a trace length of 1k instructions, we were able to generate an 85MB proof in 30 seconds on a Digital Ocean machine with 8 cores and 64 GB of RAM. When running more complex heap vulnerabilities with a trace length of 12k instructions, our system produced 1.1GB proofs in roughly 6 minutes.

Acknowledgement: This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA). The views, opinions and/or findings expressed are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

Ben Perez is a senior security engineer at Trail of Bits. He brings expertise in formal methods and applied cryptography to his work on blockchain security tools, cryptography research, and software assessments. He holds a BA in mathematics from St. Olaf College (2014) and an MS in computer science from the University of California, San Diego (2018), where his master's thesis focused on computationally efficient dimension reduction algorithms.