In International Symposium on
Logic-based Program Synthesis and Transformation (LOPSTR 2006), LNCS,
Springer-Verlag, 2006.
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.
PostScript version (16 pages)
This page is part of Manuel Chakravarty's WWW-stuff.