Model-based safety analysis of SELinux security policies

Since security has become an essential asset in numerous application areas, the integration of security policies has become a major issue in the design of security architectures, and many commodity operating systems have been furnished with abstractions to support policy protection and enforcement. Given a security policy´s key position in defining and implementing a system´s security properties, quality attributes such as policy correctness, completeness, or consistency are essential objectives in policy engineering. On the other hand, considering the large amount of their responsibilities, security policies often are large and complex, rendering the analysis and proof of crucial quality attributes difficult. This paper is a step towards tool-supported security policy analysis. It presents a model-based approach to analyze the dynamic proliferation of access rights in a policy-controlled SELinux access control system.