|Title||Towards a Methodology and Tool for the Analysis of Security-Enhanced Linux Security Policies|
|Year of Publication||2002|
|Series Title||NRL Memorandum Report|
Security-Enhanced (SE) Linux, released by NSA in January, 2001, is a version of Linux that adds security features by superimposing the Flask architecture on its kernel. In this architecture, a security server decides whether to grant particular subjects (i.e., processes) permissions to particular objects. The decisions are based on a combination of type enforcement (TE), role-based access control (RBAC), and multilevel security (MLS) rules. SE Linux includes a policy language for defining these parts of the security policy. Because the policy language forces detailed specification of which access permissions may be granted, the relation of a policy definition to high level security goals is not obvious. The length and complexity of policy definitions (thousands of rules is typical) precludes proving a high level security property by inspection. For policy analysis, tool support is clearly needed. To be effective in practice, this tool support needs to be usable by members of the open source software community. This paper reports progress made towards adapting the theorem proving tool TAME to the analysis of SE Linux security policies, and making it usable to open source developers.