Towards a Methodology and Tool for the Analysis of Security-Enhanced Linux Security Policies
Abstract
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) pernaissions 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 16, 2002
- Accession Number
- ADA409228
Entities
People
- Elizabeth Leonard
- Matteo Pradella
- Myla M. Archer
Organizations
- United States Naval Research Laboratory