Prooflets: A general paradigm for auto-certifiable mobile code and its implementation in the Coq Proof Assistant

Gérard Huet ( INRIA )

The paradigm of mobile code is gaining wide applicability with the development of Java and its variants. However, unchecked execution of possibly hostile mobile code is clearly problematic for security reasons. Type-checking and other static analysis may reveal some unsafe programs, but such techniques are not sufficient to guarantee that a piece of code will respect some security policy, or will achieve its intended aim. Using authentication protocols based on cryptography is the only practical solution to this problem today, but this limits significantly the distribution model and it suffers from export restrictions and national regulations concerning encryption technology.

Another paradigm is to send not just the executable code, but a proof of its safety specifications as well. This proof may be checked at reception, prior to execution of the code. Variants of this general scheme may generate the program from the proof, or conversely generate the proof from an appropriately annotated version of the program. This general methodology is simple to understand, but not easy to implement in a feasible manner. One needs to agree on a format for such "proof carrying code", the proof assistant where the proof has been developed must be able to represent it as a formal object of manageable size, the client must be equipped with a trustable proof checker efficient enough for on-the-fly verification, the problem of incremental proof libraries must be dealt with, the whole scheme must be consistent with version management of the proof assistants, etc.We shall describe in this talk an implementation of this paradigm in the Coq proof assistant, and provide experimental measurements showing its practical feasibility.

This talk describes joint research with Ajay Chander.