Efficient security analysis of administrative access control policies

In recent years access control has been a crucial aspect of computer systems, since it is the component responsible for giving users specific permissions enforcing a administrator-defined policy. This lead to the formation of a wide literature proposing and implementing access control models reflecting different system perspectives. Moreover, many analysis techniques have been developed with special attention to scalability, since many security properties have been proved hard to verify. In this setting the presented work provides two main contributions. In the first, we study the security of workflow systems built on top of an attribute-based access control in the case of collusion of multiples users. We define a formal model for an ARBAC based workflow system and we state a notion of security against collusion. Furthermore we propose a scalable static analysis technique for proving the security of a workflow. Finally we implement it in a prototype tool showing its effectiveness. In the second contribution, we propose a new model of administrative attribute-based access control (AABAC) where administrative actions are enabled by boolean expressions predicating on user attributes values. Subsequently we introduce two static analysis techniques for the verification of reachability problem: one precise, but bounded, and one over-approximated. We also give a set of pruning rules in order to reduce the size of the problem increasing scalability of the analysis. Finally, we implement the analysis in a tool and we show its effectiveness on several realistic case studies.