Proof-carrying code from certified abstract interpretation and fixpoint compression

F Besson, T Jensen, D Pichardie - Theoretical Computer Science, 2006 - Elsevier
Theoretical Computer Science, 2006Elsevier
Proof-carrying code (PCC) is a technique for downloading mobile code on a host machine
while ensuring that the code adheres to the host's safety policy. We show how certified
abstract interpretation can be used to build a PCC architecture where the code producer can
produce program certificates automatically. Code consumers use proof checkers derived
from certified analysers to check certificates. Proof checkers carry their own correctness
proofs and accepting a new proof checker amounts to type checking the checker in Coq …
Proof-carrying code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's safety policy. We show how certified abstract interpretation can be used to build a PCC architecture where the code producer can produce program certificates automatically. Code consumers use proof checkers derived from certified analysers to check certificates. Proof checkers carry their own correctness proofs and accepting a new proof checker amounts to type checking the checker in Coq. Certificates take the form of strategies for reconstructing a fixpoint and are kept small due to a technique for fixpoint compression. The PCC architecture has been implemented and evaluated experimentally on a byte code language for which we have designed an interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur.
Elsevier