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.