Oracle-Based Checking of Untrusted Software Seminars/Workshops

Abstract

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 review the basic motivation and design of a PCC infrastructure for Java and then we focus on novel aspects of the design that enabled us to scale to Java programs up to 100,000 lines. First, we observed that actual proofs of Java type safety can be very large even though they are quite shallow in mathematical content. This motivated us to develop a variant of PCC in which the proof checker is replaced by a non-deterministic theorem prover, which is simple yet quite powerful. The proof is then replaced by a sequence of bits acting as an oracle that the prover uses to resolve its non-deterministic choices. If the oracle guides the prover to success then the code is accepted.

There are many advantages to this oracle-based design of PCC, most notable of which being that the size of oracles adapts naturally to the complexity of the property being checked. In the particular case of proofs of type safety for assembly language programs obtained from Java source programs, the oracles are only 15% of the size of machine code, which is more than an order of magnitude smaller than the corresponding proofs. We will conclude the presentation with a discussion of a number of other design and engineering choices that were necessary to achieve scalability.