Cheesecloth: Zero-Knowledge Proofs of Real-World Vulnerabilities

ABSTRACT

Currently, when a security analyst discovers a vulnerability in critical software system, they must navigate a dilemma: immediately disclosing the vulnerability to the public could harm the system's users; whereas disclosing the vulnerability only to the software's vendor lets the vendor disregard or deprioritize the security risk, to the detriment of unwittingly-affected users. A compelling recent line of work aims to resolve this by using Zero Knowledge (ZK) protocols that let analysts prove that they know a vulnerability in a program, without revealing the details of the vulnerability or the inputs that exploit it. In principle, this could be achieved by generic ZK techniques. In practice, ZK vulnerability proofs to date have been restricted in scope and expressibility, due to challenges related to generating proof statements that model real-world software at scale and to directly formulating violated properties. This talk presents how CHEESECLOTH, a novel proof statement compiler, proves memory bugs and leaks of information in the ZK setting. We have used CHEESECLOTH to generate ZK proofs of well-known vulnerabilities in (previous versions of) critical software, including the Heartbleed information leakage in OpenSSL and a memory vulnerability in the FFmpeg media encoding library. In addition, this talk will discuss work on proving SAT statements in ZK, which could eventually be used to secure supply chains by providing proofs of safety and correctness about private, proprietary code.

Author

James Parker is a Research Engineer at Galois with a background in programming languages and formal methods. His research spans verifying information flow control mechanisms, guaranteeing correctness of distributed systems, studying secure computation, and investigating secure development practices.

James earned his PhD in Computer Science at the University of Maryland and was advised by Dr. Mike Hicks.