@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.}
}
@conference {14750,
	title = {Trusted declassification:: high-level policy for a security-typed language},
	booktitle = {Proceedings of the 2006 workshop on Programming languages and analysis for security},
	series = {PLAS {\textquoteright}06},
	year = {2006},
	month = {2006///},
	pages = {65 - 74},
	publisher = {ACM},
	organization = {ACM},
	address = {New York, NY, USA},
	abstract = {Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterferencewhich ensures that high-security data will not be observable on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassification to selectively leak high security information, e.g. when performing a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult.In this paper, we propose a simple idea we call trusted declassification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declaratively specify which declassifiers they trust so that all information flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java-like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have implemented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.},
	keywords = {<i>noninterference modolo trusted methods</i>, declassification, FJifP, information-flow control, Jif, security policy, security-typed languages, trusted declassification},
	isbn = {1-59593-374-3},
	doi = {10.1145/1134744.1134757},
	url = {http://doi.acm.org/10.1145/1134744.1134757},
	author = {Hicks,Boniface and King,Dave and McDaniel,Patrick and Hicks, Michael W.}
}
