PhD Dissertation International Doctorate School in Information and Communication Technologies DISI - University of Trento Efficient Automated Security Analysis of Complex Authorization Policies Anh Tuan Truong Advisors: Dr. Silvio Ranise and Prof. Alessandro Armando Security and Trust Unit, FBK-Irst, Trento, Italia March 2015 Committee Members: Professor Pierangela Samarati Department of Computer Science, University of Milano, Italia pierangela.it Professor Luca Viganò Department of Informatics, King’s College London, United Kingdom luca.uk Professor Armando Tacchella DIBRIS Department, University of Genoa, Italia armando.it Abstract Access Control is becoming increasingly important for today’s ubiqui- tous 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 appli- cations. These tasks are greatly complicated by the expressiveness and the dimensions of the authorization policies. It is thus necessary to provide pol- icy 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 manage- ment 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 sev- eral 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 re- cently 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. Keywords Access Control, Administration, Temporal Access Control, Automated Analysis, Safety Analysis, Security Analysis Problems, Model checking, Heuristics to Avoid the State Space Explosion Problems.
6 Acknowledgment Many other people contribute to this Dissertation. First of all, I would like to express my special appreciation and thanks to my beloved advisors: Dr. Silvio Ranise and Professor Alessandro Armando, for everything you have done to me. Indeed, words cannot express enough how much thanks I want to send to you.
I cannot imagine what my PhD research would has been without your encouragement, support, advice, and patience. Honestly, I was very lucky to meet and do research under your supervision. I would also like to thank Professor Pierangela Samarati, Professor Luca Viganò, and Professor Armando Tacchella, for your acceptance to be my PhD Committee members. I really appreciate brilliant comments and great encouragement you gave me during the defense.
Also, I want to thank you for letting my defense be an enjoyable discussion and one of the happiest moments in my life. The good results in this Dissertation cannot be obtained without great support from all my colleagues at the Security & Trust unit, Fondazione Bruno Kessler (FBK): Roberto, Clara, Laura, Riccardo, Annibale, Luca, Eliana, Matteo, Hari, Alessio, Avinash, Nadia, Daniel, Giada, Mojtaba, Stanislav, Federico, Eyasu, Harendra, Fatih and many former members of the unit. Thank you all for creating the motivating working environment and friendly community at the unit. One of the main contributions of this Dissertation has been made during my visit to King’s College London, United Kingdom and joint work with Professor Luca Viganò.
Thank you for your guidance, valuable advice, and friendliness. I also want to thank Davide Guardini and Michele Peroli for making my stay at the UK enjoyable. I also want to thank a lot of wonderful friends from Vietnam and other countries around the world (I cannot mention all of them here !). We had a lot of parties, discussion, and travel together.
These make me feel happy and balance my work and life. Lastly, this Dissertation is dedicated to my family: my grandfathers, grandmothers, my father, mother, sisters and brothers. Words cannot ex- press how grateful I am to you all. Thank you for your trust in me, your prayer for my life, and your time whenever I need.
Thank you All very much, Anh Tuan Truong Trento, March 2015.2 The Structure of this Dissertation. 7 2 RBAC and its Extensions 9 2.1 Role-Based Access Control .2 An Extension: Administrative RBAC .3 Security Analysis of Authorization Policies. 14 3 The Problem: Security Analysis of Access Control Policies 17 3.1 State of the Art .1 Security Analysis of ARBAC .2 Security Analysis of Temporal RBAC. 24 I Security Analysis of ARBAC Policies 29 4 Our Techniques for Security Analysis of ARBAC Policies 31 4.2 User-Role Reachability Problem .3 Reachability of a Class of Symbolic Transition Systems .1 Symbolic Transition System .2 Symbolic Backward Reachability Procedure .4 Solving User-Role Rechability Problems .1 Symbolic Representation of Security Problems .2 Solving the Problem.
43 5 ASASPXL: An Implementation of Our Techniques for AR- BAC 47 5.2 Model Checking Modulo Theories and ARBAC Policies .3 MCMT’s new Clothes for Analysing ARBAC Policies .1 Useful Administrative Operations .2 Reducing the Number of Invocations to the Model Checker .3 Reusing Previously Visited States .4 Putting Things Together .1 Adaptation to Non-separate Administration Assump- tion .2 Forward Useful Actions .3 Ordering Administrative Actions .6 Discussion on the Analysis of ARBAC Policies .1 Brief Summary on VAC’s Slicer .2 Where VAC’s Slicer cannot be Used. 87 ii 6 Incremental Analysis of Evolving ARBAC Policies 89 6.2 Overview of Related Approaches .3 Incremental Analysis of Evolving ARBAC Policies .1 iBR and Filter .4 Implementation and Experiments. 105 II Security Analysis of ATRBAC Policies 107 7 Our Techniques for Security Analysis of ATRBAC Policies109 7.2 Temporal RBAC Policies and Administration .3 Solving Reachability Problems for ATRBAC Systems .4 Technique and Experiment .1 Implementation and Evaluation .1 Timed Reachability Problems .2 Three Sub-classes of ATRBAC Systems. 145 8 User-Role Reachability Problem in Policies with Temporal Hierachies 147 8.2 Access Control Schemes .3 Administrative Temporal RBAC .4 Security Mappings from ATRBACH .1 τH2F : a Temporalized Version of σH2F .3 τH2M : Multi-target Mapping .5 Implementation and Experiments.
169 9 Conclusions and Extensions 171 9. 173 Bibliography 175 iv List of Tables 5.1 Experimental results on the “complex” benchmarks in [30] 77 5.2 Experimental results on the Bank Dresden case study in [30] 78 5.3 Experimental results on the benchmarks in [19] (1) .4 Experimental results on the benchmarks in [19] (2) .5 Experimental results on the benchmarks in [65] .6 Experimental results on test cases with |Ca | > 1 .7 Experimental results when turning off heuristics in Section 5.1 Values of parameters in the experiments .2 Results on benchmark class (c) .3 Results on benchmark class (d ). 145 v List of Figures 2.1 User and Permission Assignments; and Role Hierarchies .2 The combination of actions .1 Characteristics of the 6 benchmark sets .2 Comparison of our approach with that of [23, 25] on the six benchmark sets .2 Symbolic representation of reachability problems for ATR- BAC systems (1) .3 Symbolic representation of reachability problems for ATR- BAC systems (2) .4 Our technique for solving reachability problems of ATRBAC systems .5 Results on benchmark class (a) .6 Results on benchmark class (b) .1 Results on benchmarks from [48] extended with randomly generated temporal role hierarchies .2 Behavior for increasing the depth of TRH. 168 vii Chapter 1 Introduction Modern information systems hold sensitive information, which unautho- rized users want to access in order to steal it.
The most important mecha- nism to prevent this is Access Control [17] which is thus becoming increas- ingly important for today ubiquitous systems. In general, access control policies protect the resources of the systems by controlling who has per- mission to access what objects/resources. The administration of access control policies is key to the security of many IT systems that need to evolve in rapidly changing environments and dynamically finding the best trade-off among a variety of needs. Per- missions to perform administrative actions must be restricted since security officers can only be partially trusted.
For example, a project manager can only assign works to employees managed by him. In fact, some of them may collude to, inadvertently or maliciously, modify the policies so that untrusted users can get sensitive permissions. Taking into consideration the effect of all possible sequences of administrative actions is a difficult, or even an impossible task for manual inspection. Thus, push-button analysis techniques are needed to identify safety issues, i.
administrative actions generating policies by which a user can acquire permissions that may com- promise some security goals. This is known as the safety problem [27], 1 CHAPTER 1. INTRODUCTION which amounts to establish whether there exists a (finite) sequence of ad- ministrative actions, selected from a set of available ones, that applied to a given initial policy, yield a policy in which a user gets a certain per- mission. Several important policy analysis problems can be reduced to safety problems, e., deciding if the set of users having a given permission is a sub-set of that having another permission (containment), computing the minimal sets of permissions that a user should have so as to make another policy reachable by means of a finite sequence of administrative actions (weakest preconditions), and others (see, e.
This makes automated techniques capable of solving safety problems even more valu- able to understand the subtle interplay among the actions performed by several administrators. In general, the safety problem is undecidable [28]. A first step towards the development of automated techniques is to identify classes of policies for which the safety problem is decidable. Several such techniques have been proposed for administrative models of Role-Based Access Control (RBAC) policies [53].
This is so because RBAC is one of the most widely adopted access control models in the real world. The reason for this is the fact that the notion of role allows for simplifying policy management by decomposing user-permission assignment into user-role and role-permission assignments. For example, a new employee joining an organization is as- signed to a role and this is sufficient for him/her to automatically acquire all the permissions associated to that role. Similarly, when someone is pro- moted or demoted, it is sufficient to update the roles with which he/she is associated to make available the permissions required by the new position.
The role-permission assignment rarely changes since this implies a change in the organization. These observations lead researchers to study safety problems for Administrative RBAC (ARBAC) models—the most impor- tant one is the URA97 model [52]—in which administrative actions can 2 CHAPTER 1. CONTRIBUTIONS only update the user-role assignment relation (see, e., Chapter 5, 6 for an overview). Additionally, in order to enhance the security and flexibility of the sys- tem, access control models have been extended in several dimensions in which authorizations depend also on contextual information, such as time, that are widely used in real-world applications.
For instance, two tem- poral extensions of RBAC are reported in [14, 36]. These models impose temporal constraints on roles being enabled or for them to be assigned to users. In these models, the executability of administrative actions is also re- stricted by temporal constraints. Following the works for ARBAC models, researchers continue to investigate (the extensions of) analysis techniques to cover the safety problems in the context of administrative temporal RBAC models (ATRBAC).