The Fox Project
|
| Contents | Recent Talks | Recent Publications | Software | Collaborations | Further Links |
|---|---|
| Elsewhere | Bibliography |
Proof-Carrying Code (PCC) is a technique by which a host computer system can verify automatically that code provided by an untrusted agent is safe to execute.
The most obvious applications of PCC involve safe, high-performance, mobile code. However, PCC's significance in computer systems design goes well beyond mobile-code applications. PCC allows a measure of trust to be established between any parties that want to share executable content. Furthermore, PCC places few restrictions on the form of the code or the way in which it is produced. This means that the code can even be in highly optimized native form, thereby allowing extremely high performance. Finally, PCC eliminates the need for complex and potentially bug-prone components such as just-in-time compilers and bytecode verifiers from the trusted computing base, thereby increasing the level of assurance in the system as a whole.
The key idea behind PCC is to require the code producer to produce easy-to-check evidence that "explains" why the code is safe and then to attach this evidence to the code itself. Then, when the code consumer receives the code, the evidence can be extracted and easily validated.
The theoretical foundation for all of our current implementations of PCC is the notion of a formal proof of program safety. By precisely specifying the formal operational semantics of the programming language (which is typically a native machine code language) and a set of proof rules for proving the safety of every machine instruction, we are able to obtain checkable encodings of safety proofs. The encoding of the safety proofs is designed (using a logical framework language) so that the existence of the proof implies, absolutely, that the code meets all safety requirements. Precise details of the proof encoding are determined by engineering considerations, with the overall goal being the simple and fast validation of code binaries.
To produce PCC proofs automatically, certifying compilers are used. Often, certifying compilers are based on typed intermediate languages. This allows programmers to write programs in a typed high-level language such as ML or Java, and then compile these source programs into highly optimized PCC binaries automatically. In addition to handling languages such as ML and Java, the project also investigates new designs for safe languages.
The original implementation of a certifying compiler for proof-carrying code was developed by George Necula for his doctoral dissertation. This system, called Touchstone, is available via anonymous ftp.
More recently, Touchstone has been updated with software developed by Cedilla Systems Incorporated so that it compiles Java. More information about this version of Touchstone, along with an on-line demonstration, is available on George Necula's web site.
Currently we collaborate directly on proof-carrying code research with George Necula (Berkeley) and with the development team at Cedilla Systems Incorporated.
One of the main emphases of this collaboration has been the development of a production-quality certifying compiler and proof-carrying code system for Java. Also of direct practical benefit has been the development of the concept of oracle strings by George Necula, which are now used in our production implementations of PCC.
Typed Assembly Language (TAL) is an interesting and elegant idea that falls out naturally from the ideas of typed intermediate languages and proof-carrying code. We do research on TAL along with Greg Morrisett and his research group at Cornell.
Andrew Appel (Princeton), Amy Felty (Ottawa), Zhong Shao (Yale), and Adriana Compagnoni (Stevens Institute) are also working on proof-carrying code, as part of their Secure Internet Programming project. They are doing interesting work on scaling up PCC to production compilers, as well as developing key theoretical foundations.
Also at Princeton, Andrew Appel, Edward Felten, Michael Schneider, and Lujo Bauer have been developing the concept of proof-carrying authentication, which is a framework for distributed authentication based on higher-order logic.
At MIT, Martin Rinard has proposed an idea called credible compilers which is related to certifying compilers but achieves total correctness of each checked object file.
[ Home
| Contact Information
| Publications
| Researchers
]
[ FoxNet
| Typed Intermediate Languages
| Proof-Carrying Code
]
[ Logical Frameworks
| Staged Computation
| Language Design
]