Analyzing Security-Enhanced Linux Policy Specifications.

摘要

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 from 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 report 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 report concludes with some general observations on desirable properties for a policy language.