Encoding Stateful Authorization and Information Flow Policies in Fine

Nikhil Swamy, Juan Chen, and Ravi Chugh
ESOP 2010 [ paper | tech report ]

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 here.