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.
Downloads
On the Synthesis of
Proof-Carrying Temporal Reference Monitors (gzipped PostScript)
Simon Winwood, Gerwin Klein, and Manuel Chakravarty.
In Proceedings of LOPSTR'06, Venice, Italy, 2006.
(bibtex)
The prototype may be found here.
For those that wish to view the output only, the Isabelle/HOL file
containing the required theorems is here and the file
containing the output for the sample theorem in the above paper is
here.
[an error occurred while processing this directive]