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.

@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}
}