On the automated synthesis of proof-carrying temporal reference monitors

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

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.

Online Copy

Available as [PDF]

Bibtex entry

@inproceedings{WinwoodKC-06,
  author =       {Simon Winwood and Gerwin Klein and Manuel M. T. Chakravarty},
  title =        {On the automated synthesis of proof-carrying temporal reference monitors},
  booktitle =    {International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 06)},
  year =      {2007},
  series =    {LNCS},
  volume =    4407,
  editor =    {Germán Puebla},
  address =   {Italy},
  pages =     {111--126},
  publisher = {Springer}
}
Gerwin Klein
2006-06-22 12:44:48