@inbook {IOPORT.05703422, author = {Swamy, Nikhil and Chen, Juan and Chugh, Ravi}, title = {Enforcing stateful authorization and information flow policies in fine.}, year = {2010}, booktitle = {Programming languages and systems. 19th European symposium on programming, ESOP 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20--28, 2010. Proceedings}, isbn = {978-3-642-11956-9}, pages = {529-549}, publisher = {Berlin: Springer}, doi = {10.1007/978-3-642-11957-6_28}, abstract = {Summary: Proving software free of security bugs is hard. Languages that ensure that programs correctly enforce their security policies would help, but, to date, no security-typed language has the ability to verify the enforcement of the kinds of policies used in practice-dynamic, stateful policies which address a range of concerns including forms of access control and information flow tracking. This paper presents Fine, a new source-level security-typed language that, through the use of a simple module system and dependent, refinement, and affine types, checks the enforcement of dynamic security policies applied to real software. Fine is proven sound. A prototype implementation of the compiler and several example programs are available from \url{http://research.microsoft.com/fine}.}, identifier = {05703422}, }