Vellvm: Verifying the LLVM

The Vellvm project is building a (verified LLVM), a framework for reasoning about programs expressed in LLVM's intermediate representation and transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM's intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate different reasoning styles and proof techniques.

To validate Vellvm's design, we extract an interpreter from the Coq formal semantics that can execute programs from LLVM test suite and thus be compared against LLVM reference implementations. To demonstrate Vellvm's practicality, we formalize and verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm's tools allow us to extract a new, verified implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance is competitive with the non-verified, ad-hoc original.

Vellvm is a part of the DeepSpec NSF Expedition.

Current Participants

• Steve Zdancewic (PI)
• Yannick Zakowski (Post Doc)
• Calvin Beck (Ph.D. student)

Past Participants

• Christine Rizkallah (Post Doc)
• Dmitri Garbuzov (Ph.D. student)
• Richard Zhang (Ph.D. student)
• Joel McCarthy (Masters student)
• William Mansky (Post Doc)
• Vivien Durey (MSE student, graduated)
• Milo M. K. Martin (Co-PI) (now at Google)
• Jianzhou Zhao (Ph.D. student, graduated)
• Santosh Nagarakatte (Ph.D. student, graduated)

Code

• The "original" Vellvm development code base (called Vellvm-legacy) has been moved to a GitHub repository, available here https://github.com/vellvm

Publications

• Verifying Dynamic Race Detection [ CPP 2017 ]
• An Axiomatic Specification for Sequential Memory Models [ CAV 2015 ]
• A Formal C Memory Model Supporting Integer-Pointer Casts [ PLDI 2015 ]
• WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking [ CGO 2014 ]
• Hardware-enforced Comprehensive Memory Safety [IEEE Micro Top Picks 2013]
• Ironclad C++: A Library-Augmented Type-Safe Subset of C++ [OOPSLA 2013]
• Formalizing an SSA-based Compiler for Verified Advanced Program Transformations [Jianzhou Zhao's Ph.D. dissertation, 2013]
• Formal Verification of SSA-Based Optimizations for LLVM [PLDI 2013]
• Formalizing the LLVM Intermediate Representation for Verified Program Transformations [POPL 2012]
• Mechanized Verification of Computing Dominators for Formalizing Compilers [CPP 2012]
  • cpp12.tgz
  • README-dom

Funding:

• NSF Grant 1521539 Collaborative Research: Expeditions in Computing: The Science of Deep Specification
• NSF Grant XPS 1337174 CLCCA: Improving Parallel Program Reliability Through Novel Approaches to Precise Dynamic Data Race Detection
• Supported by NSF Grant 1065166: Validating Program Transformations in a Mechanized LLVM