Modeling security-enhanced Linux policy specifications for analysis

Security-Enhanced (SE) Linux is a modification of Linux initially released by NSA in January 2001 that provides a language for specifying Linux security policies and, as in the Flask architecture, a security server for enforcing policies defined in the language. To determine whether user requests to the operating system should be granted, the security server refers to an internal form of the policy compiled from the policy specification. Since the most convenient description of the policy for user understanding is its "source" specification in the policy language, it is natural for users to expect to be able to analyze the properties of the policy from this source specification. However, though specifications in the SE Linux policy language avoid implementation details, the policy language is very low-level, making the high level properties of a policy difficult to deduce by inspection. For this reason, tools to help users with the analysis are necessary. The goal of the NRL project on analyzing SE Linux security policies is to first use mechanized support to analyze the specification of an example policy, and then to customize this support for use by practitioners in the open source software community. The paper summarizes how we have modeled an example security policy in the analysis tool TAME, the kinds of analysis we can support, and prototype mechanical support to enable others to model example security policies in TAME.