Faculty & Research Staff:
Neophytos Michael ,
Kedar Swadi ,
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
(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,
Protection against untrusted code. Andrew W. Appel.
IBM Developer Works, September 1999.