Copenhagen Programming Language Seminar


Proof-carrying code from certified abstract interpretation

Thomas Jensen,
IRISA, Rennes, France

Friday, February 9th, Time: 14:00 - 15:00 (!)
IT University of Copenhagen, Rued Langgaards Vej 7, auditorium 3


Proof-Carrying Code (PCC) is a technique for downloading mobile code on a host machine in which the code comes with a proof that the code adheres to the host's safety policy. In this talk I'll show how certified abstract interpretation can be used to build a PCC architecture where the code producer can produce program certificates automatically and 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 approach will be illustrated on a byte code language for which we have designed an enhanced interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur.

Scientific host: Peter Sestoft. Administrative host: Camilla Torp-Smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org