Copenhagen Programming Language Seminar


Abstraction-Carrying code

German Puebla Technical University of Madrid (UPM)
Elvira AlbertComplutence University of Madrid (UCM)

Thursday, November 11th, 15:15-16:15
ITU, Rued Langgaards Vej 7, room 2A.12


Recent approaches to mobile code safety, like "proof-carrying code", involve associating safety information to programs. The code supplier provides a program and also includes with it a certificate (or "proof") whose validity entails compliance with a predefined safety policy. The intended benefit is that the program consumer can locally validate the certificate w.r.t. the "untrusted" program by means of a certificate checker---a process which should be much simpler, efficient, and automatic than generating the original proof. This talk presents a novel approach to mobile code safety which follows a similar scheme, but which is based throughout on the use of abstract interpretation techniques. In our framework the safety policy is specified by using an expressive assertion language defined over abstract domains. We identify a particular subset of the abstract interpretation-based static analysis results which is especially useful as a certificate. The validity of the certificate on the consumer side is checked by a very simplified and efficiently specialized abstract-interpreter. The resulting scheme has been implemented and benchmarked within the CiaoPP system, which will be demonstrated during the talk.

Scientific host: Morten Rhiger. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
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