Certifying, Optimizing Compilation

Abstract

In practice it is well-known that it is usually easier to check a proof than to generate one. Together with George Necula, I have made use of this idea to develop a mechanism that allows a host computer system to safely execute programs that are provided by an untrusted source. There are many examples of systems where a desire such a capability arises, including extensible operating systems, web servers, and run-time systems. In our approach, called Proof-Carrying Code, or simply PCC, the designer of the host system first makes a formal definition of a safety policy. Then, a programmer who wants to execute a program on the host system must provide the program in a special form that contains, addition to the native code, a formal proof of that the code adheres to the safety policy. The host can easily validate the proof using standard proof-checking techniques. If the validation succeeds, the code is guaranteed to respect the safety policy.

There are many benefits of PCC. Since the approach is based on a static verification of the program’s safety, once validated, the program can be executed without relying on run-time checks. Hence it can be executed without expensive modification or interpretation. This guarantee holds even if the proof or native code are tampered with. Also, PCC can provide an important form of system security without using cryptography and without consulting any external trusted entities. Finally, safety is provided by a relatively small and simple proof-checking program, thereby enhancing the trustworthiness of the entire system.

While there is a significant engineering benefit to reducing the problem of code verification to a much simpler proof-checking process, this puts the application writer in the rather uncomfortable position of being obligated to generate formal proofs of programs. In order to automate this process for an important class of safety policies, we have developed and implemented the concept of a Certifying Compiler. A certifying compiler automatically generates the proof along with the target code from a given source program. The main complication in the construction of a certifying compiler is in the static program analyses; each analysis must provide enough information so that generating the proofs for the subsequently optimized code will always succeed.

This lecture describes the concepts of Proof-Carrying Code and Certifying Compilation, and gives a detailed overview of Touchstone, a certifying compiler for a safe subset of C. Particular attention will be paid to the reformulation of the program analyses, and how these affect the overall structure of the compiler.