Documentation on Certified Program Verifiers in Coq

Adam Chlipala

This is the documentation for the software related to the ICFP'06 paper Modular Development of Certified Program Verifiers with a Proof Assistant.

Organizational Outline

The software from this SourceForge project is divided up into three pieces: two generally useful libraries and the main module for the development described in the paper. The libraries are:

  • "asm", which provides OCaml code for parsing x86 binaries into abstract syntax trees and a Coq development formalizing the semantics of programs in that form
  • "accel" or "Proof Accelerator", for building a modified Coq binary that supports a mode of extraction where certain standard types like nat are extracted into more efficient native types like int
  • Prerequisites for Installation

    You'll need the following software:

  • A recent version of GCC and the associated GNU compilation toolchain, for compiling the example programs to verify
  • The Coq proof assistant, version 8.0 or later. In fact, you probably need very specifically the latest released version, since Proof Accelerator reaches into Coq's internals. Installing Debian Linux package coq is sufficient, and I recommend proofgeneral-coq for editing Coq developments in emacs. Unless you only want the asm library, you'll need the Coq source tree as well, to build Proof Accelerator. In Debian, apt-get source coq suffices to install this source tree into the current directory.
  • Objective Caml version 3.09.2 or higher, which you can obtain from Debian package ocaml.
  • OCamlMakefile, a generic Makefile for building OCaml programs. Configuration will be easiest if you install it into either /usr/include or /usr/local/include.

    I've really only tested this in Debian Linux, so things might not work elsewhere.

    Obtaining the Source Code

    The code is only available at present through this SourceForge project's CVS services. If you want to build the main certified verifiers development, you should check out all three modules (asm, accel, and proofos) via anonymous CVS, preferably in the same directory.


    In the directory where you checked out the asm CVS repository, run:


    and then


    If you installed OCamlMakefile somewhere besides one of the recommended places, pass an additional configure command-line argument OCAMLMAKEFILE=/path/to/it.

    In the directory where you checked out accel, run:

    ./configure COQSRC=/path/to/coq/source/tree

    and then


    With a non-standard OCamlMakefile location, pass the same extra argument as above. Make sure you've built Coq from source in the directory you've specified (by following the directions in the Coq source distribution) before runing make here.

    In the directory where you checked out the proofos CVS repository, run:


    and then


    Follow the same instructions as above for a non-standard OCamlMakefile location. If you haven't checked out the three CVS modules into subdirectories of the same parent directory, then you'll need to pass configure command-line arguments specifying ASMHOME and ACCELHOME.

    Testing the Installation

    The default make target for proofos should have built a number of verifiers and a number of test cases for them. To run the most basic test, try:

    VER=Vanilla make test

    It does abstract interpretation on the minimally sized example, printing a trace of the abstract states encountered in the process. For a more complicated example, try:

    VER=MemoryTypes TEST=mtlist make test

    This selects the MemoryTypes verifier described in the paper and runs it on the test case whose source is found in tests/mtlist.c.

    Building Documentation

    Most of the source files are marked up with comments for use with ocamldoc and coqdoc. To build this documentation in the doc directory of the proofos module, run this in the proofos root:

    make docs_fresh

    The current make rules need to recompile all of the .v Coq sources to get the information needed to include hyperlinks to Coq definitions in the generated HTML files. If you're not making modifications yourself, there's no need to sit through this process, since the documentation generated is the same as is presented on this web site.

    The asm Library

    The asm library is designed to be a generally useful tool for parsing machine code in both formal and informal settings. There is an OCaml library for parsing machine code into abstract syntax trees, as well as a Coq formalization of a semantics for these trees. I've also stuck some generic Coq utility code in this module.

    OCaml modules

    The OCaml source is located in asm/src/ocaml.

    Module Description
    AsmUtil Utilities related to reading binary file formats
    X86Types Representations of elements of x86 machine code
    X86Util Conversions and other utility code related to elements of x86 machine code
    X86Print Pretty-printing x86 code
    X86Parse Reading x86 binaries

    The Util Coq library

    The Coq source is located in asm/src/coq/Util.

    Module Description
    Specif New Set-level types for expressing rich specifications
    Monad Failure monad interface to some of the types from Specif
    Tactics Some useful tactics
    Mod Modular arithmetic
    Vector Vector tactics, based on CoLoR
    ListUtil Augments the List-related lemmas from the Coq standard library
    Maps The finite map code from the CompCert project, slightly expanded
    Coqlib Support code for Maps

    The Bitvector Coq library

    The Coq source is located in asm/src/coq/Bitvector.

    Module Description
    Defs Basic definitions of bitvector types and operations
    Bitwise Theorems about bitwise operations
    BArith Theorems about finite precision arithmetic
    Split Definitions and theorems about splitting bitvectors into halves
    Convert Theorems about converting between bitvectors and natural numbers
    Tactics Tactics for working with bitvectors
    Bitvector Exports all of the above modules in one namespace

    The X86 Coq library

    The Coq source is located in asm/src/coq/X86.

    Module Description
    Defs Basic definitions about x86 machine code
    Memory Helper theorems about memory access
    X86 Exports all of the above modules in one namespace

    The accel Library (Proof Accelerator)

    Some types in the Coq standard library are defined in a way that gives them convenient induction principles but makes their values hard to manipulate with time efficiency that isn't asymptotically worse than what we're used to. For instance, nats are effectively represented in unary. Other types, like Z, have optimal representations, but their naive extractions to OCaml don't take advantage of processors' native support for integers, so we end up with significant constant-factor slowdowns.

    Proof Accelerator implements a new extraction command for Coq that gives special treatment to a few of the types in the standard library. It's implemented in such a way as to make it easy to modularly add special treatment of new types.

    The accel OCaml library

    The OCaml source is located in accel/src/lib.

    Module Description
    CoqNat Support code for translation of nat to Big_int.big_int
    CoqZ Support code for translation of Z to Big_int.big_int
    CoqBvector Support code for translation of Bvector to native fixed-precision integers

    OCaml code for the new extraction commands

    This OCaml source is located in accel/src/extract. Most of it is slight modifications to extraction code distributed with Coq.

    Module Description
    Accel_common Modified version of the module from the Coq distribution
    Accel_extract_env Modified version of the module from the Coq distribution
    Accel_ocaml Modified version of the module from the Coq distribution
    Accel_ocaml_custom "Plug-ins" for special handling of particular types

    The proofos Module

    This is the main part of the repository, dealing with the construction of certified program verifiers.

    The Trusted Coq library

    This library presents the entirety of the Coq trusted computing base for certified verifiers, with the exception of the Coq standard library and the x86 formalization from asm. The Coq source is located in proofos/src/coq2/Trusted.

    Module Description
    Machine An abstract characterization of machines
    Arches Machine descriptions for particular architectures (currently just x86)
    Safety The definition of safety in terms of infinite progress

    The AbsInt Coq library

    This library implements verification by abstract interpretation. The bulk of it is functors for translating verification strategies between levels of abstraction. Its code is in proofos/src/coq2/AbsInt.

    Module Description
    Bounded Abstract interpretation of machine code programs with a fixed bound on basic block length
    Reduce Check a program for one machine by checking a compilation to another machine
    Sal Simplified Assembly Language and compilation to it from x86
    FixedCode The abstraction of an immutable code segment
    TypeSystem The Cartesian abstraction of associating types with registers
    StackTypes Retrofitting a type system to understand x86 stack and calling conventions
    SimpleCond Tracking of condition codes
    TopOnly The trivial type system deriving all its interesting parts from StackTypes
    SimpleTypes A class of simple "pointer-free" type systems
    SimpleDriver Verification driver based on SimpleTypes
    WeakUpdateTypes A class of type systems based on weak memory update
    WeakDriver Verification driver for WeakUpdateTypes-based verifiers

    The Examples Coq library

    These are the complete example verifiers, found in proofos/src/coq2/Examples.

    Module Description
    Vanilla Type-based verifier with all interesting functionality coming from StackTypes
    EvenOdd Abstract interpreter tracking parity of integers
    IntPtr Type-based verifier that understands int ref options
    MemoryTypes The verifier for linked, heap-allocated data structures described in the paper

    OCaml support code for the executable verifiers

    This OCaml source code is located in proofos/src/ver2.

    Module Description
    Ver_types Common types associated with modules in AbsInt
    Ver_fixed Code for reading metadata in a common format from executables