Towards a Formal Model for Security Policies Specification and Validation in the SELinux system

This paper presents a formal model, called SELAC, for analyzing an arbitrary security policy configuration for the SELinux system. A security policy for SELinux is complex and large: it is made by many configuration rules that refer to the access control sub-models implemented in the system. Among the rules composing a security policy configuration, many relationships occur and it is extremely difficult to understand their overall effects in the system. Our aim is to define semantics for the constructs of the SELinux configuration language and to model the relationships occurring among sets of configuration rules. Finally, we develop an algorithm based upon SELAC, which can verify whether, given an arbitrary security policy configuration, a given subject can access a given object in a given mode.