Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Vellvm: Verifying Safety in the LLVM IR
Steve Zdancewic
University of Pennsylvania
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 9 October 2014
10:30
90 Minutes
E1 5
029
Saarbrücken
Abstract
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).
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).
Contact
Claudia Richter
93039103
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
112
passcode not visible
logged in users only
Claudia Richter, 10/09/2014 09:26
Claudia Richter, 10/08/2014 09:17
Claudia Richter, 10/07/2014 16:09 -- Created document.
Claudia Richter, 10/08/2014 09:17
Claudia Richter, 10/07/2014 16:09 -- Created document.