Vellvm: Formal Verification of LLVM IR Code
By. Dr. Steve Zdancewic
Abstract
LLVM is an industrial-strength compiler that's used for everything from iOS development to academic research. However, like any piece of complicated software, LLVM IR itself has a complex specification, making it hard to fully understand, and its implementation has bugs, which can cause potentially catastrophic mis-compilation errors. These properties make the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.
This talk will survey the Vellvm (Verified LLVM) project, which aims to define a formal, mathematical specification for a large, useful subset of LLVM. Vellvm is implemented in the Rocq interactive theorem prover, which can be used for developing machine-checkable properties about LLVM IR programs and compiler optimization passes. Along the way, we'll explore some subtleties of LLVM IR semantics and see how Vellvm models them in a modular way by composing "monadic interpreters" built on top of a data structure called _interaction trees_. We'll also see some applications of Vellvm for verified compiler construction.
Bio
Dr. Zdancewic is the Schlein Family President's Distinguished Professor in the Computer and Information Science Department 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, and a Sloan Fellowship. His numerous publications in the areas of programming languages and computer security include several best paper awards.
More information
Recording
Abstract
LLVM is an industrial-strength compiler that's used for everything from iOS development to academic research. However, like any piece of complicated software, LLVM IR itself has a complex specification, making it hard to fully understand, and its implementation has bugs, which can cause potentially catastrophic mis-compilation errors. These properties make the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.
This talk will survey the Vellvm (Verified LLVM) project, which aims to define a formal, mathematical specification for a large, useful subset of LLVM. Vellvm is implemented in the Rocq interactive theorem prover, which can be used for developing machine-checkable properties about LLVM IR programs and compiler optimization passes. Along the way, we'll explore some subtleties of LLVM IR semantics and see how Vellvm models them in a modular way by composing "monadic interpreters" built on top of a data structure called _interaction trees_. We'll also see some applications of Vellvm for verified compiler construction.
Bio
Dr. Zdancewic is the Schlein Family President's Distinguished Professor in the Computer and Information Science Department 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, and a Sloan Fellowship. His numerous publications in the areas of programming languages and computer security include several best paper awards.
More information
Recording
Practical information
- General public
- Free
Contact
- Host: Prof. Nate Foster