|Title||Modeling Security-Enchanced Linux Policy Specifications for Analysis|
|Publication Type||Conference Paper|
|Year of Publication||2003|
|Authors||Archer, M., E. Leonard, and M. Pradella|
|Conference Name||Research Summaries for DISCEX III|
|Conference Location||Washington, D.C.|
NSA's Security-Enhanced (SE) Linux enhances Linux by providing a specification language for security policies and a Flask-like architecture with a security server for enforcing policies defined in the language. While the security server refers to an internal form of the policy compiled form the policy specification, the description of the policy most understandable to the user 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. But 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 NRL project on analyzing SE Linux policies aims first to use mechanized support to analyze an example policy specification and then to customize this support for use by practitioners in the open source software community. This paper describes how we model policies in the analysis tool TAME, the kinds of analysis we can support, and prototype mechanical support to enable others to model example policies in TAME. The paper concludes with some general observations on desirable properties for a policy language. This paper summarizes the research described in our full paper that is to appear in the proceedings of the IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY 2003), Lake Como, Italy, June 4-6, 2003. The longer paper is also available as NRL Memorandum Report NRL/MR/5540--03-8659.
|NRL Publication Release Number|| |