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.