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 has been generated by bibtex2html 1.69