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 pasttime 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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Winwood, S., Klein, G., & Chakravarty, M. M. T. (2007). On the automated synthesis of proof-carrying temporal reference monitors. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4407 LNCS, pp. 111–126). Springer Verlag. https://doi.org/10.1007/978-3-540-71410-1_9
Mendeley helps you to discover research relevant for your work.