Proof-Carrying Code

The Touchstone Certifying Compiler

Oct 1998 Release

Contents

See also: the Touchstone compiler page, the Proof-Carrying Code page, George Necula's home page, and the Touchstone online demo (more pointers are listed below).

Dependencies

This release of Touchstone works only on Alphas running Digital Unix V3.2 or V4.0. In addition to software that comes with Digital Unix (such as the assembler and linker), you'll need the following: GNU make, gcc, perl5 (installed as /usr/local/bin/perl5), m4, and SML/NJ version 110.

Using Touchstone

First, you need to download and unpack the Touchstone sources. These can be found at ftp.cs.cmu.edu. We'll use $ROOT to refer to the top-level Touchstone directory (containing subdirs pcc, cc, and prover).

Set the following environment variables (CCOMP and PCC should be absolute paths):

Before you can use Touchstone for the first time, you have to run GNU make in $ROOT/pcc. This builds the programs engine and transl_elf and puts them in $ROOT/pcc/Bin.

Touchstone includes a driver program that knows all the steps necessary to compile a Touchstone C program into proof-carrying code. This driver is the ML function Main.compile. Each time you want to use Touchstone, you need to:

Important Directories

Here's a short description of some of the important directories in this release:

pcc/cc/src
ML source for an optimizing, certifying compiler for a type-safe subset of C
pcc/prover/src
ML source for a theorem prover
pcc/pcc/Src
C source for:
transl_elf
translates a fully explicit Elf signature into a binary (represented as Alpha assembler input).
engine
Both the VCGen and proof checker for Touchstone. Works with the binary for predicates and proofs, stored in COFF files.
pcc/pcc/Exper/LF
LF logic and axioms for Touchstone's safety policy.
pcc/cc/test
Test code and benchmarks (*.cc) written in Touchstone C. A few of the Touchstone programs include C driver programs (named *.main.c). The Touchstone compiler's log file is stored here (out).
cc/pccout
Temporary files and output produced by Main.compile go here.
pcc/Bin
Contains perl scripts and binaries used during Main.compile.

References


This work was sponsored in part by the Advanced Research Projects Agency CSTO under the title "The Fox Project: Advanced Languages for Systems Software," ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050.

Maintained by:

David.Swasey@cs.cmu.edu
(last updated Thu Mar 18 10:13:05 EST 1999 )