Secure Internet Programming - menu
Secure Internet Programming
Princeton University
Department of Computer Science

Proof-Carrying Code
Faculty & Research Staff: Andrew Appel, David Walker, Roberto Virga
Students: Neophytos Michael , Kedar Swadi , Amal Ahmed, Juan Chen, Gang Tan, Simon Ou, Chris Richards, Dinghao Wu
External Collaborators:
Zhong Shao (Yale), Amy Felty (U. of Ottawa)

Proof-carrying code (PCC) is a promising new technology, developed in a proof-of-concept prototype by Necula and Lee. We propose to fully realize the ultimate impact of this technology by scaling it up to real programming languages, production compilers, and sophisticated security policies. We will pay particular attention to scalability, interoperability, efficiency, and the principled interaction of security policies with containment mechanisms.

(An overview of proof-carrying code by Peter Lee.)

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

Detailed project description:
Scaling Proof-Carrying Code to Production Compilers and Security Policies


Dependent Types Ensure Partial Correctness of Theorem Provers, by Andrew W. Appel and Amy P. Felty. Accepted for publication, Journal of Functional Programming.

A Stratified Semantics of General References Embeddable in Higher-Order Logic.  Amal J. Ahmed, Andrew W. Appel, and Roberto Virga.  Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 75-86, Copenhagen, Denmark, July 2002.

A Trustworthy Proof Checker, by Andrew W. Appel, Neophytos G. Michael, Aaron Stump, and Roberto Virga. Princeton University CS TR-648-02, April 2002.

JVM TCB: Measurements of the Trusted Computing Base of Java Virtual Machines, by Andrew W. Appel and Daniel C. Wang. Princeton University CS TR-647-02, April 2002.

Typed Machine Language and its Semantics, by Kedar N. Swadi and Andrew W. Appel, preliminary version of July 2001.

Foundational Proof-Carrying Code. Andrew W. Appel, in 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), June 2001 (to appear).

An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. Andrew W. Appel and David McAllester. ACM Transactions on Programming Languages and Systems 23 (5) 657-683, September 2001.

Machine Instruction Syntax and Semantics in Higher Order Logic. Neophytos G. Michael and Andrew W. Appel. 17th International Conference on Automated Deduction (CADE-17), Springer-Verlag (Lecture Notes in Artificial Intelligence), June 2000 (to appear).

A Semantic Model of Types and Machine Instructions for Proof-Carrying Code, Andrew W. Appel and Amy P. Felty, 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '00), pp. 243-253, January 2000.

Lightweight Lemmas in Lambda Prolog, Andrew W. Appel and Amy P. Felty, in 16th International Conference on Logic Programming, pp. 411-425, MIT Press, November 1999.

Protection against untrusted code. Andrew W. Appel. IBM Developer Works, September 1999.