DARPA ISO Sponsored Research

2000 Project Summary
Scaling Proof-Carrying Code to Production Compilers and Security Policies
Princeton University and Yale University

Project Website:  http://www.cs.princeton.edu/sip/projects/darpapcc.php3 -- Additional project information provided by the performing organization 
Quad Chart:  Quad Chart   provided by the performing organization
Objective: The objective of this project is to develop an advanced mobile-code infrastructure that would dramatically improve the inherent survivability property of the end system. The project takes Necula and Lee's proof-carrying code (PCC) prototype framework and scales it up to real programming languages, production compilers, and sophisticated security policies. The main focus is to reduce the size of the trusted computing base (TCB) while still maintaining scalability, interoperability, efficiency, and the principled interaction of security policies with containment mechanisms.

This research will dramatically expand the impact of PCC in several ways: it will generalize and simplify the safety policies to allow higher assurance and more flexibility of the policies themselves; it will provide production-quality certifying compilers for mainstream programming languages such as Java and ML; and it will use PCC to express much more sophisticated security policies than the simple safety properties that were demonstrated in the first prototypes. 

Approach: The proposed work on PCC can be divided into three main areas: 

Language independence, scalability, and high-assurance safety policies. In the systems demonstrated by Necula and Lee, each code consumer's safety policy is based on the way a specific compiler lays out program and data structures. A host using such axioms will not easily accept programs originally written in other languages. This project will show how clients can rely on much more general axiom sets, so that code producers have much more flexibility in choice of programming languages and compilers. These safety policies will be smaller, simpler, and will naturally have higher assurance than safety policies tailored to a particular type system.

Production-quality certifying compilers for real programming languages. A code producer must either prove safety properties by hand (which is impractical for any but tiny programs) or use a certifying compiler. The best technology for building certifying compilers is through the use of typed intermediate languages. This project will use the FLINT typed intermediate language for compiling object-oriented, functional, and imperative source languages. It will provide a high-quality, robust, optimizing, certifying compiler for ML and for Java---allowing principled interoperability and fully automatic generation of PCC on real languages. 

Support for high-level security policies. This project will extend PCC to handle not only safety policies (such as ``all memory accesses are in the valid region'') but also full-fledged security policies (every access to resource X has a proper chain of authorization). This will allow the principled interaction of mobile code containment (the usual stated goal of PCC technology) with the enforcement of higher-level security properties.

Recent FY-99/FY-00 Accomplishments: This project started in June 1999.
FY-00 Plans: Distribution of the Security Logic as a technical report for peer review.

Prototype prover/checker implemented for research in proof engineering.

Distribution of alpha-release Certifying compiler software for preliminary use by applications programmers.

Technology Transition: The software products resulting from this research will be distributed with source code and should be directly usable by others. The Certifying Compiler will be immediately usable by the same user community that now uses Standard ML of New Jersey, but (since it will be certifying) will provide even higher levels of assurance and safety. The Prover/checker software will be a tool for generating and verifying efficient machine-readable proofs of software properties. The Security PCC software will be a useful and extremely flexible infrastructure for building distributed security systems. The low-level FLINT intermediate language will serve as an excellent platform-independent mobile executable content. 

Other components of this research are either theoretical results underpinning the practical implementations or prototype software that will evolve later into the architecture for future secure systems. The PIs will publish the research results and present them at conferences and workshops so that the entire community can take advantage of their experience. 

The PIs have a track record in distributing production-quality research software in usable form: the Standard ML of New Jersey software (including FLINT) has thousands of users at hundreds of sites. The SML/NJ compiler has been used to implement many important pieces of research software, including many components of the research at CMU in proof-carrying code and related technologies: Touchstone compiler, Elf theorem prover, TIL compiler, Foxnet system. Furthermore, SML/NJ is an open system: it is distributed with source code, which is sufficiently well documented in books and research papers that many researchers have been able to modify the system for their own compiler-related research, and use elements of its structure in the design of their own systems. The PCC system will be up to the same standard: a robust, usable system distributed with source code well-documented by research publications and user manuals.

Principal Investigator: Andrew Appel
Department of Computer Science
Princeton University
35 Olden Street
Princeton, NJ 08544-2087
(609) 258-4627
(609) 258-1771 fax
appel@cs.princeton.edu

Edward Felten
Department of Computer Science
Princeton University
35 Olden Street
Princeton, NJ 08544-2087
(609) 258-5906
(609) 258-1771 fax
felten@cs.princeton.edu

Zhong Shao
Department of Computer Science
Yale University
51 Prospect Street
New Haven, CT 06520-8285
(203) 432-6828
(203) 432-0593 fax
shao-zhong@cs.yale.edu