On the automated synthesis of proof-carrying temporal reference monitors

Simon Winwood, Gerwin Klein, and Manuel M. T. Chakravarty.

In International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2006), LNCS, Springer-Verlag, 2006.

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.

PostScript version (16 pages)

This page is part of Manuel Chakravarty's WWW-stuff.