Abstract

Access Control is becoming increasingly important for today's ubiquitous systems. Sophisticated security requirements need to be ensured by authorization policies for increasingly complex and large applications. As a consequence, designers need to understand such policies and ensure that they meet the desired security constraints while administrators must also maintain them so as to comply with the evolving needs of systems and applications. These tasks are greatly complicated by the expressiveness and the dimensions of the authorization policies. It is thus necessary to provide policy designers and administrators with automated analysis techniques that are capable to foresee if, and under what conditions, security properties may be violated. For example, some analysis techniques have already been proposed in the literature for Role-Based Access Control (RBAC) policies. RBAC is a security model for access control that has been widely adopted in real-world applications. Although RBAC simplifies the design and management of policies, modifications of RBAC policies in complex organizations are difficult and error prone activities due to the limited expressiveness of the basic RBAC model. For this reason, RBAC has been extended in several directions to accommodate various needs arising in the real world such as Administrative RBAC (ARBAC) and Temporal RBAC (TRBAC). This Dissertation presents our research efforts to find the best trade-off between scalability and expressiveness for the design and benchmarking of analysis techniques for authorization policies. We review the state-of-the-art of automated analysis for authorization policies, identify limitations of available techniques and then describe our approach that is based on recently developed symbolic model checking techniques based on Satisfiability Modulo Theories (SMT) solving (for expressiveness) and carefully tuned heuristics (for scalability). Particularly, we present the implementation of the techniques on the automated analysis of ARBAC and ATRBAC policies and discuss extensive experiments that show that the proposed approach is superior to other state-of-the-art analysis techniques. Finally, we discuss directions for extensions.