Strange Loop

Vellvm - Verifying the LLVM

LLVM is an industrial-strength compiler that's used for everything from day-to-day iOS development (in Swift) to pie-in-the-sky academic research projects. This makes the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.

This talk asks the question: what does LLVM code mean, and, how can we ensure that LLVM-based tools (compilers, optimizers, code instrumentation passes, etc.) do what they're supposed to -- especially for safety or security critical applications? The Verified LLVM project (Vellvm) is our attempt to provide an answer.

We'll look at the LLVM intermediate representation from the point of view of programming language semantics and see how Vellvm provides a basis for developing machine-checkable formal properties about LLVM IR programs and transformation passes. Along the way, we'll get a taste of what LLVM code looks like, including some of its trickier aspects, and see (at a high level) how modern interactive theorem provers--in this case, Coq--can be used to verify compiler transformations.

No experience with LLVM or formal verification technologies will be assumed.

This is joint work with many collaborators at Penn, and Vellvm is part of the NSF Expeditions project: The Science of Deep Specifications.

Steve Zdancewic

University of Pennsylvania

Dr. Zdancewic is a Full Professor and Associate Deparment chair in Computer and Information Science at the University of Pennsylvania. He received his Ph.D. in Computer Science from Cornell University in 2002, and he graduated from Carnegie Mellon University with a B.S. in Computer Science and Mathematics in 1996. He is the recipient of an NSF Graduate Research Fellowship, an Intel fellowship, an NSF CAREER award, a Sloan Fellowship. His numerous ublications in the areas of programming languages and computer security include several best paper awards. Dr. Zdancewic's research centers around using programming languages technology to help build secure and reliable software. He has worked on type-based enforcement of both information-flow and authorization policies, compiler techniques for ensure memory safety of legacy C code, and, more recently, on using interactive theorem-proving technology to construct highly-trustworthy compiler optimization passes. His interests also include type theory and linear logics.