Computer Science Department
School of Computer Science, Carnegie Mellon University
Compiling with Proofs
George Ciprian Necula
In this dissertation, I propose to tackle such system integrity and security problems with techniques from mathematical logic and programming-language semantics. I propose a framework, called proof-carrying code, in which the extension provider sends along with the extension code a representation of a formal proof that the code meets certain safety and correctness requirements. Then, the code receiver can ensure the safety of executing the extension by validating the attached proof. The major advantages of proof-carrying code are that it requires a simple trusted infrastructure and that it does not impose run-time penalties for the purpose of ensuring safety.
In addition to the concept of proof-carrying code, this dissertation contributes the idea of certifying compilation. A certifying compiler emits, in addition to optimized target code, function specifications and loop invariants that enable a theorem-proving agent to prove non-trivial properties of the target code, such as type safety. Such a certifying compiler, along with a proof-generating theorem prover, is not only a convenient producer of proof-carrying code but also a powerful software-engineering tool. The certifier also acts as an effective referee for the correctness of each compilation, thus simplifying considerably compiler testing and maintenance.
A complete system for proof-carrying code must also contain a proof-generating theorem prover for the purpose of producing the attached proofs of safety. This dissertation shows how standard decision procedures can be adapted so that they can produce detailed proofs of the proved predicates and also how these proofs can be encoded compactly and checked efficiently. Just like for the certifying compiler, a proof-generating theorem prover has significant software-engineering advantages over a traditional prover. In this case, a simple proof checker can ensure the soundness of each successful proving task and indirectly assist in testing and maintenance of the theorem prover.