@article {14756,
	title = {Verified enforcement of stateful information release policies},
	journal = {SIGPLAN Not.},
	volume = {43},
	year = {2009},
	month = {2009/02//},
	pages = {21 - 31},
	abstract = {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.},
	keywords = {affine types, certified evaluation, declassification, dependent types, singleton types, state modifying policies},
	isbn = {0362-1340},
	doi = {10.1145/1513443.1513448},
	url = {http://doi.acm.org/10.1145/1513443.1513448},
	author = {Swamy,Nikhil and Hicks, Michael W.}
}
