Efficient Proofs of Software Exploitability for Real-world Processors
Authors: Matthew Green (Johns Hopkins University), Mathias Hall-Andersen (Aarhus University), Eric Hennenfent (Trail of Bits), Gabriel Kaptchuk (Boston University), Benjamin Perez (Trail of Bits), Gijs Van Laer (Johns Hopkins University)
Volume: 2023
Issue: 1
Pages: 627–640
DOI: https://doi.org/10.56553/popets-2023-0036
Abstract: We consider the problem of proving in zero-knowledge the existence of vulnerabilities in executables compiled to run on real-world processors. We demonstrate that it is practical to prove knowledge of real exploits for real-world processor architectures without the need for source code and without limiting our consideration to narrow vulnerability classes. To achieve this, we devise a novel circuit compiler and a toolchain that produces highly optimized, non-interactive zero-knowledge proofs for programs executed on the MSP430, an ISA commonly used in embedded hardware. Our toolchain employs a highly optimized circuit compiler and a number of novel optimizations to construct efficient proofs for program binaries. To demonstrate the capability of our system, we test our toolchain by constructing proofs for challenges in the Microcorruption capture the flag exercises.
Keywords: zero-knowledge proof, NIZK, Reverie, exploits, real-world processors, MSP430, KKW
Copyright in PoPETs articles are held by their authors. This article is published under a Creative Commons Attribution 4.0 license.
