Proof Carrying Code

By George Necula 

Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Langauges (POPL '97)

The main contribution of the paper is a mechanism that shifts the
burden of verifying the safety properties of a piece of untrusted code
to the code producer, away from the code consumer. The code consumer
only needs to specify a safety policy in terms of inference
rules. This policy forms the basis of the proof generated by the
producer. The burden is on the code producer to come up with
appropriate safety proof that can be automatically validated by the
consumer using the predefined inference rules. 

For this the producer generates predicates and searched for a proof
modulo the inference rules. Presumably, this searching for the proof
can be quite complex and may require sophisticated offline
analysis. The proof can be validated once by the consumer
automatically, by generating the same predicates, and following the
proof steps automatically. This moves the task of verification away
from critical performance paths, paving the way for certifying
compilers to simplify the task of program verification.

Advantages:

1. Tamperproof: Tampering with PCC will result in proof that is no
longer valid, or with a valid proof that preserves safety.  

2. Orthogonal to cryptography (which only establishes identity of code
producer and ownership) or execution monitoring or the need to rely on
trusted third parties.

3. Significant performance advantages by moving program verification
away from critical performance paths by replacing it with a
sophisticated do-it-once static analysis. Can be used to build
certifying compilers.

Disadvantages:

1. General safety problem is undecidable. The authors have focused
type-checking and memory safety issues which are decidable and simple
to specify.

2.Program verification of large programs written in HLL (High level
languages) can be very complicated, non trivial and time
consuming. PCC may not scale in these cases.

3. In the example, searching for the proof is not much harder than
validating it for the problem they are focusing on. What is more
interesting is how this works in general for large programs and for
software modules that interact with other modules and other open
systems.