Proof-Carrying Code: Design, Implementation and Applications

George Necula

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


Proof-carrying code (PCC) has been proposed as a general mechanism that allows the receiver of an untrusted program to check the program's compliance with certain key safety policies, such as type safety or disciplined resource management. To make this possible the program comes accompanied by an easy-to-check proof of compliance; this leaves to the receiver the easy task of proof checking. One of the major applications of PCC to date has been to instrument a Java compiler to produce proofs of type safety along with the optimized machine code. This enables a Java client to combine the speed of compiled code with the safety checking of bytecode, all in a slim package consisting mostly of a machine code parser and a proof checker.

In this talk we present a variant of Proof-Carrying Code (PCC) where the safety policy is represented as a higher-order logic program, the proof checker is replaced by a nondeterministic higher-order logic interpreter and the proof by an oracle implemented as a stream of bits that resolve the nondeterministic interpretation choices. Seen this way, Proof-Carrying Code allows the receiver of the code the luxury of using a simple yet powerful nondeterministic checking procedure.

This oracle-based variant of PCC is able to adapt quite naturally to situations when the property being checked is simple or there is a fairly directed search procedure for it. Furthermore, we are able to use standard techniques for optimizing logic interpreters in order to reduce the amount of non-determinism and thus reduce the size of oracles. As an example, we demonstrate that if PCC is used to verify type safety of assembly language programs compiled from Java source programs, the oracles that are needed are on the average just 7% of the size of the code, which represents an improvement of a factor of 40 over previous syntactic representations of PCC proofs. In this setting, PCC becomes as efficient as special-purpose techniques such as Typed Assembly Language, while remaining more general.