Verified Software Toolchain

The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context.

Use the verifiable-c tag on stackoverflow.com for your VST-related programming/proving questions!

VST Diagram

Research results

Verifiable C tools:
Book, software, documentation

Download

Technical overview of the VST logic

Mechanized Semantic Library
for Separation Logic and Indirection Theory

Compositional CompCert

VeriSmall foundationally verified shape analysis, using VeriStar certified entailment checker

Other publications below

Program Logics for Certified Compilers
(e-book)
  (hardcover)

Participants

Andrew Appel
Andrew W. Appel

Princeton University
Lennart Beringer
Lennart Beringer

Princeton University
Gordon Stewart
Gordon Stewart

Princeton University
Josiah Dodds
Josiah Dodds

Princeton University
Qinxiang Cao
Qinxiang Cao

Princeton University
Santiago Cuellar
Santiago Cuellar

Princeton University

Collaborators, affiliated researchers, alumni

Xavier Leroy
Xavier Leroy

INRIA
Jesper Bengtson
Jesper Bengtson

ITU Copenhagen
Robert Dockins
Robert Dockins

Galois.com
Aquinas Hobor
Aquinas Hobor

National U. Singapore
Sandrine Blazy
Sandrine Blazy

U. Rennes 1

Rationale

In some application domains it is not enough to build reliable software systems, one wants proved-correct software. This is the case for safety-critical systems (where software bugs can cause injury or death) and for security-critical applications (where an attacker is deliberately searching for, and exploiting, software bugs). Since proofs are large and complex, the proof-checking must be mechanized. Machine-checked proofs of real software systems are difficult, but now should be possible, given the recent advances in the theory and engineering of mechanized proof systems applied to software verification. But there are several challenges: We address these challenges by defining Verifiable C, a program logic for the C programming language. Verifiable C is proved sound with respect to the operational semantics of CompCert C; in turn, the CompCert verified optimizing C compiler is proved correct with respect to the assembly-language semantics of the PowerPC, ARM, and x86 processors.

Publications

Compositional CompCert, by Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. POPL 2015: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, to appear, January 2015.

Verification of a Cryptographic Primitive: SHA-256, by Andrew W. Appel, August 2014.

Portable Software Fault Isolation, by Joshua A. Kroll, Gordon Stewart, and Andrew W. Appel. CSF'14: Computer Security Foundations Symposium, IEEE Press, July 2014.

Verified Compilation for Shared-memory C, by Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. 23rd European Symposium on Programming (ESOP'14), April 2014.

Program Logics for Certified Compilers, by Andrew W. Appel with Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Cambridge University Press, 2014.

Mostly Sound Type System Improves a Foundational Program Verifier, by Josiah Dodds and Andrew W. Appel. 3rd International Conference on Certified Programs and Proofs (CPP 2013), December 2013.

Verifiable C: Applying the Verified Software Toolchain to C programs, by Andrew W. Appel. 2013.

Verified Heap Theorem Prover by Paramodulation, by Gordon Stewart, Lennart Beringer, and Andrew W. Appel. In ICFP 2012: The 17th ACM SIGPLAN International Conference on Functional Programming, September 2012.

Operational Refinement for Compiler Correctness by Robert Dockins. PhD thesis, Princeton University, September 2012.

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow, by Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, Lennart Beringer, John Hatcliff, Xinming Ou and Andrew Cousino. First Conference on Principles of Security and Trust (POST 2012), March 2012.

VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: First International Conference on Certified Programs and Proofs, December 2011.

Relational Decomposition, by Lennart Beringer. Proceedings of the Second International Conference on Interactive Theorem Proving (ITP 2011), pages 39-54, August 2011. Springer LNCS 6898.

Verified Software Toolchain, by Andrew W. Appel. In ESOP 2011: 20th European Symposium on Programming, LNCS 6602, pp. 1-17, March 2011.

Relational program logics in decomposed style, by Lennart Beringer, July 2010.

Formal Verification of Coalescing Graph-Coloring Register Allocation, by Sandrine Blazy, Benoit Robillard, and Andrew W. Appel. In ESOP 2010: 19th European Symposium on Programming, March 2010.

A Theory of Indirection via Approximation, by Aquinas Hobor, Robert Dockins, and Andrew W. Appel. In POPL 2010: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2010.

Local Actions for a Curry-style Operational Semantics by Gordon Stewart and Andrew W. Appel. In PLPV'11: 5th ACM SIGPLAN Workshop on Programming Languages meets Program Verification, January 29, 2011.

A Fresh Look at Separation Algebras and Share Accounting by Robert Dockins, Aquinas Hobor, and Andrew W. Appel. To appear in Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009), December 2009.

Multimodal Separation Logic for Reasoning About Operational Semantics, by Robert Dockins, Andrew W. Appel, and Aquinas Hobor, (to appear) in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 2008.

Automating Separation Logic for Concurrent C Minor, by William Mansky. Undergraduate thesis, May 2008.

Foundational High-level Static Analysis, by Andrew W. Appel. In CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly, July 2008.

Oracle Semantics for Concurrent Separation Logic by Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. European Symposium on Programming (ESOP), April 2008. Extended version with appendix.

Separation Logic for Small-step C Minor, by Andrew W. Appel and Sandrine Blazy. in TPHOLs 2007: 20th International Conference on Theorem Proving in Higher-Order Logics, September 2007. Tactics for Separation Logic, by Andrew W. Appel, January 2006.

Parts of this research are funded by:

The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of AFOSR, NSF, DARPA, or the U.S. Government.

Early research leading to the Verified Software Toolchain was conducted in the Concurrent C minor project.

Last overhaul of this page: April 2013