@article {14754,
	title = {Verified enforcement of automaton-based information release policies},
	journal = {Proceedings of the 2008 Workshop on Programming Languages and Analysis for Security. ACM Press},
	year = {2008},
	month = {2008///},
	abstract = {Many organizations specify information release policies to describe the terms under which sensitive information may bereleased 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 λAIR, a core formalism for a functional programming language. λAIR 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 λAIR meet the requirements of the original AIR policy specification.
},
	author = {Swamy,N. and Hicks, Michael W.}
}
