Paper presented by Adam Chlipala at the USENIX Symposium on Operating Systems Design and Implementation 2010.

We present a system for sound static checking of security policies for database-backed Web applications. Our tool checks a combination of access control and information flow policies, where the policies vary based on database contents. For instance, one or more database tables may represent an access control matrix, controlling who may read or write which cells of these and other tables.