Oracle-based checking of untrusted software

We present a variant of Proof-Carrying Code (PCC) in which the trusted inference rules are 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. In this setting, ProofCarrying Code allows the receiver of the code the luxury of using nondeterminism in constructing a simple yet powerful 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. 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 12% of the size of the code, which represents an improvement of a factor of 30 over previous syntactic representations of PCC proofs.

• Type: Conference
• Year: 2001
• Where: POPL
• Authors: George C. Necula, Shree Prakash Rahul
• Keywords: Assembly Language Programs, Nondeterministic Interpretation Choices, POPL 2001, Powerful Checking Procedure, Programming Languages