George Necula's Publications

Technical reports

Ph.D. Thesis

An annotated bibliography on Proof-Carrying Code

Note: This is not up to date anymore. Now it should contain also many papers by other authors.

Note: this bibliography is now out of date and does not include papers written by other researchers. The following papers are ordered by their technical difficulty, starting with the gentlest introductions to the Proof-Carrying Code technique and ending with a detailed implementation guide. These papers address different aspects of Proof-Carrying Code, ranging from its foundations in type-theory and logic, to its applications in software systems. I recommend first the application papers since the papers dealing with type-theory and logic might seem too technical to the reader that is not experienced in these areas. However, even in the most technical of the papers, we have tried to get across the purely practical and engineering motivations for most of the formal developments, and so, they might make an interesting reading even for the non-specialist

 For the busy reader, here is a one-page introduction to Proof-Carrying Code: "Research on Proof-Carrying Code for Untrusted-Code Security". George C. Necula and Peter Lee. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, Oakland, 1997.

 Another short paper about Proof-Carrying Code, with an emphasis on its applications for mobile-code security: "Research on Proof-Carrying Code on Mobile-Code Security". George C. Necula and Peter Lee. In Proceedings of the Workshop on Foundations of Mobile Code Security, Monterey, 1997.

 Next comes our first paper on PCC, paper which received the Best Paper Award at OSDI'96. "Safe Kernel Extensions Without Run-Time Checking". George C. Necula, Peter Lee. Presented at OSDI'96,October 1996.

If you want to read about more applications on the spirit of network packet filters, then you can read the expanded version of the OSDI'96 paper. Keep in mind, however, that some of the later papers might describe PCC slightly differently, as our own understanding of it has improved.

 Next paper is the standard reference for PCC. "Proof-Carrying Code ". George C. Necula. Presented at POPL97, January 1997.

·  Abstract: This paper describes Proof-Carrying Code from a more formal and language-theoretic perspective. On the application side, this paper describes the use of PCC as a basis for verifying the type safety of hand-optimized assembly language programs. This is useful for the safe interaction of native code libraries with code written in a type-safe language.

 Next is a recent paper that describes part of my thesis work. The Design and Implementation of a Certifying Compiler , George C. Necula, Peter Lee, June 1998, presented at PLDI'98.

·  Abstract: This paper presents a compiler from a type-safe subset of the C language to optimized DEC Alpha machine code. The novel feature of the compiler is that it contains a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the assembly-language target program. The ensemble of the compiler and the certifier is called a certifying compiler.

Several advantages of certifying compilation over previous approaches can be claimed. The notion of a certifying compiler is significantly easier to employ than a formal compiler verification, in part because it is generally easier to verify the correctness of the result of a computation than to prove the correctness of the computation itself. Also, the approach can be applied even to highly optimizing compilers, as demonstrated by the fact that our compiler generates target code, for a range of realistic C programs, which is competitive with both the cc and gcc compilers with all optimizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might otherwise require many executions to detect. Finally, this approach is a practical way to produce the safety proofs for a Proof-Carrying Code system, and thus may be useful in a system for safe mobile code.

 This is the most technical paper on PCC. It describes the framework that is used in PCC to represent and to verify the safety proofs: Efficient Representation and Validation of Proofs George C. Necula, Peter Lee, June 1998, presented at LICS'98.

·  Abstract: This paper presents a logical framework derived from the Edinburgh Logical Framework (LF) that can be used to obtain compact representations of proofs and efficient proof checkers. These are essential ingredients of any application that manipulates proofs as first-class objects, such as a Proof-Carrying Code system, in which proofs are used to allow the easy validation of properties of safety-critical or untrusted code.

Our framework, which we call LFi, inherits from LF the capability to encode various logics in a natural way. In addition, the LFi framework allows proof representations without the high degree of redundancy that is characteristic of LF representations. The missing parts of LFi proof representations can be reconstructed during proof checking by an efficient reconstruction algorithm. We also describe an algorithm that can be used to strip the unnecessary parts of an LF representation of a proof. The experimental data that we gathered in the context of a Proof-Carrying Code system shows that the savings obtained from using LFi instead of LF can make the difference between practically useless proofs of several megabytes and manageable proofs of tens of kilobytes.

This paper is an abbreviated version of a longer (70 pages) technical report. Read it if you want to see the detailed (15 pages) proofs of soundness of the efficient proof-checking algorithm that is used in PCC.

 This longer paper describes many of the implementation details of our PCC prototype. It also describes the use of PCC for enforcing resource-usage bounds in addition to memory and type-safety. Safe, Untrusted Agents using Proof-Carrying Code George C. Necula, Peter Lee. October 1997, in LNCS 1419: Special Issue on Mobile Agent Security.

·  Abstract: This paper is intended to be both a comprehensive implementation guide for a Proof-Carrying Code system and a case study for using PCC in a mobile agent environment. Specifically, the paper describes the use of PCC for enforcing memory safety, access control and resource usage bounds for untrusted agents that access a database.

My home page