Touchstone

A certifying compiler for Java

(This system was implemented by Cedilla Systems Inc.)

Contents

Overview

Touchstone is a certifying compiler for Java for Intel x86. The main diffence from a standard compiler is that it also produces a formal proof that the resulting machine code is type-safe and memory safe. This is possible because, once the source program passed the type checker, the type safety property is established, and all the compiler has to do is to preserve the safety proof.

The compilation process is described in the figure below. (The rectangular boxes symbolize processes and the wavy boxes programs and data that is manipulated. The green elements are trusted, while the orange ones are not.) The following steps are involved:

  1. The source program is compiled to machine code annotated with loop invariants and with some other annotations.
  2. The annotated machine code is passed through the Verification Condition Generator (VCGen) that verifies the well-formedness of the code (such as that the branch targets are within the code segment) and emits a verification condition (VC). The verification condition is a predicate that is provable only if the code meets the safety policy.
  3. The verification condition is passed to a theorem prover that finds and emits a proof of it according to the logic requested by the code consumer.
  4. The proof is verified to be valid (with respect to the given logic) and to prove the required verification condition.
  5. If the proof checking succeeds, the code meets the safety policy and can be safely installed for execution.

The framework for representing the logic, the verification condition and its proof, along with the efficient algorithms for generating verification conditions and for checking proofs constitute the Proof-Carrying Code (PCC) infrastructure. PCC is also interesting on its own because it can be used for safe execution of mobile code. Its key advantages over competing techniques is that even complex safety policies can be enforced without performance penalty and while using a small trusted computing infrastructure. Static checking is the reason this combination is possible; the proof constitutes easily-checkable evidence to the safety of the code, so that static checking is simple. See my PCC page for further information.

I have put together a demonstration of the certifying compiler and PCC. You can compile and verify the safety of some of our own examples, or you can upload and compile your own source. Enjoy!

Author: George Necula (necula@cs.berkeley.edu). Last revised: February 21, 2001 10:45 AM.