Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Enforcing Stateful Authorization and Information Flow Policies in Fine

Nikhil Swamy, Juan Chen, and Ravi Chugh

Abstract

Proving software free of security bugs is hard. Programming language support to ensure that programs correctly enforce their security policies would help, but, to date, no language has the ability to verify the enforcement of the kinds of policies used in practice---dynamic, stateful policies which address a broad 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.

Details

Publication typeInproceedings
Published inESOP 2010: 19th European Symposium on Programming
NumberMSR-TR-2009-164
PublisherSpringer Verlag
> Publications > Enforcing Stateful Authorization and Information Flow Policies in Fine