[Club2] Mo. 24.07. 16.00 (Turing)

[Norbert Schirmer]

Next Monday, 24.07. 16.00 (Room: Turing, 00.09.055)

Simon Winwood:

On the Synthesis of Proof-Carrying Temporal Reference Monitors 


Abstract

 We extend the range of security policies that can be guaranteed with proof 
carrying code from the classical type safety, control safety, memory safety, 
and space/time guarantees to more general security policies, such as general 
resource and access control. We do so by means of (1) a specification logic 
for security policies, which is the past-time fragment of LTL, and (2) a 
synthesis algorithm generating reference monitor code and accompanying proof 
objects from formulae of the specification logic. To evaluate the feasibility 
of our approach, we developed a prototype implementation producing proofs in 
Isabelle/HOL. 


   Norbert