1 - Introduction

Summary

An exciting development of the 21st century is that the 20th-century vision of mechanized program verification is finally becoming practical, thanks to 30 years of advances in logic, programming-language theory, proof-assistant software, decision procedures for theorem proving, and even Moore's law which gives us everyday computers powerful enough to run all this software.

We can write functional programs in ML-like languages and prove them correct in expressive higher-order logics; and we can write imperative programs in C-like languages and prove them correct in appropriately chosen program logics. We can even prove the correctness of the verification toolchain itself: the compiler, the program logic, automatic static analyzers, concurrency primitives (and their interaction with the compiler). There will be few places for bugs (or security vulnerabilities) to hide.

This book explains how to construct powerful and expressive program logics based on separation logic and Indirection Theory. It is accompanied by an open-source machine-checked formal model and soundness proof, the Verified Software Toolchain (VST), formalized in the Coq proof assistant. The VST components include the theory of separation logic for reasoning about pointer-manipulating programs; indirection theory for reasoning with “step-indexing” about first-class function pointers, recursive types, recursive functions, dynamic mutual-exclusion locks, and other higher-order programming; a Hoare logic (separation logic) with full reasoning about control-flow and data-flow of the C programming language; theories of concurrency for reasoning about programming models such as Pthreads; theories of compiler correctness for connecting to the CompCert verified C compiler; theories of symbolic execution for implementing foundationally verified static analyses.