Verified Enforcement of Stateful Information Release Policies. Nikhil Swamy and Michael Hicks. In Proceedings of the ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS), pages 21–32, June 2008.

Many organizations specify information release policies to describe the terms under which sensitive information may be released to other organizations. This paper presents a new approach for ensuring that security-critical software correctly enforces its information release policy. Our approach has two parts. First, an information release policy is specified as a security automaton written in a new language called AIR. Second, we enforce an AIR policy by translating it into an API for programs written in Lair, a core formalism for a functional programming language. Lair uses a novel combination of dependent, affine, and singleton types to ensure that the API is used correctly. As a consequence we can certify that programs written in Lair meet the requirements of the original AIR policy specification.

[ .pdf ]

@inproceedings{swamy08air,
  author = {Nikhil Swamy and Michael Hicks},
  title = {Verified Enforcement of Stateful Information Release Policies},
  booktitle = {Proceedings of the {ACM SIGPLAN} Workshop on Programming Languages and Analysis for Security (PLAS)},
  month = jun,
  year = 2008,
  pages = {21--32}
}

This file was generated by bibtex2html 1.99.