Verified Enforcement of Automaton-based Information Release Policies. Nikhil Swamy and Michael Hicks. Technical Report CS-TR-4906, University of Maryland, Department of Computer Science, 2008. Full version of PLAS 08 paper.

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 ]

  AUTHOR = {Nikhil Swamy and Michael Hicks},
  INSTITUTION = {University of Maryland, Department of Computer Science},
  NUMBER = {CS-TR-4906},
  TITLE = {Verified Enforcement of Automaton-based Information Release Policies},
  MON = JUN,
  YEAR = 2008,
  NOTE = {Full version of PLAS 08 paper}

This file has been generated by bibtex2html 1.69