  Currently, when a security analyst discovers a vulnerability in critical
software system, they must navigate a fraught 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 paper presents CHEESECLOTH, a
novel proofstatement compiler, which proves practical vulnerabilities in ZK by
soundly-but-aggressively preprocessing programs on public inputs, selectively
revealing information about executed control segments, and formalizing
information leakage using a novel storage-labeling scheme. CHEESECLOTH's
practicality is demonstrated by generating 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 graphics framework.
