Prof. Dr. Heike Wehrheim

Abstract:

Proof-carrying code approaches aim at the safe execution of untrusted code by having the code producer attach a safety proof to the code which the code consumer only has to validate. Depending on the type of safety property, proofs can however become quite large and their validation - though faster than their construction - still time consuming.

Programs from Proofs is a new concept for the safe execution of untrusted code. It keeps the idea of putting the time consuming part of proving on the side of the code producer, however, attaches no proofs to code anymore, but instead uses the proof to transform the program into an equivalent but more efficiently verifiable program. Code consumers thus still do proving themselves, however, on a computationally inexpensive level only. The talk will give an introduction to this general framework and illustrate it by verifying type-state properties of programs, i.e. adherence of program executions to protocols specified in finite state automata.