Compiling with Proofs
Abstract
One of the major challenges of building software systems is to ensure that the various components fit together in a well-defined manner. This problem is exacerbated by the recent advent of software components whose origin is unknown or inherently untrusted, such as mobile code or user extensions for operating-system kernels or database servers. Such extensions are useful for implementing an efficient interaction model between a client and a server because several data exchanges between them can be saved at the cost of a single code exchange. 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 18, 1998
- Accession Number
- ADA363676
Entities
People
- George C. Necula
Organizations
- Carnegie Mellon University