The Low-Level Virtual Machine (LLVM) compiler provides a modern, industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target
platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses, making it an ideal target for enforcing security properties of
low-level code.
In this talk, I will describe the Vellvm project, which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of
the subtleties of modeling the LLVM IR semantics, including nondeterminism and its use of SSA representation. I'll also describe some of the proof techniques that we have used for reasoning about
LLVM IR transformations and describe our results about the formal verification of the SoftBound pass, which hardens C programs against memory safety errors.
Vellvm, which is implemented in the Coq theorem prover, provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler, thus enabling us to create verified
optimization passes for LLVM and evaluate them against their unverified counterparts. Our experimental results show that fully verified and automatically extracted implementations can yield
competitive performance.
This is joint work with Jianzhou Zhao and Milo Martin (both at Penn) and Santosh Nagarakatte (at Rutgers University).