Zero-Knowledge Proofs in Vulnerability Disclosure

One research team led by Galois, Inc., has demonstrated a ZKP for a previously known memory-safety vulnerability in the Game Boy Advance (GBA) Raster Image Transmogrifier, known as grit. Memory-safety vulnerabilities are a critical class of vulnerabilities that frequently occur in modern software. In the Galois-led demonstration, a vulnerability researcher was able to interactively convince another party of the existence of the specific vulnerability in around eight minutes.

To achieve this milestone, researchers developed techniques and prototypes that implement a combination of novel program analyses and protocols for proving and evaluating statements in zero knowledge. Specifically, the team was able to develop a way to compactly mathematically represent memory-safety vulnerabilities, and then create a zero-knowledge proof based on that representation.

Although the current prototype can only produce proofs for programs that use a restricted set of language features, the Galois team aims to extend its capabilities to prove vulnerabilities of any C/C++ program that can be compiled using a standard compiler. They are also actively researching prototypes that offer ZKPs of more complex claims, such as a program’s overall memory safety.

A second team of researchers from Trail of Bits is working to model vulnerabilities at the systems architectural level, which is a lower level of abstraction than Galois is working on. Their initial work has created a way to represent real-world instruction set architectures as Boolean circuits – or mathematical models of digital logic circuits – compatible with ZKPs so that users can demonstrate their ability to force a public binary into a specific malicious state. The team’s initial work targets the MSP430 microcontroller, a microprocessor commonly used in embedded systems. From there, they discovered a way to mathematically represent a variety of common vulnerabilities so that ZKPs could be developed to prove the existence of those vulnerabilities. The ZKP statement sizes ranged from 86MB to 1.1 GB, and took from 23 seconds to 256 seconds to verify on a desktop PC.

As an example, the team was able to prove that a smart lock using the MSP430 microcontroller could be opened via an undisclosed exploit without having to share details about the exploit or vulnerability.

“Essentially, the researchers took a smart lock, locked it, and then threw away the key. They were then able to exploit the underlying MSP430 to unlock it, and developed a zero-knowledge proof of the exploit to show that it could be done without having to share how it was done,” explained Baron.

Trail of Bits has so far demonstrated the ability to perform ZKP disclosure for a wide variety of common types of vulnerabilities in MSP430 binaries, including stack and heap overflows, code injection, format string vulnerabilities, and bypassing memory protections, such as Data Execution Prevention (DEP) and Address Space Layout Randomization (ASLR).

The team is now working to expand the list of supported architectures and runtime environments, with the goal of capturing much of the common x86 architecture. For example, they plan to produce ZKPs of binaries from DARPA’s 2016 Cyber Grand Challenge, which run on DECREE – a simple operating system built on x86. In this way, SIEVE is building on over a decade of DARPA research in how to formalize cybersecurity.