Verifying information flow goals in Security-Enhanced Linux

A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an Selinux configuration, provides the framework for determining information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux.