A certifying compiler for Java
(This system was implemented by Cedilla Systems Inc.)
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:
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!