Granalyze: towards the automatic verification of Grsecurity RBAC policies

Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy specifications arising from system administrators' needs, formally verifying that access control systems enforce some defined security invariants is a problem of crucial importance. In a previous work which has been accepted for presentation at IEEE CSF 2012, we developed a framework for the formal verification of Grsecurity RBAC, an access control system developed on top of Unix/Linux systems. In this thesis we improve the framework by considering the interaction with the underlying operating system. This refinement allows for a reduction in the number of transitions within the labelled transition systems resulting from policies. Additionally, we deal with the problem of automatic verification of Grsecurity RBAC policies by defining a set of security invariants. Based on our abstract semantics, we implement Granalyze, a model checker that accounts for the verification of real policies. We report on the results of the experimental analysis conducted using the tool on existing public servers running Grsecurity RBAC.