Formalizing the LLVM intermediate representation for verified program transformations

Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, Steve Zdancewic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

56 Scopus citations

Abstract

This paper presents Vellvm (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.

Original languageEnglish (US)
Title of host publicationPOPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages427-439
Number of pages13
DOIs
StatePublished - 2012
Externally publishedYes
Event39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12 - Philadelphia, PA, United States
Duration: Jan 25 2012Jan 27 2012

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'12
CountryUnited States
CityPhiladelphia, PA
Period1/25/121/27/12

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Coq
  • LLVM
  • Memory safety

Fingerprint Dive into the research topics of 'Formalizing the LLVM intermediate representation for verified program transformations'. Together they form a unique fingerprint.

Cite this