Prooflets: A general paradigm for auto-certifiable mobile code and its implementation in the Coq Proof Assistant
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.