Date: February 19, 1998
Speaker: George Necula, Carnegie Mellon University
Compiling with Proofs
Abstract:
A client system can interact in a flexible and efficient manner with a server by uploading programs to be installed and executed in the server's environment. A major requirement in this scenario is to ensure that the safety of the server is not compromised, and furthermore to do this without undue burden on the server.
This talk presents a technique, called certified compilation, where the untrusted client uses a compiler to generate the mobile executable along with a formal proof of its safety. The server does not have to trust the client or its certifying compiler; it must only verify the correctness of the formal proof of safety. The certifying compiler can produce the proof automatically when the required safety properties are guaranteed by the semantics of the source language. As a proof of concept, I describe the design and implementation of the Touchstone certifying compiler for a type-safe subset of the C language, in which case the formal proof attests to the type and memory safety of the emitted machine code. For efficient proof representation and validation and to relate the proof to the optimized machine code, Touchstone uses the Proof-Carrying Code infrastructure.
In addition to generating safe mobile code, certifying compilation drastically improves the effectiveness of compiler testing because it statically signals the vast majority of compilation errors. Furthermore, the approach can be applied even in the presence of complex optimizations, as demonstrated by the fact that Touchstone generates target code that, for a realistic set of examples, is competitive with traditional optimizing C compilers. The overhead of certification in Touchstone is 25% of compilation time with proofs that are about three times larger than the machine code.
SDI / LCS Seminar Questions?
Karen Lindenfelser, 86716, or visit www.pdl.cmu.edu/SDI/