[Club2] Club2: Proof Carrying Code in Isabelle/HOL

[Martin Wildmoser]

Liebe Kolleginnen und Kollegen,

ich lade Sie herzlich ein zu Vortraegen zum
Themenkomplex  "Proof Carrying Code, Jinja Bytecode
und Programmanalyse mit und in Isabelle/HOL".

A)
Titel: Asserting Bytecode Safety
Zeit: 24.3.2005 14:00 - 14:25
Raum: 00.09.055 (Alan Turing)

B)
Titel: Bytecode Analysis and Proof Carrying Code
Zeit: 24.3.2005 14:30 - 14:45
Raum: 00.09.055 (Alan Turing)


Abstract A)

We instantiate an Isabelle/HOL framework
for proof carrying code to Jinja bytecode, a downsized
variant of Java bytecode featuring objects,
inheritance, method calls and exceptions.
Bytecode annotated in a first order expression language can be certified 
not to produce arithmetic overflows. For this purpose we use a generic 
verification condition generator, which we have proven correct and 
relatively complete.

Abstract B)

Out of annotated programs proof carrying code systems construct and 
prove verification conditions that guarantee a given safety policy. The 
annotations may come from various program analyzers and must not
be trusted as they need to be verified. A generic verification condition 
generator can be utilized such that a combination of annotations is 
verified incrementally. New annotations may be verified by using 
previously verified ones as trusted facts.
We show how results from a trusted type analyzer may be
combined with untrusted interval analysis to automatically verify that 
bytecode programs do not overflow. All trusted components are formalized 
and verified in Isabelle/HOL.

Viele Gruesse,
Martin Wildmoser