This is the documentation for the software related to the ICFP'06 paper Modular Development of Certified Program Verifiers with a Proof Assistant.
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:
You'll need the following software:
I've really only tested this in Debian Linux, so things might not work elsewhere.
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:
./configure
and then
make
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
make
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:
./configure
and then
make
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.
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.
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 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.
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 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 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 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 |
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 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 |
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 |
This is the main part of the repository, dealing with the construction of certified program verifiers.
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 |
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 |
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 |
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 |