Researchers Demonstrate Potential for Zero-Knowledge Proofs in Vulnerability Disclosure

Today, the disclosure process for software vulnerabilities is fraught with challenges. Cybersecurity researchers and software security analysts are faced with an ethics versus efficacy dilemma when it comes to reporting or sharing discovered bugs. Revealing a vulnerability publicly may get the attention of the program’s developers and motivate a timely response, but it could also result in a lawsuit against the researcher. Further, public disclosure could enable bad actors to exploit the discovery before a patch or fix can be applied. Sharing the vulnerability directly with the software maker on the other hand is ethically sound, but may not necessarily prompt action. As history has shown, software makers are often reluctant or unwilling to engage with outside security teams and the disclosed vulnerabilities are frequently ignored, or corrective action is dangerously delayed.

DARPA’s Securing Information for Encrypted Verification and Evaluation (SIEVE) program is exploring potential solutions to this problem through the use of zero-knowledge proofs (ZKPs). ZKPs are mathematically verifiable problem statements that can be used to reason about software or systems. The proofs can be used publicly without giving away sensitive information. SIEVE is focused on developing computer science theory and software capable of increasing the expressivity of problem statements for which ZKPs are constructed while also making it easier to use the cryptographic method.

“Prior to SIEVE, one primary focus of applying ZKP research had been on maximizing the speed of communicating and verifying proofs – sometimes called ‘succinct zero-knowledge’,” said Josh Baron, the program manager leading SIEVE. “For applications like cryptocurrency and blockchain transactions, prioritizing communication and verification efficiency is essential. However, for many potential defense applications, including for highly complex proof statements like those that the Department of Defense may wish to employ, achieving total efficiency and optimization across all metrics may be needed.”

In the case of vulnerability disclosure, ZKPs could allow a vulnerability researcher (the prover) to convince a software maker (the verifier) that they possess a piece of information – such as a bug or an exploit – without revealing so much information that their potential for a reward is ruined or requiring that they divulge how the information was uncovered. One year into the SIEVE program, two research teams have demonstrated the first-ever capability to mathematically prove the exploitability of vulnerable software without revealing critical details around the vulnerability itself or the exploit.

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.

# # #

Media with inquiries should contact DARPA Public Affairs at outreach@darpa.mil

Associated images posted on www.darpa.mil and video posted at www.youtube.com/darpatv may be reused according to the terms of the DARPA User Agreement, available here: http://go.usa.gov/cuTXR.

Tweet @darpa