ABSTRACT Title of dissertation: A LOGIC-BASED FRAMEWORK FOR WEB ACCESS CONTROL POLICIES Vladimir Kolovski, Doctor of Philosophy, 2008 Dissertation directed by: Professor James Hendler Department of Computer Science With the widespread use of web services, there is a need for adequate security and privacy support to protect the sensitive information these services could provide. As a result, there has been a great interest in access control policy languages which accom- modate large, open, distributed and heterogeneous environments like the Web. XACML has emerged as a popular access control language, but because of its rich expressiveness and informal o cial semantics, it su ers from a) a lack of understanding of its formal properties, and b) a lack of automated, compile-time services that can detect errors in expressive, distributed and heterogeneous policies. In this dissertation, I present a logic-based framework for XACML that addresses the above issues. One component of the framework is a Datalog-based mapping for XACML v3.0 that provides a theoretical foundation for the language: a concise and formal semantics and complexity results for full XACML and various fragments. Addi- tionally, considering that most previous work on access control is based on some variant of Datalog, my mapping discovers close relationships between XACML and other logic based languages such as the Flexible Authorization Framework. The second component of this framework provides a practical foundation for static analysis of expressive XACML policies. The analysis services detect semantic errors or di erences between policies before they are deployed. To provide these services, I present a mapping from XACML to the Web Ontology Language (OWL), which is the standardized language for representing the semantics of information on the Web. In par- ticular, I focus on the OWL-DL sub-language, which is a logic-based fragment of OWL. Finally, to demonstrate the practicality of using OWL-DL reasoners as policy analyzers, I have implemented an OWL-based XACML analyzer and performed extensive empirical evaluation using both real world and synthetic policy sets. A LOGIC-BASED FRAMEWORK FOR WEB ACCESS CONTROL POLICIES by Vladimir Kolovski Dissertation submitted to the Faculty of the Graduate School of the University of Maryland, College Park in partial fulfillment of the requirements for the degree of Doctor of Philosophy 2008 Advisory Committee: Professor James Hendler, co-Chair Professor V.S. Subrahmanian, co-Chair Professor Jennifer Golbeck, co-Chair Professor Bruce Jacob Professor Ashok Agrawala Daniel Weitzner c Copyright by Vladimir Kolovski 2008 Dedication To my family ii Acknowledgments I would like to thank here the many people that helped me during my graduate studies at University of Maryland. First of all, I would like to thank my advisor, James Hendler, who gave me the freedom to pursue my research topic and provided me with unwavering support during my graduate studies. Thank you Jim for your guidance and encouragement. I would also like to thank Jennifer Golbeck, who de facto became my co- advisor in the latter stages of my studies. A heartfelt thanks to you Jen for your extremely useful advice on all things dissertation-related. Finishing this thesis would not have been possible without the support of Prof. Hendler and Prof. Golbeck. I would like to thank my thesis committee members: Ashok Agrawala, Daniel Weitzner, V.S. Subrahmanian and Bruce Jacob for providing valuable feedback on my dissertation. I would especially like to thank Prof. Subrahmanian, who provided me with important technical feedback after my thesis proposal that helped me narrow my research topic. My colleagues at the MINDSWAP research group helped me in every stage of my research. Above all, I would like to thank Christian Halaschek-Wiener for being a close friend and a valuable source of technical and professional advice. I would also like to thank Bijan Parsia, who pushed me in the right direction during the rockiest year of my graduate studies. I received a lot of support from the other members or my research group, including Aditya Kalyanpur, Evren Sirin, Taowei (David) Wang, Bernardo Cuenca-Grau, Yarden Katz, Hamid Haidarian-Shahri, Bin Zhao, Naiwen Lin, Ugur Kuter and others I may have forgotten. iii I would like to express my gratitude to Kendall Clark from Clark&Parsia and An- drew Schain from NASA HQ for their collaboration on developing realistic policy sets. Thank you for the numerous discussions on how to apply my research in a real-world setting. On a more personal note, I would like to thank my close friends and housemates from LagunaHouse: Dov, Arkady, AT and Matus, who made my life in Prince George?s county a lot easier and helped me immensely in finishing my thesis writing smoothly. A heartfelt thank you to my parents Metodija and Katerina for providing a caring and stimulating intellectual environment at home. Thanks to my sister Jana for always loving me, no matter how much I annoyed her. Finally, I would like to thank my fiancee Marija for providing me with endless love and support during this whole process. Thank you Marija for making College Park feel like home. iv Table of Contents List of Tables ix List of Figures xii 1 Introduction 1 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1.1 Motivation: Lack of Formal Semantics . . . . . . . . . . . . . . 3 1.1.2 Motivation: Analysis Services for Distributed Policies . . . . . . 4 1.2 Proposed Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4 Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2 Preliminaries 12 2.1 XACML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.1 Rules, Targets, Attributes and Requests . . . . . . . . . . 13 2.1.2 Combining Algorithms . . . . . . . . . . . . . . . . . . . . . . . 14 2.1.3 Administrative XACML . . . . . . . . . . . . . . . . . . . . . . 15 2.1.4 Hierarchical and Multiple Resource Profile . . . . . . . . . . . . 16 2.2 Logic Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2.1 Datalog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2.1.1 Semantics of Datalog . . . . . . . . . . . . . . . . . . 19 2.2.1.2 Negation in Datalog . . . . . . . . . . . . . . . . . . . 19 2.2.2 Description Logics . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2.2.1 Concrete Domains . . . . . . . . . . . . . . . . . . . . 24 2.2.2.2 Syntax and Semantics ofSHIQ(D) . . . . . . . . . . 25 2.2.2.3 DL Reasoning Services . . . . . . . . . . . . . . . . . 29 2.3 Semantic Web . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3 Related Work 32 3.1 Access Control Models . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.2 Access Control Languages . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.2.1 Logic-Based Languages . . . . . . . . . . . . . . . . . . . . . . 36 3.2.1.1 Centralized Policies . . . . . . . . . . . . . . . . . . . 36 3.2.1.2 Distributed Policies . . . . . . . . . . . . . . . . . . . 38 3.2.1.3 Dynamic/Temporal Access Policy Languages . . . . . 41 3.2.2 Semantic Web-Based languages . . . . . . . . . . . . . . . . . . 42 3.2.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.3 Policy Analysis and Verification . . . . . . . . . . . . . . . . . . . . . . 44 3.3.1 Embedding Policy Languages in Logic . . . . . . . . . . . . . . 50 3.3.2 XACML Analysis and Verification . . . . . . . . . . . . . . . . . 51 v 4 Operational Semantics of XACML 53 4.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.2 Proof-theoretic Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 55 4.2.1 Matching Functions . . . . . . . . . . . . . . . . . . . . . . . . 56 4.2.2 Rules, Policies, PolicySets . . . . . . . . . . . . . . . . . . . . . 59 4.2.3 Multiple Resource and Hierarchical Profile . . . . . . . . . . . . 61 4.2.4 Administrative Profile . . . . . . . . . . . . . . . . . . . . . . . 63 4.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 5 Datalog-Based Theoretical Foundation of XACML 66 5.1 Mapping XACML to Datalog . . . . . . . . . . . . . . . . . . . . . . . . 67 5.1.1 Mapping XACML policy structure to Datalog . . . . . . . . . . . 68 5.1.2 Mapping Rules, Policies and PolicySets . . . . . . . . . . . 70 5.1.2.1 Matching Requests to Rules . . . . . . . . . . . . . . . 71 5.1.2.2 Matching Requests to Policies . . . . . . . . . . . . . . 74 5.1.2.3 Matching Requests to PolicySets . . . . . . . . . . . . 77 5.1.3 Administrative Profile . . . . . . . . . . . . . . . . . . . . . . . 79 5.1.3.1 Reduction Rules . . . . . . . . . . . . . . . . . . . . . 79 5.1.3.2 Propagation Rules . . . . . . . . . . . . . . . . . . . . 80 5.1.4 Functions in XACML . . . . . . . . . . . . . . . . . . . . . . . 81 5.2 Complexity of XACML . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 5.2.1 XACML with cyclical PolicySets . . . . . . . . . . . . . . . . 82 5.2.2 Tractable Fragments . . . . . . . . . . . . . . . . . . . . . . . . 87 5.3 XACML and Logic-Based Languages . . . . . . . . . . . . . . . . . . . 89 6 XACML Analysis Services 94 6.1 Mapping XACML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 6.1.1 Mapping Requests . . . . . . . . . . . . . . . . . . . . . . . . 97 6.1.2 Mapping Target . . . . . . . . . . . . . . . . . . . . . . . . . . 99 6.1.3 Mapping XACML Rules . . . . . . . . . . . . . . . . . . . . . 103 6.1.4 Mapping Policies . . . . . . . . . . . . . . . . . . . . . . . . 106 6.1.5 Mapping PolicySets . . . . . . . . . . . . . . . . . . . . . . . 111 6.1.6 Mapping Administrative XACML . . . . . . . . . . . . . . . . . 113 6.1.6.1 Extending the XACML Mapping . . . . . . . . . . . . 115 6.1.7 XACML Datatypes and Functions . . . . . . . . . . . . . . . . . 116 6.1.7.1 AttributeSelector . . . . . . . . . . . . . . . . . . . . . 119 6.2 Services . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.2.1 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.2.1.1 Tracing . . . . . . . . . . . . . . . . . . . . . . . . . . 123 6.2.2 Policy Comparison . . . . . . . . . . . . . . . . . . . . . . . . . 124 6.2.3 Redundancy Checking . . . . . . . . . . . . . . . . . . . . . . . 127 6.3 Analyzing Heterogeneous XACML Policies . . . . . . . . . . . . . . . . 129 6.3.1 Representing Policy Idioms . . . . . . . . . . . . . . . . . . . . 131 6.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 vi 7 Formalizing and Analyzing Web Service Policies 135 7.1 WS-Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 7.1.1 Mapping WS-Policy Operators to OWL-DL . . . . . . . . . . . . 137 7.1.2 Mapping Policy Assertions to OWL . . . . . . . . . . . . . . . . 141 7.1.3 WS-Policy Merge and Intersection . . . . . . . . . . . . . . . . . 142 7.1.4 Policy Processing . . . . . . . . . . . . . . . . . . . . . . . . . . 143 7.2 WS-XACML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 7.2.1 Syntax of WS-XACML . . . . . . . . . . . . . . . . . . . . . . 145 7.2.2 Semantics of WS-XACML . . . . . . . . . . . . . . . . . . . . . 147 7.2.2.1 Matching Constraints . . . . . . . . . . . . . . . . . . 148 7.2.3 Mapping WS-XACML . . . . . . . . . . . . . . . . . . . . . . . 150 7.2.3.1 Mapping Constraints . . . . . . . . . . . . . . . . . 151 7.2.3.2 Analysis Services . . . . . . . . . . . . . . . . . . . . 152 7.3 Putting it All Together . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 7.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 8 Implementation and Evaluation 157 8.1 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 8.2 Policy Test Suite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 8.2.1 Formal Verification Results . . . . . . . . . . . . . . . . . . . . . 163 8.2.2 Policy Comparison Results . . . . . . . . . . . . . . . . . . . . . 164 8.2.3 Redundancy Checking Results . . . . . . . . . . . . . . . . . . . 166 8.2.4 Extended Policies . . . . . . . . . . . . . . . . . . . . . . . . . . 167 8.2.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 8.3 NASA Federated Data Access Use Case . . . . . . . . . . . . . . . . . . 170 8.3.1 BIANCA Policy Set . . . . . . . . . . . . . . . . . . . . . . . . 172 8.3.2 Empirical Results . . . . . . . . . . . . . . . . . . . . . . . . . . 173 8.4 Healthcare Access Policy . . . . . . . . . . . . . . . . . . . . . . . . . . 174 8.4.1 Background: HL7 and Electronic Health Records . . . . . . . . . 176 8.4.2 HL7 RBAC Policy . . . . . . . . . . . . . . . . . . . . . . . . . 177 8.4.3 Converting HL7-RBAC to XACML . . . . . . . . . . . . . . . . 178 8.4.4 Empirical Results . . . . . . . . . . . . . . . . . . . . . . . . . . 179 8.4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181 8.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182 9 Conclusions and Future Work 183 9.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 9.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 9.2.1 Theoretical Framework . . . . . . . . . . . . . . . . . . . . . . . 185 9.2.1.1 Dynamic Environment and Obligations . . . . . . . . . 185 9.2.1.2 Extensions of XACML . . . . . . . . . . . . . . . . . 186 9.2.2 Analysis Services . . . . . . . . . . . . . . . . . . . . . . . . . . 187 9.2.2.1 Computing All Di erences between Policies . . . . . . 187 9.2.2.2 Policy Repair . . . . . . . . . . . . . . . . . . . . . . 188 9.2.2.3 Extending and Evaluating Redundancy Checking . . . 190 vii 9.2.3 Analyzing Business Rules . . . . . . . . . . . . . . . . . . . . . 191 A Proofs 192 Bibliography 232 viii List of Tables 2.1 Interpretations ofSHIQ(D) Concepts and Roles . . . . . . . . . . . . . 28 2.2 Interpretations ofSHIQ(D) Axioms . . . . . . . . . . . . . . . . . . . 28 4.1 Syntax of Policy Elements. . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.2 Syntax of Targets and Matching Functions. . . . . . . . . . . . . . . . 54 4.3 Syntax of Condition element. . . . . . . . . . . . . . . . . . . . . . . . 55 4.4 Syntax of access requests. ARQ represents an administrative request (a special case of access requests). . . . . . . . . . . . . . . . . . . . . . . 55 4.5 Matching AttributeDesignator and AttributeSelector with at- tributes in Request. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.6 Matching a Request(RQ) with a Target(T). . . . . . . . . . . . . . . . 58 4.7 Evaluating a Rule against a Request. . . . . . . . . . . . . . . . . . . . . 58 4.8 -Overrides Rule Combining Algorithm. stands for Permit or Deny, and ? for the opposite. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 4.9 First-Applicable Rule Combining Algorithms. . . . . . . . . . . . . . . . 60 4.10 Only-One-Applicable Rule Overriding Algorithm. . . . . . . . . . . . . . 61 4.11 Permit-Overrides and Deny-Overrides Policy Combining Algorithms. . . 62 4.12 Generic Indeterminate rule for policies and rules. . . . . . . . . . . . 62 4.13 Reduction Rules. stands for a Permit or Deny. . . . . . . . . . . . . . 64 4.14 Propagation Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 5.1 Matching a request (?RQ) against an AttributeDesignator (?AD) in Datalog. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 5.2 Matching a request (?RQ) against a target (?T) in Datalog. . . . . . . . . 73 5.3 Matching a Request (?RQ) against a Rule (?R) in Datalog. . . . . . . . 73 5.4 Correspondence of Natural Deduction rules and Datalog rules for XACML request matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 ix 5.5 Strata ordering ofPR. . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 5.6 Mapping Permit- and Deny-Overrides rule-combining algorithm to Datalog. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 5.7 Mapping First-Applicable rule-combining algorithm to Datalog. . . . 75 5.8 Representation of Only-One-Applicable rule-combining algorithm in Datalog. stands for either a Permit or Deny. . . . . . . . . . . . . . . . 76 5.9 Correspondence of operational semantics and Datalog rules for XACML policy matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 5.10 Strata ofPR[PP. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 5.11 Representation of Permit- and Deny-Overrides policy combining al- gorithms in Datalog. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 5.12 Datalog version of reduction rules in XACML 3.0. . . . . . . . . . . . . 79 5.13 Rules to generate edges in reduction graph. . . . . . . . . . . . . . . . . 80 5.14 Authorization rules for access decision in reduction graph. . . . . . . . . 80 5.15 Representing a clause consisting of three variables with a XACML policy structure. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 6.1 Mapping Request to a DL concept expression . . . . . . . . . . . . . . 98 6.2 Mapping access requests that match Target to a DL concept expression . 101 6.3 Mapping access requests that return Indeterminate when matched against Target to a DL concept expression . . . . . . . . . . . . . . . . . . . . 101 6.4 Mapping matching functions. . . . . . . . . . . . . . . . . . . . . . . . . 118 6.5 Predicates supported by Racer (table taken from RacerPro user guide [82]).118 6.6 Mappings of Common Types of Policy Tests. T refers to the test pol- icy (containing the security property) and P refers to the top level policy set. Property holds if and only if the entailment holds, i.e., the concept expression is not satisfiable. . . . . . . . . . . . . . . . . . . . . . . . . 123 7.1 Mapping of WS-Policy Constructs to OWL . . . . . . . . . . . . . . . . 139 7.2 Syntax of Web Service Profile of XACML. . . . . . . . . . . . . . . . . 145 x 7.3 Matching Requirements with Capabilities. . . . . . . . . . . . . . . 148 7.4 Matching XACML Assertions. . . . . . . . . . . . . . . . . . . . . . . . 149 7.5 Mapping matching functions. . . . . . . . . . . . . . . . . . . . . . . . . 152 7.6 Mapping Constraint functions. . . . . . . . . . . . . . . . . . . . . . . 153 8.1 General Information on Policies in Test Suite. . . . . . . . . . . . . . . . 162 8.2 Fragment of BIANCA Policy Set. . . . . . . . . . . . . . . . . . . . . . 172 xi List of Figures 1.1 Example Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 6.1 Example Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 6.2 Updated Policy (with LeadDev role) . . . . . . . . . . . . . . . . . . . . 125 7.1 Example policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140 7.2 Example policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 8.1 Architecture of Analysis Framework. . . . . . . . . . . . . . . . . . . . . 158 8.2 Sample Output of Formal Verification Service. . . . . . . . . . . . . . . . 160 8.3 Verification results for OWL-DL-based, HSAT and Margrave. Times shown are for formal verification of security properties. Top left figure contains the time for parsing the XACML policy and loading/converting into the appropriate structure (BDD, conjunctive formula, OWL-DL on- tology). The top right figure contains the verification time, once the struc- ture is converted. Bottom figure contains aggregate (loading+verification) timings. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 8.4 Policy comparison results for OWL-DL-based, SAT and Margrave. Times shown are for checking policy equivalence. The figure contains the aggregate (loading+comparing) timings. . . . . . . . . . . . . . . . . 166 8.5 Checking redundancy of Rule, Policy and PolicySets. Times shown are aggregate (loading the policy, converting it to OWL-DL form and pro- cessing each policy element). . . . . . . . . . . . . . . . . . . . . . . . . 167 8.6 Testing the policy analyzers on an extended version of Continue. con- tinuex1 refers to the original version of the policy, continuexn denotes a policy that is n times large than the original. The Y-axis denotes the total time needed to load the policy and verify all 11 security properties. . . . . 169 8.7 Testing the policy analyzers on an extended version of Fedora. fedo- rax1 refers to the original version of the policy and fedoraxn denotes a policy that is n times large than the original. The Y-axis denotes the total time needed to load the policy and verify 5 randomly generated security properties. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 xii 8.8 Analysis time for the Personally Identifiable Information Query on various policies addressing the NASA HQ federated data access use case. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174 8.9 Analysis time for the Policy Comparison (compliance) query on var- ious policies addressing the NASA HQ federated data access use case. 175 8.10 Analysis time for the Policy Disjointness Query on various policies addressing the NASA HQ federated data access use case. . . . . . . . 175 8.11 Formal Verification of HL7 policy. Please note that HL7x1 refers to the original policy whereas HL7xn refers to a meta-policy containing n policies of the same size and structure as HL7. . . . . . . . . . . . . . . 180 8.12 Policy Comparison timings for HL7 policy. Please note that HL7x1 refers to the original policy whereas HL7xn refers to a meta-policy con- taining n policies of the same size and structure as HL7. . . . . . . . . . . 181 9.1 Example Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 xiii Chapter 1 Introduction 1.1 Motivation With the ever-increasing amount of data being made accessible on the Web, there is a corresponding increasing need for information publishers and data owners to control access to sensitive segments of their data. While access control specification and manage- ment has been an active field for more than 30 years1, applying these security mechanisms in an open, distributed and heterogeneous environment like the World Wide Web (or the enterprise) presents novel challenges. For example, an access control language for such distributed environment should be powerful and flexible enough to express many di er- ent types of security policies (e.g., mandatory, discretionary and role-based access control policies) and support various datatype functions. In such an environment the resources that are being protected might be distributed, but also the policy specifications themselves could be also distributed, so a mechanism for references among policies and policy inte- gration is needed. There has been great interest coming from industry and academia in developing an expressive access control policy language for open, heterogeneous and distributed envi- ronments that can cover the above access control requirements [113, 15, 27, 87, 34, 72, 128]. To facilitate interoperability, there has been a strong push (mostly by enterprise 1One of the seminal papers on secure computer systems (by Bell and LaPadula) was published in 1973[28]. 1 application providers like Oracle and SAP) to standardize one of the proposed security languages. The eXtensible Access Control Markup Language (XACML [113]) has emerged as the language preferred by most leading enterprise application providers: it was standard- ized by OASIS in 2003. XACML was originally developed by Sun Microsystems and has gained momentum over the years: it is currently deployed or supported by more than 65 systems and projects [16]. The language has also attracted academic attention ? there are more than 200 peer-reviewed papers published on XACML since 2003 [16]. XACML is a declarative access control language with a variety of features: it allows for distributed policies and resources, it supports attribute-based (as opposed to identity- based) access control, negative authorization (Deny policies), conflict resolution algo- rithms to integrate distributed policies and role-based access control (RBAC). Moreover, the language has more than 200 built-in functions that range from data-type comparison and conversion to boolean functions and even some with higher order flavor. The lan- guage is based on XML and specifies a processing model for checking policy compliance at run time. As an example, following is a XACML rule which returns a Permit only when the value of the action-id attribute is read. read 2 1.1.1 Motivation: Lack of Formal Semantics The specification of XACML v1.0 was published in 2003, and since then there has been continuing work on the standard. As of March 2008, XACML v3.0[113], which in- cludes delegation policies, is close to standardization. During this time, the OASIS work- ing group developing XACML has not yet provided a formal semantics for the language ? the o cial semantics of XACML is given informally, in normative documents. Pre- vious academic e orts [68] that formalized early versions of XACML notwithstanding, currently there is no formal semantics that covers XACML 3.0 and includes the profiles that are part of its latest version: delegation policies [114] and Web Service access control policies (WS-XACML)[19]. One consequence of the lack of a formal treatment is that the computational com- plexity properties of the language are still unknown. For example, consider access request checking, the main service the XACML processing model provides: given an access re- quest R and a policy P, determine the access decision of P for R2. Given the rich set of features of XACML, its verbose specifications, and its lack of a formal treatment, it is still unknown if access request checking is tractable. A formal, declarative semantics would also shed light on the relationship between XACML and previous work on languages for distributed access control policies. Even before work on XACML began, there were numerous policy language proposals coming 2XACML supports Permit, Deny, Indeterminate (for errors) and NotApplicable as access deci- sion. 3 from both academia and industry [87, 32, 27, 72, 12]. While there have been some at- tempts to compare XACML to its closest competitors from industry (e.g., EPAL [15]), there has been no in-depth comparison with formal security languages such as the Flexi- ble Authorization Framework [72], Delegation Logic [87] or SecPal [27]. Most of these academic policy languages have a formal foundation (usually logic-based) and tractable (polynomial) complexity. From an academic viewpoint, a logic-based semantics for XACML would help us understand where the language fits in (in terms of expressive- ness and computational complexity) in the active research field of access control policy specification. If it can be shown that XACML is close to some of these languages, then from a practical perspective, these similarities could provide possible areas of improve- ment for XACML itself by adding features available in other languages. 1.1.2 Motivation: Analysis Services for Distributed Policies Due to the expressiveness of XACML and its lack of ?compile time? support, it is non-trivial for a policy developer to understand the overall e ect and consequences of the XACML policies he/she writes. Even arguably the most important feature in access control - checking that the policy will not result in leakage of permissions to an unintended or unauthorized principal, i.e., safety - is di cult (if not impossible) to do manually. For example, incomplete security policies might unintentionally give access to an intruder. How can a security administrator be certain that her policy covers all possible corner cases? Even if the administrator does discover a bug in the policy, and fixes it accordingly, the consequences of that fix (policy change) are di cult to analyze. 4 One approach for verifying correctness of policies is to perform testing [98], where a test case for a policy would consist of an access request and expected outcome (Permit, Deny, NotApplicable or Indeterminate). However, testing is not exhaustive and it is di cult to think of all possible scenarios that need to be tested. To illustrate the limitations of testing, consider the following example. In this sce- nario, there are only two roles: Manager and Developer, one resource: Report, and two actions: read, write. The main (root) policy contains two policies which are combined us- ing First-Applicable combining algorithm. First-Applicable is a XACML com- bining algorithm that, given a set of policies, returns the decision of the first policy that is successfully applied while ignoring the decisions of the subsequent policies. In the exam- ple below, if P1 returns a decision (Permit or Deny), this decision would be propagated to the parent policy PS 1 without taking into account the decision of PS 2. The policy is presented in graphical form in Figure 1.1. Figure 1.1: Example Policy 5 In this example, a security administrator could specify a test condition for this pol- icy in the form of a XACML access request, ?Developer requests write access to report?, and the expected outcome, Deny. Testing policies in such manner is not exhaustive, since it is di cult to think of all possible conditions that need to be tested. In this particular ex- ample, the simple test would pass, since the Deny rule R3 would fire, however the policy would be still vulnerable. Consider what happens if a user tries to both read and write to File as part of the same access request. In this case, rule R2 will fire as well, thus the policy set would return a Permit. Essentially, this policy allows an invalid request (a write+read request) to piggyback on top of a valid one (read request). Violations such as above will not necessarily be caught by simple testing. For this purpose, techniques such as formal verification of a policy against security properties have been investigated in literature [67, 74, 50, 131]. Formal verification explores all possible combinations of attributes in a policy in an attempt to break the security property, so it would catch the security error in the above example. The above examples illustrated the benefits of formal verification of policies, and there has been some interest in providing such services for XACML [50, 66, 131]. How- ever, the analysis approaches of previous work do not capture more expressive language features needed for the type of heterogeneous and distributed environments that XACML is intended to be deployed in. These features include: Data-types and functions. XACML supports all of the XML Schema Datatypes and in addition it defines four datatypes of its own: ipAddress, x500Name, rfc- 822Name and dnsName. The language supports a powerful set of more than 200 6 functions that make use of these datatypes: from data-type matching functions (e.g., string-equal, date-time-greater-than) to boolean and set operations and functions with higher order flavor (i.e., functions that operate on other functions). Heterogeneous policies. There has also been interest in extending XACML with expressive policy descriptions and support for data integration, for the purpose of federated access control management. Consider what happens when access con- trol is federated across multiple, independent organizations. These organizations might use di erent attribute schemes to describe subjects, actions and resources. For example, in an e-commerce scenario, an online book store might use a boolean attribute adultAge to represent adult customers, whereas a video rental store might use an integer attribute age. In a large enterprise with many di erent departments where each department potentially has a di erent attribute scheme, integrating and reasoning about such heterogeneous security information is a challenging problem. Delegation policies. XACML allows users to specify delegation policies in addi- tion to access policies. Delegation policies can specify which users have rights to add access policies: ?HR-Admins can create policies concerning the Payroll servers? , or can be used for delegation as well: ?Jack can approve expenses while Mary is on vacation?. In previous work, there exists no formal analysis framework that can reason about XACML policies with the above features. 7 1.2 Proposed Solution This dissertation presents a theoretical and practical foundation for analysis of ex- pressive XACML policies. The theoretical component presents a formal, proof-theoretic semantics for XACML 3.0 based on natural deduction rules. The semantics covers the core of XACML along with its Delegation and Web Service Policies Profile, and repre- sents a concise and unambiguous version of the informal semantics given in the language specification. To determine XACML?s complexity properties, I provide a translation of various subsets of the language to variants of the rule-based language Datalog, thus es- tablishing its polynomial data complexity and close relationship to other logic-based lan- guages such as the Flexible Authorization Framework [73]. Additionally, I show that access request checking in XACML with arbitrary references between policies is NP- complete. The practical component of this thesis presents a logic-based analysis framework that can reason about administrative and heterogeneous XACML policies. The analysis support is done at compile-time and enables discovery of semantic errors or di erences between policies before they are deployed. One of the goals of this dissertation is to provide these analysis services while hiding the details of the logic formalism used and the internals of the analysis tool. To accomplish this, I allow users to specify security properties in XACML and present the verification results back in XACML. In addition to verification, the analysis framework also provides policy comparison (including checking for subsumption and compatibility/disjointness), and detecting redundant (?dead?) poli- cies. 8 As a basis for the practical analysis framework, I use Description Logics (DL), which are a family of formalisms that are decidable subsets of First-Order logic, and are the formal basis for the Web Ontology Language(OWL3) [45]. Because of the correspon- dence of policy analysis services to DL reasoning services (e.g., policy comparison can be reduced to concept subsumption, whereas formal verification can be reduced to con- cept satisfiability), my framework can leverage o -the-shelf DL reasoners optimized to provide the above-mentioned analysis services. An important benefit of using a logic compatible with OWL is that I can leverage OWL being a W3C standard for representing and integrating information on the Web. Thus, the analysis framework has built-in support for representing expressive vocabulary domains for policies (as OWL ontologies), so it is able to reason about heterogeneous XACML policies distributed across the enterprise (or the Web). To evaluate the practicality of my approach, I implemented the framework as a XACML analysis tool that reduces policy analysis services to DL reasoning tasks. I per- formed empirical evaluations using real-world XACML policies, testing the performance of my approach against other scalable XACML analyzers. Additionally, to fully evaluate the expressive features of the analysis framework, including support for information inte- gration across heterogeneous policies, I used two real-world policy use cases: the NASA Federated Data Access use case[118] and an RBAC policy from the healthcare domain [62] (the policy is part of the Health Level 7 standard). Considering the size and com- plexity of both of these real-world policies, my empirical evaluation shows the approach 3OWL has three subsets: OWL-Lite, OWL-DL and OWL Full, the first two of which are grounded in description logics. From now on, I will use OWL to refer to the OWL-DL sublanguage. 9 is practical for large and expressive XACML policy sets. 1.3 Contributions The contributions of this thesis are as follows: A formal, proof-theoretic semantics of XACML v3.0 that covers the core specifi- cation and the Administrative Policy Profile. The semantics is given using natural deduction rules. A mapping of XACML to Datalog that provides a model-theoretic semantics and computational complexity results for full XACML and various fragments. Addi- tionally, an extensive comparison with other logic-based languages such as Flexible Authorization Framework [73] based on the Datalog mapping. A static analysis framework based on OWL-DL that can reason about expressive XACML policies. A comprehensive set of services are provided with this mapping: formal verification, policy comparison (change analysis) and redundancy checking. Demonstration that the analysis framework is applicable to other domains. This was accomplished by formalizing and analyzing the W3C standard language for web service policies (WS-Policy [129]) . An empirical evaluation of the scalability of the analysis framework. The evaluation demonstrates the scalability of the analysis framework using real-world policies: a XACML policy test suite consisting of policies used to evaluate other XACML 10 analyzers, as well as datasets from two real-world use cases for expressive policies (NASA HQ data access and healthcare RBAC policies). 1.4 Organization This thesis is organized as follows: Chapter 2 introduces background information and necessary preliminaries needed to understand the technical contributions of the dis- sertation. Chapter 3 surveys related work to this dissertation, namely: access control policy models and languages, and policy analysis and verification approaches. In Chapter 4 a formal, proof-theoretic semantics for XACML 3.0 is presented using natural deduc- tion rules. Chapter 4 also provides a translation of various subsets of the language to locally stratified Datalog, thus establishing its polynomial data complexity and close re- lationship to other logic-based access control languages. Chapter 5 presents an analysis approach that can reason about both distributed and heterogeneous XACML policies. In particular, I show how with a mapping to description logics (DL), we can perform change analysis, formal verification, and coverage checking for XACML policies. An application of the formal framework to other domains is presented in Chapter 6. In particular, WS- Policy (a web services policy language) is formalized and analyzed in a similar fashion to XACML. In Chapter 7, I present my prototype implementation of a XACML-to-DL mapper and policy analyzer. I have performed an extensive empirical evaluation to de- termine if DL reasoners are suitable as policy analyzers; the results of the evaluation are also presented in Chapter 7. Finally, Chapter 8 presents concluding remarks as well as possible areas of future work. 11 Chapter 2 Preliminaries In this chapter, I present background information on the language that is the focus of this dissertation: XACML, and on the logical formalisms used to analyze XACML, namely: Datalog and Description Logics. The purpose is to present the basic concepts, terminology and definitions that are used throughout this thesis. 2.1 XACML The eXtensible Access Control Markup Language (XACML [113]) is a standard- ized, expressive and increasingly popular XML-based language for writing access control policies about distributed resources. Before I discuss the syntax of XACML policies, I present a brief overview of the high level XACML policy model. Essentially, there are two high level components of a XACML-enabled system. A PDP, or Policy Decision Point, is the processing engine that evaluates access requests against XACML policies. A PEP, or Policy Enforcement Point, is the application-specific element that physically enforces access to a resource. The PEP generates the access requests to be sent to the PDP and enforces the access decisions made by the PDP. The focus of my dissertation is on how policy decisions are made (not enforced), so the discussion from now on will be mostly regarding the PDP. At the root of all XACML policies is a Policy or a PolicySet. A PolicySet is a 12 container that can hold other Policies or PolicySets, as well as references to policies found in remote locations. A Policy represents a single access control policy, expressed through a set of Rules. Each XACML policy document contains exactly one Policy or PolicySet root element. Following, an explanation of the basic elements of XACML (Rules, Targets and Attributes) is provided and then more advanced features of the language are discussed. 2.1.1 Rules, Targets, Attributes and Requests Rule is the most basic policy element of XACML that actually makes an access decision. Essentially, a Rule is a function that takes an access request as input and yields a Permit, Deny or Not-Applicable. To determine if a Rule is applicable to an access request, the Target element is used. The Target defines the set of requests to which the rule is intended to apply in the form of a logical expression on attributes in the request. Target is comprised of a conjunction of DisjunctiveMatch elements, where each DisjunctiveMatch contains a set of ConjunctiveMatch elements. Finally, each ConjunctiveMatch contains a list of attributes and values. Attributes are the atomic unit in XACML. They represent characteristics of the subjects, resources, actions or the environment where the access request was made. For example, a user?s role, their name, the file they want to access and the current date are all attribute values. Access requests in XACML are represented as a set of attribute-value pairs. Each attribute can belong to a category - the most common categories in XACML 13 are Subject, Resource, Action and Environment1. An example of a rule that returns Deny for access requests that have value read for action-type attribute is given below: read 2.1.2 Combining Algorithms Because a Policy or PolicySet may contain multiple policies or Rules, each of which may evaluate to di erent access control decisions, XACML a mechanism to com- bine access decisions. This is accomplished using a collection of combining algorithms, where each algorithm represents a di erent way of combining multiple access decisions into a single one. Following is a list of the most common combining algorithms: Permit-overrides. If any rule evaluates to Permit, then the combined decision is also Permit. Deny-overrides. If any rule evaluates to Deny, then the combined decision is also Deny. 1The full names of these categories consist of a lenghty prefix, e.g., urn:oasis:names:tc:xacml:- 3.0:attribute-category:Action. For clarity, I use shortened names in this dissertation. 14 First-applicable. The e ect of the first rule that applies is the decision of the policy. The rules must be evaluated in the order that they are listed. Only-one-applicable. If more than one rule is applicable, return Indetermina- te. Otherwise return the access decision of the applicable rule. In this dissertation, I use the following notation: for a XACML policy element P, I refer to its Target, Effect (in cases of Rules), its ordered list of children policy elements, its parent policy element and combining algorithm using P:target, P:e f f ect, P:children, P:parent, P:comb respectively. P:pos is used to refer to the position of P w.r.t its sibling policy elements. 2.1.3 Administrative XACML So far, I have only been discussing XACML access policies, i.e., policies that spec- ify the situations under which users are granted or denied access to a resource. However, XACML 3.0 also supports administrative (or delegation) policies, which essentially are policies that authorize access policies. For example, an administrative policy might state that members of group Clinicians are allowed to write access policies about PatientRe- ports. This section described the basic elements of an administrative policy. Policy Issuers and Delegates A policy in XACML can contain a PolicyIssuer ele- ment that describes the source of the policy. A special form of the PolicyIssuer el- ement, called the trusted issuer, is used to specify that a policy is trusted by the Policy Decision Point (PDP). A missing PolicyIssuer element is shorthand for the trusted 15 issuer. In previous versions of XACML with only access policies, the PolicyIssuer element is missing and all access policies are trusted (authorized) by default. If a policy?s issuer is not trusted, then the policies has to be authorized by using available administra- tive policies. The Delegate element of the administrative policy is used for matching against other policies. Essentially, if the Delegate of policy A matches the PolicyIssuer of policy B, that means that A can authorize policy B. When an administrative policy authorizes an access policy, it can also specify under which conditions the access policy is authorized. This is called a constrained situation in [114], and is analogous to the Target attribute in access policies. 2.1.4 Hierarchical and Multiple Resource Profile The policy evaluation performed by a XACML PDP is defined in terms of a single requested resource, with the authorization decision contained in a single Result element in the response. However, A Policy Enforcement Point, or PEP, may wish to submit a single request context for access to multiple resources, and may wish to obtain a sin- gle response context that contains a separate authorization decision (Result) for each requested resource. Such a request context might be used to avoid sending multiple de- cision request messages between a PEP and PDP, for example. Alternatively, a PEP may wish to submit a single request context for all the nodes in a hierarchy, and may wish to obtain a single authorization decision that indicates whether access is permitted to all of the requested nodes. 16 The Multiple Resource Profile provides a mechanism such that a PEP can request authorization decisions for multiple resources in a single request context. It is important to note that the Multiple Resource Profile does not a ect the policy itself. It deals with the XACML Access Requests, introducing syntactic shorthand so that multiple requests contexts can be merged into one. The Hierarchical Resource Profile[18] allows users to specify one policy that ap- plies to an entire subtree of a hierarchy, rather than having to specify a separate policy for each node of the subtree. In this Profile, a resource organized as a hierarchy may be a with a single root (tree) or multiple roots (forest), however cycles are not allowed. The nodes in a hierarchical resource are treated as individual resources. An authorization decision that permits (or denies) access to an interior node does not imply that access to its descendant nodes is permitted (or denied). 2.2 Logic Preliminaries 2.2.1 Datalog Datalog [111] is a logical language typically used to specify facts, rules and queries in deductive databases (i.e, databases that can infer information based on existing facts and rules). The basic building blocks of Datalog are the following: term can be either a constant or a variable (variables are denoted with a starting ???) atom ? is of the form Pi(t1;:::;tk) where Pi is a predicate symbol and ti are terms. 17 Given an atom A, a literal stands for A or:A. S(P) denotes the set of all predicate symbols in the datalog program P. fact ? assertion about a relevant piece of the world. Facts are expressed using literals that do not have any variable terms. For example, ?Vlad is enrolled at University of Maryland? can be expressed as enrolled(Vlad;UniversityMaryland) rule ? logical sentence that allows us to infer facts from other facts. For example, ?If X is enrolled at a university, then X is a student? is a rule. The following Prolog-like syntax will be used to describe rules: H :- B1;:::;Bn where H and Bi are literals. H represents the head of the Datalog rule and B1;:::;Bn the body literals. Given this, the rule example above can be written as: student(?X) :- enrolled(?X;?Y);university(?Y) A predicate that occurs in the head of some rule is called an IDB (intensional database) predicate, while all other predicates are called extensional (EDB). The pred- icates occurring in the body can be either intensional or extensional. Datalog can be considered as a special case of general logic programming, since it imposes the following conditions on logic programs: Safety condition: each variable that occurs in the head of a rule must also occur in 18 the body of the same rule. This condition guarantees that the set of all facts that can be derived from a Datalog program is finite. Datalog does not allow nesting of terms terms (i.e., no function symbols). For example, terms such as F(G(?x)) are not allowed. 2.2.1.1 Semantics of Datalog The Herbrand Base HB of a Datalog program P is the set of all facts (ground atoms) defined over the predicates inS(P). A Herbrand interpretationMis simply a subset of the Herbrand Base HB, which contains all of the ground facts that are true underM. A Datalog rule of the form H0 : B1;:::;Bn is true underMi for each substitution which replaces variables by constants, whenever (B1);:::; (Bn) 2M, then it also holds that (H0)2M. A Herbrand interpretation where all of the rules and clauses in a program are true is called a Herbrand model for the program P. A modelMis minimal if no subset ofMis a model for P. Assuming P is finite and there is no negation of IDB predicates, then there exists a unique minimal Herbrand model, which represents the meaning of the program P. 2.2.1.2 Negation in Datalog In positive Datalog, negated literals are not allowed in heads or bodies of rules. However, by adopting the Closed World Assumption (CWA) it is still possible to infer negative facts from a set of positive Datalog clauses. CWA states that if we cannot infer a 19 fact from a set of Datalog rules, then we infer the negation of that fact. Adding unrestricted negation in rule bodies produces more complicated seman- tics for the datalog program. Consider the following program consisting of one rule Pa = fstudent(John) :- :pro f essor(John)g. Pa has two minimal Herbrand models M1 = fstudent(John)g and M2 = fpro f essor(John)g. Having multiple minimal mod- els produces more complicated semantics, since it is unclear which one of these models should be chosen during query answering (it also increases the computational complexity of the language). To retain the unique minimal model property, there is a version of Datalog called stratified Datalog that allows a restricted form of negation. The intuition behind it is as follows: when evaluating a rule with one or more negative literals in the body, first evaluate the predicates corresponding to these negative literals. To evaluate these negative literals, we might need to evaluate additional rules that can have negative body literals as well, so we have to make sure that the program will allow such step-by-step evaluation without running into a cycle. Datalog programs that allow such evaluation are called stratified. Definition 1 Stratified Datalog. A Datalog program is called stratified if there is a parti- tion P = P1[:::[PN such that the following conditions hold for i = 1;2;:::;n: 1. Each IDB predicate in P has all of its defining rules (i.e., rules where the predicate occurs in the head) in one partition of P, 2. Each partition Pi contains only rules where the negative literals correspond to pred- icates defined in partitions Pj where j < i. 20 Each partition Pi is called a stratum of P. The level of a predicate symbol is the index of the strata within which it is defined. Query answering in positive and stratified Datalog has polynomial data complexity, whereas Datalog with unrestricted negation is data complete for co-NP [44] under the stable model semantics [54]. 2.2.2 Description Logics Description Logics (DL) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally well-understood manner [22]. The name comes from the facts that, on the one hand, the application domains are described using concept descriptions and, on the other hand, they possess formal, logic-based semantics which can be given by a translation into first-order logic (FOL). Each DL consists of the following building blocks: atomic concepts, atomic roles and individuals. Atomic concepts correspond to unary predicates in FOL (e.g., S tudent(x)), atomic roles correspond to binary predicates in FOL (e.g., enrolledIn(x;y)) and individu- als represent constant terms in FOL. Atomic concepts and roles are elementary descriptions of objects; complex ones can be built on top of them using DL constructors. For example, applying a concept dis- junction constructor (t) on the atomic concepts Male and Female, we retrieve the set of all individuals who are either Male or Female: MaletFemale. In addition to disjunction, DLs typically provide the standard boolean operators as constructors: concept conjunc- 21 tion (u) and concept negation (:). Most DLs also provide a restricted quantification, in terms of universal and existential restrictions on roles. There are many other additional concept and role constructors; they will be discussed in Section 2.2.2.2. In addition to constructors that allow us to form complex concepts and roles, a DL also provides means for expressing axioms (logical relations) involving concepts and roles. For example, we can specify concept inclusion of the form S tudent v Person stating that every student is a person, and role inclusion such as isBrother v isRelated stating that if two individuals are brothers, that implies that they are related. DL knowledge bases (KB) typically consists of the following components: A TBox containing intensional knowledge (axioms and concepts) in the form of a terminology. The axioms in the TBox are concept inclusions of the form C1 v C2 where C1 and C2 are concepts (not necessarily atomic). An RBox containing role inclusion axioms of the form R1 v R2 where R1 and R2 are DL Roles. An ABox containing extensional knowledge about the individuals in the domain. Axioms in the ABox are of the form C(a), called concept (or type) assertions and R(a,b), called role assertions, where a,b are individual names, R is a role and C is a concept. There are di erent types of TBoxes depending on the nature of the concepts occur in their axioms. The simplest TBox type consists of a restricted form of concept inclusion axioms called concept definitions: sentences of the form A v C or A C, where A is atomic. Restricting a TBox to concept definitions which are both unique (each atomic 22 concept occurs only once on the LHS of an inclusion axiom) and acyclic (the RHS of an axiom cannot refer, directly or indirectly, to the concept in the LHS) yields a definitorial TBox. On the other hand, if a TBox contains axioms of the form C v D where C is non-atomic, then the axiom is called a general concept inclusion axiom (GCI) and the TBox is called a general TBox. The distinction between definitorial and general TBoxes is important since a definitorial TBox greatly reduces reasoning complexity. A very common example of DL concept constructors often referred to in this thesis are DL number restrictions. The most expressive form is qualified number restrictions, which allow building of the concepts nR:C and nR:C from a role R, a natural number n and a concept C. For example, qualified number restrictions can be used to represent a father of exactly two sons: Maleu 2hasChild:Maleu 2hasChild:Male A more restricted form are unqualified number restrictions ? these do not allow to specify a what kind of concept is used as role filler in the restriction. For example, unqualified number restrictions can be used to denote a father of exactly two children: Maleu 2hasChildu 2hasChild Finally, a very important feature of DL for the purpose of this thesis is their datatype support, i.e., support for describing concepts using numbers, strings, regular expressions, IP addresses, etc. The main approach is to provide DLs with an interface to concrete 23 domains, together with a set of built-in predicates which are associated with that interface. The interface is achieved by using a new type of roles, called datatype (or concrete) roles, which link abstract objects from the DL domain with datatype predicates from the concrete domain. Also, new concept constructors related to these datatype roles is added. For example, we can denote the set of all people who are more than 18 years old using a datatype role: 9age: 18. Since concrete domains are important for the purposes of this thesis, in the next section we formally present their definition and properties. The concrete domains presentation is based on [104]. 2.2.2.1 Concrete Domains Informally, a concrete domain provides a set of predicates with a predefined inter- pretation. If a decision procedure for checking satisfiability of finite conjunctions over concrete domain predicates exists, many DLs can be coupled with a concrete domain while retaining decidability. However, in [96] it was shown that a logic with GCIs and concrete domains is undecidable. In order to retain decidability, several restrictions were investigated (a survey is available at [97]). The Web Ontology Language, OWL [45] sup- ports a basic form of concrete domains, referred to as OWL datatypes; thus, any OWL reasoner implementation also supports reasoning with (limited) concrete domains. Definition 2 A concrete domain D is a pair (4D, ), where where 4D is a set called the domain of D, and is a finite set of predicate names. Each d 2 is associated with an arity n and an extension dD 4nD. A concrete domain D is admissible if the following conditions holds: 24 is closed under negation. In other words, for each d 2 , there exists a predicate :d 2 with:d =4nDndD contains a unary predicate>D interpreted as the universal concept (4D) satisfiability of finite conjunctions of the form Vni=1 di(xi) is decidable The interpretation of concrete objects is usually separated from the interpretation of the other (abstract) DL objects in the logic to retain decidability. Additionally, for web ontology languages such as OWL, the coupling has been such that only unary concrete predicates are allowed. However, the definition for concrete domains does not have such restriction. In fact, there are implementations of DL reasoners coupled with n-ary concrete domains (see RacerPro [58]) ? this is important since n- ary concrete domains are extensively used in access control policy languages such as XACML. Finally, without loss of generality we can consider only one concrete domain at a time, since an approach for combining two or more concrete domains into one has been presented in [23]. 2.2.2.2 Syntax and Semantics ofSHIQ(D) There has been a great amount of attention to developing reasoning algorithms for increasingly more expressive logics in the DL family. In this following section, I will formally present the syntax and semantics of the very expressive logicSHIQ(D) , which is expressive enough for the purposes of this thesis. 25 Syntax ofSHIQ(D) Definition 3SHIQ(D) Roles Let NR, NcR be the disjoint sets of abstract and concrete atomic roles. The set of SHIQ(D) abstract roles is the set NR [fR j R 2 NRg, where R denotes the inverse of the atomic role R. To avoid considering roles such as R , we define the function Inv such that Inv(R) = R and Inv(R ) = R for R 2 NR. There are no inverses on concrete roles, so the set of SHIQ(D) concrete roles is simply NcR. A role inclusion axiom is of the form R v S where R;S 2 NR, or of the form u v v, where u;v 2 NcR. A transitivity axiom is an expression of the form Trans(R), where R 2 NR. Finally, an RBoxRis a set of role inclusion and transitivity axioms. Letv be the reflexive-transitive closure ofv. A role R is transitive if there is a role S s.t. Trans(S ) 2Rwith S v R and R v S . R is called a simple role if there is no role S s.t. S v R and S is transitive. Definition 4SHIQ(D) Concepts Let NC;NI stand for the set of concept and individual names, andD= (4D; D) be a concrete domain, where4D stands for the domain, and D for the set of predicate names inD. The set ofSHIQ(D) -concepts is defined inductively as the smallest set for which the following holds: every concept name C 2NC is a concept if C and D are concepts and R is a role, then (CuD), (CtD), (:C), (8R:C) and (9R:C) are also concepts if C is a concept, R a simple role and n a natural number, then ( nR:C) and 26 ( nR:C) are also concepts (called at-most and at-least qualified number restric- tions) If P2 D and u2NcR then (9u:P), (8u:P), ( nu:P) , ( nu:P) are also concepts. We write>and?to abbreviate Ct:C and Cu:C respectively. For concepts C;D, a concept inclusion axiom is an expression of the form C v D. A TBox T is a finite set of concept inclusion axioms. An ABox A is a finite set of concept assertions of the form C(a) (where C can be an arbitrary concept expression), role asser- tions of the form R(a;b), concrete domain predicate assertions of the form P(x1;:::;xn) and concrete role assertions u(a;x) where P2 D;a2NI;xi 24D and u2Rd. Given all of the above, aSHIQ(D) KB K is a triple (T ,R ,A ) consisting of a TBox T , RBox R and ABox A . Semantics ofSHIQ(D) The semantics of SHIQ(D) is defined using an interpretation I, which is a pair I = (4;:I), where4is a non-empty set, called the domain of the interpretation, disjoint from the concrete domain4D and :I is the interpretation function. The interpretation function assigns to each atomic concept A a subset of4, to each role R a subset of of4 4and to each individual a an element of4. Additionally, the interpretation function assigns to each concrete atomic role u 2 NcR a subset of4 4D, to each predicate P 2 D a subset of 4D and to each x 2 D an element of 4D. The interpretation function is extended to complex roles and concepts is given in Table 2.2.2.2 (note that R is an abstract role, S is a simple abstract role, u is a concrete role and # denotes cardinality). The model-theoretic semantics ofSHIQ(D) axioms is shown in Table 2.2.2.2. 27 >I = 4 ?I = ; (:C)I = 4nCI (CuD)I = CI ^DI (CtD)I = CI _DI (8R:C)I = fxj8y : (x;y)2RI !y2CIg (9R:C)I = fxj9y : (x;y)2RI ^y2CIg ( nR:C)I = fxj#fyj(x;y)2RI ^y2CIg ng ( nR:C)I = fxj#fyj(x;y)2RI ^y2CIg ng (Inv(R))I = f(a;b)j(b;a)2RIg (8u:P)I = faj8x24D : (a;x)2uI ! x2PIg (9u:P)I = faj9x24D : (a;x)2uI ^x2PIg ( nu:P)I = faj#fx24D j(a;x)2uI ^x2PIg ng ( nu:P)I = faj#fx24D j(a;x)2uI ^x2PIg ng Table 2.1: Interpretations ofSHIQ(D) Concepts and Roles C vD = CI DI C D = CI = DI RvS = RI S I uvv = uI vI Trans(R) = (RI)+ RI C(a) = aI 2CI R(a;b) = (aI;bI)2CI u(a;x) = (aI;xI)2uI a = b = aI = bI a , b = aI , bI Table 2.2: Interpretations ofSHIQ(D) Axioms 28 The interpretation I is a model of the RBox R (respectively of the TBox T and ABox A ) if it satisfies all the axioms in R (respectively T and A ). I is a model of K = (T;R;A), denoted byIj= K, i Iis a model of T , R and A . A KB K is inconsistent if there is no possible model for it, i.e., there is no interpre- tationIthat satisfies the semantics of all of the axioms in T ,R and A . 2.2.2.3 DL Reasoning Services There are a few basic reasoning services in DL, which allow users to deduce implicit knowledge from explicitly represented knowledge: Consistency Checking ? The process of ensuring that the knowledge base has a model (i.e., does not contain contradictory facts). Concept Satisfiability ? Given a concept C, checking if C is satisfiable w.r.t KB K is the task of determining if there exists an interpretationIof K s.t. the interpretation of C (CI) is non empty. Subsumption ? Given concepts C and D, C is subsumed by D w.r.t K , denoted Kj= C vD, if in all interpretationsIof K , CI DI. Instance checking ? determines instance relationships: an individual i is an instance of concept C if in all interpretationsIof K , aI 2CI. It is important to note that all of the above services can be reduced to consistency checking. For example, if we want to check if a concept C is satisfiable w.r.t KB K , when we generate a new individual a s.t. aI 2 CI, and check the consistency of the KB 29 K[fC(a)g. If K is consistent, that means the interpretation of C is non-empty and C is satisfiable. Reasoning in DL is usually done using systems based on tableau algorithms (see [24] for a survey). Tableau algorithms are already used for consistency checking in var- ious optimized DL reasoners that are freely or commercially available, such as RACER [124], FACT++ [65] and Pellet [109]. 2.3 Semantic Web The Semantic Web is intended to be an extension of the current World Wide Web in which information on the Web is represented in a machine processable format with a well defined meaning (semantics). Representing the knowledge on the Web in such a manner provides a variety of benefits including ease of knowledge exchange and integration and machine-automated reasoning. A set of standardized knowledge representation languages (published as W3C recommendations) form the foundation of the Semantic Web and are structured as a layered stack. Following is a brief overview of the standardized Semantic Web languages: The Resource Description Framework (RDF [35] ) is a fairly simple language to describe resources on the web and relations between them. The RDF model is based on the idea of making statements about resources in the form of triples: subject- predicate-object expressions. RDF is based on the same architectural principles that made the Web successful: it uses Universal Resource Identifiers (URI) to identify and link resources on the web. Unlike traditional URLs, however, RDF URIs can 30 refer to any identifiable thing, including things that may not be directly retrievable on the web. RDF Schema [39] is a vocabulary for describing properties and classes of RDF resources. It is a more expressive modeling language than RDF, with the capa- bility for expressing subclasses and subproperties, along with domain and range constraints on properties. OWL [45] adds even more vocabulary for describing properties and classes: among others, relations between classes (e.g. disjointness), cardinality (e.g. ?exactly one?), equality, richer typing of properties, characteristics of properties (e.g. sym- metry), and enumerated classes. OWL comes in three di erent flavors with in- creasing expressivity: OWL Lite, OWL DL and OWL Full. OWL DL and OWL Lite build on the research tradition of Description Logics (they are firmly grounded in DL), so they are both decidable with well studied decision procedures. Since OWL is based on the successful architecture of the Web, it is designed to be open, scalable and distributed which makes it suitable for a web policy representation lan- guage. Its key properties as an ontology language include the use of the URI (Universal Resource Identifier) as the unique identifier for named OWL classes, properties and indi- viduals, and the ability to freely link and/or import ontology models using URIs directly. In addition, OWL assumes open-world semantics, which makes it di erent from closed- world database-schema languages in that information which is not explicitly asserted in the OWL KB is assumed to be unknown or missing instead of non-existent or false. 31 Chapter 3 Related Work In this chapter, an overview of related work in access control languages, access models and verification approaches is presented. First, in Section 3.1 a discussion of the most common access control models (DAC, MAC and RBAC) is presented, followed by an overview of research on access policy languages (Section 3.2). In Section 3.3, I discuss related work in formal verification of access control languages (including XACML), using both state-based and logic-based techniques. 3.1 Access Control Models For the purpose of this thesis, a general understanding of basic access control mod- els is necessary, so this section contains an overview. The three most widely recognized access control models are the following: Mandatory Access Control (MAC) In MAC [8], the access policy is enforced inde- pendently of users? preferences ? in other words, even though a user might be an owner of a resource, he is not allowed to specify an access policy for that resource. MAC is used in systems that process highly sensitive information (e.g., military). One of the most widely used MAC systems is the Multi-Level Security (MLS) policy, i.e., the Bell-LaPadula secu- rity model [28]. The Bell-LaPadula model represents a set of simple access control rules 32 which use security labels on objects and clearances for subjects. These labels form a lat- tice; for example, a well known set of labels is unclassi f ied con f idential secret top-secret. Given these labels, there are only two access rules in the model: The Simple Security Property states that a subject at a given security level may not read an object at a higher security level (no read-up). The *-property (star-property) states that a subject at a given security level is not allowed to write to any object at a lower security level (no write-down). This prop- erty is used to prevent users or programs from declassifying sensitive information. Because of its inflexible nature (only two fixed access rules), MAC has not been deemed expressive enough for commercial purposes. Discretionary Access Control (DAC) In DAC [9], the access policy about an object is determined solely by the object?s owner. An example of this is file ownership in the Unix file system: every file in the system has an owner, and the file?s initial owner can specify its access privileges for other users. Additionally, in DAC users can also delegate control over objects to other users. Discretionary Access Control has been widely used to enforce access policies in operating systems. The most common types of DAC implementations are discussed below. An Access control matrix is a a two-dimensional matrix representing users on the rows and objects on the columns. Each entry in the matrix represents the access type held by that user to that object. Since access control matrices are usually sparsely populated, there exist other, more storage-e cient mechanisms such as access control lists (ACL) 33 and capability-based matrices. ACLs represent each column of the matrix as a list, hence each object is associated with the set of authorized users. An ACL-like mechanism is used in the UNIX file system, where each file is associated with access rights for its owner, group, and everyone else in the system. On the other hand, capability-based systems store the access control matrix by rows. In such systems, each subject is associated with a list of objects he is authorized to access. While more flexible than MAC, Discretionary Access Control su ers from some drawbacks as well. In particular, managing systems with a large number of subjects of objects can be very time-consuming. For example, removing a user (i.e., subject) from the system involves traversing and removing the subject from the ACL of each object. Role Based Access Control RBAC [10] is a newer alternative to MAC and DAC, ex- pressive enough to cover both. In RBAC, roles are created for various job functions. Each role can have a number of permissions assigned to it; these permissions refer to certain operations needed for the particular function. Users are then assigned particular roles, and through these assignments acquire the permissions needed to perform the job func- tions. RBAC di ers from ACLs in that it assigns permissions to specific operations with meaning in the organization, rather than to low level data objects. There has been a lot of interest in developing RBAC models in the past years [116, 107, 106, 125, 100], however the consensus is that RBAC0 [116] has emerged as the core RBAC model (it is also being standardized by NIST [10]). In RBAC0, the key components are sets of users (U), roles (R) and permissions (P). The policy is then specified by a user assignment relation, associating users to roles they hold, and a permission assignment 34 relation linking roles to sets of permissions. Additionally, roles have to be activated within sessions. A user can activate multiple roles in a single session; she can also act in multiple sessions at the same time. There have been a number of extensions to RBAC0, the most important being role hierarchies (RBAC1) and constraints (RBAC2). Role hierarchies allow a role to inherit all of the access privileges of another role. For example, one can state that role Manager is senior to Intern, so a user activating the Manager role will inherit all of the permissions of Intern. RBAC2 supports constraints, which essentially impose restrictions on acceptable configurations of the di erent RBAC components. A common motivation for constraints is the example of mutually disjoint roles, such as purchasing manager and accounts man- ager. In most organizations, the same individual will not be permitted to be a member of both roles, because this creates a possibility for committing fraud. This is the well-known security principle of separation of duties, and is available as a constraint in RBAC2. Ad- ditionally, it is possible to limit the number of roles which an individual user can activate (using a cardinality constraint). Since XACML subsumes RBAC2 in terms of expressiveness [17], all of the XAML analysis services presented in this dissertation apply to RBAC implementations as well. 3.2 Access Control Languages This section contains an overview of related work in logic-based security languages as well policy languages based on Semantic Web techniques. The goal is to compare my 35 logic-based, semantic web-enabled policy framework with previous work in the area. 3.2.1 Logic-Based Languages The languages discussed in this section all benefit from having unambiguous se- mantics and well understood computational properties. Most of them are based on Dat- alog, so evaluating whether a request satisfies the policy is done in PTIME. Some of the proposals [72] even materialize the unique model of the underlying Datalog program to avoid doing any reasoning at runtime. 3.2.1.1 Centralized Policies Centralized access policies refers to security systems with only one PDP (Policy Decision Point). Note that this still allows the policies to be distributed ? however, during deployment they have to be retrieved and evaluated at a single PDP. There are many logic- based policy frameworks that fit this description [30, 71, 73, 32]. This section presents two representative approaches: the work by Woo and Lam [128], which is one of the earliest attempts at a logic-based authorization framework, and the Flexible Authorization Framework (FAF) [71] which represents one of the most influential policy frameworks. Authorization using Default Logic (Woo and Lam) One of the earliest attempts at a general, logic-based framework for expressing authorizations was made by Woo and Lam [128], who proposed the use of default logic to model authorization and control rules. Default logic is a very expressive framework, allowing the authors to cover both open and closed policy bases with their languages, as well as the Bell-LaPadula model. 36 To overcome the complexity drawbacks of default logic (it?s undecidable in the general case), the authors used a subset of the logic called extended logic programs (ELP) as the basis for their framework. ELPs are essentially a class of stratified logic programs with both classical negation and negation as failure, but with a unique minimal model that can be computed in quadratic time. The authors, however, did not address the question of how this restriction will a ect the expressiveness of their policies. Additionally, they did not provide any analysis services such as formal verification of policies. Flexible Authorization Framework (FAF) Jajodia et al.[71] proposed a logical lan- guage for specification of authorizations that allows users to specify, together with the authorizations, the policy according to which access control decisions are to be made. Policies are expressed by means of rules which enforce derivation of authorizations, con- flict resolution, access control, and integrity constraint checking. The architecture of FAF consists of the following components: A history table whose rows describe the access requests processed. An authorization table whose rows are composed of authorization triples (o,s,+a) and (o,s,-a). Informally, (o,s,+a) is a positive authorization triple ? it means that subject s can perform action a on object o; (o,s,-a) forbids the action. A propagation policy that specifies how to derive authorizations from the explicit authorization table above. In particular, FAF supports the following propagation policies: no propagation, no overriding, most specific overrides and path overrides. A conflict resolution and decision policy that specifies how to override conflicts 37 when one or two conflicting authorizations apply to a given authorization triple. Ex- amples of conflict resolution policies supported by FAF include: no-conflict (con- flicts are considered errors), denials-take-precedence, permissions-take-precedence and nothing-takes-precedence (conflicts remain unsolved). The decision policy also determines the system?s final response to every access request. For example, the decision policy can force a deny decision whenever conflicts occur, or can force a decision to fill in the gaps in the absence of any access decision for a particular access request. A set of integrity constraints that impose restrictions on the content of the individual components in FAF. The authorization table in FAF is viewed as a database. The propagation, conflict resolution and decision policies are expressed using stratified logic programs, guarantee- ing that the overall policy system has a unique stable model. As a result, FAF corresponds to a quadratic time data complexity fragment of logic programming. To improve scala- bility of the framework, the authors proposed a materialization technique that allows for incremental updates of the unique stable model at run-time. One of the contributions of my work is a detailed comparison between XACML and FAF, provided in Chapter 5. 3.2.1.2 Distributed Policies By distributed access policies I refer to policies that exist in a distributed envi- ronment such as the Web and security systems with multiple PDPs. Such decentralized 38 environments have the following distinctive characteristics: Identity of all possible access requesters cannot be known before hand, so subjects present digital credentials (which may be distributed themselves) in order to gain access. In addition to the access policy on the server, the access subjects (clients) might have policies for their own data as well. In such case, there exists a need for trust negotiation to determine if client?s and server?s policies are compatible. Delegation is essential to distributed PDPs. Depending on the object o being ac- cessed, a particular security point might not be qualified to make an access decision about o; in such cases, the access request is delegated to a security point with the system that has authority over objects of type o. In the following, a survey of logic-based approaches to distributed policy authoriza- tion is presented. Delegation Logic [88] combines the following features: it is based on logic pro- grams, can express delegation depth explicitly and supports a wide variety of complex delegation principles (e.g., k-out-of-n threshold). In addition, Delegation Logic provides a concept of proof-of-compliance that is based on model-theoretic semantics. The frame- work is based on a restricted class of logic programming called Ordinary Logic Programs (OLP [56]), and a transformation is presented from OLP to positive Datalog programs. However, the transformation is exponential in the number of logical variables used in the policy, and no evaluation is presented, so it is unclear whether the approach scales. 39 Additionally, Delegation Logic can be extended with non-monotonicity, negation and prioritized conflict handling; however, severe restrictions on the usage of the delega- tion constructs are placed to ensure tractability [85]. PeerAccess [127] is a trust negotiation framework for reasoning about authoriza- tion in open distributed systems. It supports a declarative description of the behavior of peers that selectively push and/or pull information from certain other peers. PeerAccess local knowledge bases encode the basic knowledge of each peer, its policies governing the release of each possible piece of information to other peers.PeerAccess proofs of autho- rization are verifiable and nonrepudiable, and their construction relies only on the local information possessed by peers and their parameterized behavior with respect to query answering, information push/pull and information release policies. In addition to PeerAccess and Delegation Logic, there are other Datalog-based lan- guages that support delegation; SecPal [27], Binder [46], SD3 [75], RT [90] and Cas- sandra [101] all use Datalog as basis for syntax and semantics. (Cassandra and RTC are based on Datalog with constraints for higher flexibility.) In contrast to the above approaches, Proof-carrying Authorization (PCA) and re- lated distributed proof systems [26] are an authorization framework based on a higher- order logic where di erent domains in the system use di erent, less expressive, application- specific logics. The higher-order logic (AF logic) used to check the proofs is undecidable, though this problem is avoided by forcing clients to generate proofs on their own, using only a decidable subset of AF logic. Consequently, the authorizing servers task of proof- checking is reduced to a tractable type-checking problem - however this leads to large rate of increase of sizes of the client proof. 40 3.2.1.3 Dynamic/Temporal Access Policy Languages Most of previous work that was discussed dealt with static authorization, i.e., access policies where the authorizations do not change over time and do not have any temporal dependencies. This section surveys approaches that deal with dynamic policies. First, I discuss a seminal approach that supports evolving subjects, resources and authoriza- tions, and then discuss a more recent policy language extension of RBAC that supports temporally dependent authorizations. The framework of Harrison, Ruzzo and Ullman [61] is one of the earliest ap- proaches that allows for changing number of subjects, roles, resources, and authoriza- tions. The HRU model is very expressive; it could model most of the protection systems in use at that time when it was proposed. However, because of the expressiveness, there is no algorithm to decide if a given subject can eventually obtain an access privilege to a given object (it is undecidable). Bertino et al [29] presented a temporal extension of the RBAC model called TR- BAC. TRBAC supports periodic role enabling and disabling?possibly with individual exceptions for particular users?and temporal dependencies among such actions, ex- pressed by means of role triggers. Role trigger actions may be either immediately ex- ecuted, or deferred by an explicitly specified amount of time. Enabling and disabling actions may be given a priority, which is used to solve conflicting actions. A formal se- mantics for the specification language was provided, and a polynomial safeness check was introduced to reject ambiguous or inconsistent specifications. The authors also presented an implementation of TRBAC on top of a conventional DBMS. 41 3.2.2 Semantic Web-Based languages Recently there has been a great amount of attention to how Semantic Web tech- nologies can be used in policy systems. In particular, there have been a number of proposals that show how to ground or express policies in a Semantic Web framework [126, 77, 78, 122]. Rei [77] is a policy specification language based on a combination of OWL-Lite, logic-like variables and rules. It allows users to develop declarative policies over domain specific ontologies in RDF and OWL. Rei allows policies to be specified as constraints over allowable and obligated actions on resources in the environment. A distinguishing feature of Rei is that it includes specifications for speech acts for remote policy manage- ment and policy analysis specifications like what-if analysis and use-case management. The successor of Rei is Rein [78], which is a policy framework grounded in se- mantic web technologies that allows for di erent policy languages and supports hetero- geneous policy systems. Rein provides an ontology for describing policy domains in a decentralized manner and provides a reasoning engine built on top of CWM, an N3 rules reasoner. Using Rein and CWM, the authors showed how it is possible to develop domain and policy language specific security systems. Rein has been successfully used as a pol- icy management system in the Policy Aware Web project [126], which in turn provides an architecture for scalable, discretionary, rule-based access control in open and distributed environments. PeerTrust [52] deals with discretionary access control on the web using seman- tic web technologies. It provides a mechanism for gaining access to secure informa- 42 tion/services on the web by using semantic annotations, policies and automated trust ne- gotiation. In PeerTrust, trust is established incrementally through an iterative process which involves gradually disclosing credentials and requests for credentials. PeerTrust?s policy language for expressing access control policies is based on definite Horn clauses. A distinguishing feature of PeerTrust is that it expects both parties to exchange credentials in order to trust each other and assumes that policies are private, which is appropriate for critical resources such as military applications and e-commerce sites. Finally, KaOS Policy and Domain Services [122] use ontology concepts encoded in OWL to build policies. These policies constrain allowable actions performed by actors which may be clients or agents. The KAoS Policy Service distinguishes between autho- rizations and obligations. The applicability of the policy is defined by a class of situations which definition can contain components specifying required history, state and currently undertaken action. 3.2.3 Discussion One of the goals of this section was to demonstrate that recently there has been a great amount of interest in logic-based policy languages, and that most of these languages are based on some variant of logic programming (most often, Datalog). Given that, it is surprising that a standardized and widely distributed language such as XACML has not been formally compared to these languages. The main impediment for this was the lack of formal, logic-based semantics for the language. This problem is addressed in Chapter 5, where I show that the core of XACML can be embedded in stratified Datalog. 43 Additionally, note that most of the policy languages discussed in this section ad- dress the challenges that a policy system should overcome to be usable in a massively open and distributed setting. Thus, they mostly discuss the architectural, privacy and scalability aspects of a policy framework. Much less attention is being paid to security analysis issues such as formal verification of policies against security properties, change analysis of di erent policies and coverage checking which are important to ensure the ac- cess policy has no bugs. Most of the above approaches base their semantics in Datalog, in order to maintain balance between policy expressiveness and computational complexity. However, as shown in [31], in Datalog-based models it is very hard (actually undecid- able) to provide change analysis, i.e., for two policies expressed as Datalog programs to determine if they would always return the same access decision for any potential access request. To provide such analysis services, instead of logic programming I use a di erent family of logics, called Description Logics ? more information is presented in Chapter 6. 3.3 Policy Analysis and Verification The policy languages surveyed in the previous section usually o er two basic ser- vices: 1) checking the consistency of an access policy set, i.e., determining if there are any conflicting policies in the system, and 2) for a given request R and a policy P determining the access decision of P for R. However, recently, there has been a great amount of interest into other types of analysis services for policies [92, 91, 14, 83, 50, 66, 131, 117, 50, 36], the most common being verification of a policy against given safety properties. For ex- ample, as a part of a company-wide access policy, one could state ?Junior developers 44 should never be allowed to sign expense reports? or ?At any given time, a user cannot activate more than one of the following three roles fJuniorDeveloper, SeniorDeveloper, AccountsClerkg?. Then, company security o cers would use automated tools to verify that these constraints will not be violated against all possible access requests. In the event violations are discovered and the policy is updated, change analysis can be performed to ensure no new bugs were unintentionally introduced ? for example, using queries of the form ?Show me all requests involving Expense Reports that used to map to Deny but now are mapping to Permit?. The above mentioned services of verification and change analysis have been proposed as the building block of a useful policy analysis tool ([50]). This section surveys previous work on such analysis services for access control policies. First, I provide an overview of security policy analysis (using state-based or logic-based approaches), then in Section 3.3.1 I discuss approaches that embed existing policy languages into a logic, thus providing analysis services previously not available. Finally, in Section 3.3.2 I survey such logical embeddings of XACML itself. Elisa Bertino et al [31] proposed a formal framework for reasoning about di er- ent access control models. Their framework is logic-based and can capture DAC, MAC and RBAC models. Each instance of the proposed framework corresponds to a Datalog program, interpreted according to the stable model semantics. To demonstrate its expres- siveness, the authors mapped the Bell and LaPadula model [28] and NIST RBAC [116] to the framework. They also proposed some parameters (along with decidability results) along which access control models can be compared. For example, they showed that checking for structural subsumption/equivalence between di erent access control models is decidable, however access request equivalence is not. The di erence with our work 45 is the language we analyze (XACML) and the services we provide (e.g., we show that access request equivalence is decidable for XACML). Chomicki and Lobo [38] introduced a declarative policy description language called PDLin which policies are described as sets of event-condition-action (ECA) rules. They provided a framework for detecting and resolving conflicts between the ECA rules and any action constraints. This is performed using a policy monitor, which, in order to resolve conflicts chooses or ignores certain events, essentially preventing the ECA rule from activating and causing the conflict. The semantics of the ECA rules and conflict detection and resolution are defined using logic programs. Unlike XACML, where con- flict resolution is built in the language, in their framework whenever a conflict occurs the policy engine has to generate a minimal set of actions to be removed in order to remain consistent. Dougherty et al. [48] presented a model for formal analysis of access-control poli- cies in dynamic environments, taking into account the possible interactions of the policies with their environments. For this model, they proposed two analysis services: a) goal reachability, which checks if there is some accessible state in the dynamic access model which satisfies some boolean expression over the policy facts and b) contextual policy containment, which essentially checks if one policy is more permissive than another. These services are provided using a combination of relational and temporal reasoning. Policies that change their environment are not addressed in my thesis; on the other hand, we perform static analysis services on a richer policy language ([48] does not support concrete domains and ontology-based policy models). Lithium [59] is a language for reasoning about digital rights and is based on a 46 fragment of first order logic. It is di erent from Datalog-based approaches since it allows full negation in the conclusion as well as in the premises of policy rules. To show its expressiveness, the authors gathered a large collection of policies from di erent types of libraries and mapped them to Lithium. They also showed how large fragments of XrML [60] and ODRL [112] can be translated in the language. Two core analysis services are provided: Given a set of policies, a policy environment and an access request, does it follow that the access request is permitted by the policy set? Consistency checking of a policy set. Unlike [71], the language does not support conflict resolution mechanisms, so whenever both a permit and deny is returned by a policy, it is treated as an error. In order to remain decidable, Lithium restricts recursion and cannot easily express dele- gation. Unlike XACML, Lithium does not provide any conflict resolution mechanisms, and it does not support change analysis and coverage checking of policies. There has also been research on security analysis for access control [92, 91] that uses the notions of states of policy systems and transitions (for example, adding a role, or changing a permission) that alter those states. Then, usually a set of queries is proposed that investigates the possible consequences of certain changes in the policy. Simple safety checking is an example of a query; it checks if there exists a reachable state in which a (presumably untrusted) principal has access to a resource. Although early results showed that this type of safety analysis can easily lead to undecidability [61], there has been recent work that demonstrates a class of access control models and queries for which safety is 47 decidable and e cient algorithms exist [92]. Unfortunately, there are limitations to the expressiveness of the models that are analyzed: the states are described using positive Datalog programs, so there is no support for classical negation. No classical negation in turn implies no support for negative authorizations and common constraints such as mutually exclusive roles. As another state-based approach, Schaad et al. [117] examineed the problem of verifying a policy that is subject to change coming from another policy. Using the Alloy [70] specification language and its model-checking facilities, they showed how to spec- ify an RBAC96-style model, ARBAC97-style extensions and a set of separation of duty properties. There were no implementation or evaluation results given, so it is di cult to compare with our approach. In [131] the authors presented a model-checking algorithm which can be used to evaluate access control policies, and a tool which implements it. Their tool provides reachability analysis: not only checks whether the policies give legitimate users enough permissions to reach their goals, but also whether the policies prevent intruders from reaching their malicious goals. Policies of the access control system and goals of agents are described in the language RW [57]. RW and the analysis framework presented in this thesis provide a complementary set of services: theirs is reachability analysis in presence of rule interactions, cooperating agents and multi-step actions, while in this thesis the services provided are change analysis, coverage checking and formal verification for a static policy system. There are also proposals for analyzing policies based on description [132] or modal logics [99]. Both of these provide a formalization of RBAC, and show how tableau-based 48 decision methods can be used for consistency checking of policies, evaluating access re- quests and verifying policies against security properties. Zhao et al [132] presented a formalization of RBAC based on the description logic ALCQ. They also showed how RBAC policy constraints (separation of duty, role hierarchies) can be captured in this logic. Massacci [99] formalized RBAC using multi modal logic and presented a deci- sion method based on analytic tableaux. Because tableau-based algorithms are used , services similar to ours are provided: logical consequence, model generation and consis- tency checking of policies. The analysis framework in my thesis is for a more expressive language (e.g., neither of the approaches supports conflict resolution algorithms or con- crete domains). In [14], the authors proposed a set of services under the name of policy ratification. In particular, they presented algorithms for analysis tasks such as dominance, coverage and consistency check that can be performed independently of policy model and language and require little domain-specific knowledge. They presented algorithms from constraint, linear, and logic programming disciplines to help perform ratification tasks. Also, an al- gorithm is provided to e ciently assign priorities to the policies based on relative policy preferences indicated by policy administrators. Finally, they present how these algorithms have been integrated with a working policy system to provide feedback to a policy admin- istrator regarding potential interactions of policies. The techniques the authors use for ratification are similar to the algorithms used for datatype reasoning in this thesis. How- ever, our work can be considered an extension of theirs since it covers a more expressive policy language (XACML). 49 3.3.1 Embedding Policy Languages in Logic As mentioned in the previous section, the authors of Lithium showed that large fragments of ODRL [112] and XrML [60] can be translated to their FOL-based language. In addition to giving ODRL formal semantics, the authors considered the practical prob- lem of determining whether a set of ODRL statements imply a permission or prohibition. Using their semantics, they formally defined the problem and showed that it is NP-hard. They also showed that by removing a component of ODRL whose meaning seems to be somewhat unclear, a tractable fragment of the language results. They proved that the frag- ment is tractable by creating a polynomial-time algorithm to determine whether a set of ODRL statements imply a permission (or prohibition). They presented a similar contribu- tion for XrML in [60]: propose a formal semantics, show that deciding access requests in the language is NP-hard, then show an expressive fragment of the language for which de- ciding access requests is polynomial. The relationship between XrML and ODRL on one hand and XACML on the other is unclear; however we discussed the di erences between Lithium (the language used to formalize XrML and ODRL) and our formal framework in the previous section. In [89] the authors presented a first-order logic (FOL) semantics for the Simple Distributed Security Infrastructure (SDSI [115]). The authors proved that the FOL se- mantics is equivalent to the string rewriting semantics used by SDSI designers, for all queries associated with the rewriting semantics. Using their semantics, they discovered a few problems in the proof procedures for SDSI. Finally, they compared SDSI with RT1C, a datalog-based language that is part of the RT policy framework [90]. The authors did 50 not discuss formal verification or change analysis for their language. 3.3.2 XACML Analysis and Verification In this section I will discuss approaches that formalize and analyze fragments of XACML [66, 131, 117, 50, 121, 36, 40] and are most related to my dissertation. Hughes et al. [66] proposed a framework for automated verification of XACML policies based on relational First-Order Logic. They introduced a formal model for sys- tematically specifying access to resources, and showed that XACML policies can be trans- lated to a simple form which partitions the input domain to four classes: permit, deny, error, and notapplicable. The authors showed how to automatically verify policies using an existing automated analysis tool, Alloy [70]. Because using the first-order constructs of Alloy to model XACML policies is prohibitively expensive (in terms of performance), the authors used only the propositional constructs. The limitation of their approach is that they do not fully support data-types, policy vocabularies and delegation policies. I have provided a thorough empirical comparison of my prototype analyzer against their XACML analysis tool; results are discussed in Chapter 8. Bryans et al. [36] formalized XACML policies using a process algebra known as Communicating Sequential Processes (CSP [63]). This allows them to use model check- ers such as FDR for formally verifying properties of policies and for comparing access control policies. In addition, the authors showed how limited workflows can also be mapped to CSP. The workflow is sequential in nature and in that sense their approach is more expressive than first-order logic approaches. The authors provide no information on 51 any empirical results or prototype implementation, so I have not performed an comparison with my XACML reasoner. In [50], the authors expressed XACML policies using Multi-Terminal Binary De- cision Diagrams (MTBDDs). MTBDDs [51] are a more general version of Binary Deci- sion Diagrams, that maps bit vectors over a set of variables to a finite set of results. In [50], variables in the decision diagram are used to represent attribute/value pairs (such as role=Student, action=View, etc.) and the policy results (Deny, Permit, Indeterminate) are mapped to diagram terminals. The approach from their paper is implemented in Mar- grave, a tool for analyzing XACML policies. Margrave provides verification and compre- hensive change-impact analysis support based on the semantic di erences between the MTBDDs representing the policies. Compared to Margrave, our analysis framework cov- ers a richer subset of XACML (administrative policies, datatypes, ontology-based policy models). In addition, for the subset that both Margrave and our tool support, I provide a detailed performance comparison of the tools in Chapter 8. Finally, in [42] the authors extended the work by Fisler et al. [50] by adding more expressiveness to the language being analyzed and supporting additional analysis ser- vices. Their tool, called EXAM (comprehensive framework for analysis of access control policies), in addition to supporting core XACML defined in [50] also supports datatype domains. One of the components in the framework is a policy similarity analyzer [93] which is used to filter out policies with low similarity score. While EXAM provides datatype support, it does not explicitly address ontology-based policy models or delega- tion policies. . 52 Chapter 4 Operational Semantics of XACML In this chapter, a formal semantics for XACML v3.0 is presented. The semantics is provided through a concise set of rules that capture the meaning of the XACML constructs as presented in the o cial specification. This semantics is used to prove the correctness of the Datalog and Description Logic mappings presented in Chapters 5 and 6. 4.1 Syntax To avoid the verbose XML representation of XACML, a lisp-like syntax is used, similarly to [121]. A typewriter font denotes names of syntax elements as they occur in the XACML specification. Thus, Policy refers to the XACML syntactic element that contains Rules, whereas a policy can refer to a set of Policy or PolicySet elements. Also, terminal nodes in the syntax grammar below are denoted by a lower case starting letter. The syntax for XACML Policies, PolicySets and Rules is shown in Table 4.1. Table 4.2 presents the syntax of Targets and matching functions. Table 4.3 shows the syntax of Condition elements in Rules. Note that arbitrary nesting of functions is allowed in the Condition element. I only show a few of the sup- ported functions in the table; a full listing can be found in the XACML 3.0 Specification [113]. Finally, Table 4.4 contains the syntax for XACML access requests. 53 S ::= (PolicySet Comb T S id) j (Policy Comb T R id) R ::= (Rule Cond T E ect) Comb ::= permit-Overrides j deny-Overrides j first-Applicable j only-One-Applicable E ect ::= PermitjDeny Table 4.1: Syntax of Policy Elements. T ::= (Target DM ) DM ::= (DisjunctiveMatch CM+) CM ::= (ConjunctiveMatch M+) M ::= (Match AV AD MatchFcn) j (Match AV AS MatchFcn) AD ::= (AttributeDesignator cat attr-ID Type issuer? mustBePresent?) AS ::= (AttributeSelector contextPath Type present?) AV ::= (AttributeValue value Type) MatchFcn ::= type-equaljtype-greater-thanj type-greater-than-or-equaljtype-less-thanj type-less-than-or-equaljtype-regexp-match Type ::= stringjbooleanjintegerj ::: Table 4.2: Syntax of Targets and Matching Functions. Example 4.1.0.1 This example illustrates how a XACML Rule element in normative XML syntax is translated to my abbreviated lisp-like representation. med.example.com 54 Cond ::= (Condition Expr ) Expr ::= ApplyjASjAV j FunctionjVariableReferencejAD Apply ::= (Fcn-ID Expr ) Function ::= (Fcn-ID Expr ) Fcn-ID ::= any-ofjall-ofjregexp-match::: Table 4.3: Syntax of Condition element. RQ ::= (Request ATS ) ATS ::= (Attributes (AT content) cat) AT ::= (Attribute AV attr-ID issuer) ARQ ::= (Request Delegated Del-info Delegate ATS ) Delegate ::= ((AT content) delegate) Del-info ::= ((AT content) del-info) Delegated ::= ((AT content) delegated) Table 4.4: Syntax of access requests. ARQ represents an administrative request (a special case of access requests). The example Rule is abbreviated as: (Rule SimpleRule1 () (Target (DisjunctiveMatch (ConjunctiveMatch (Match (AttributeValue med.example.com string) (AttributeDesignator access-subject subject-id rfc822Name ()()) rfc822Name-match )))) Permit) 4.2 Proof-theoretic Semantics In this section, a proof-theoretic semantics of XACML is presented using natural deduction rules. I use the following notation: for a syntactic element P, XP refers to a 55 child element of P that is of type X. For example, for a Policy element P, TP refers to its Target. 4.2.1 Matching Functions XACML is an attribute-based language, so in its most basic form it matches at- tribute values from a request with policy Targets. This section (specifically Tables 4.5 and 4.6) presents the inference rules that determine if a Request matches a Target. Table 4.5 contains the inference rules that determine how an AttributeDesignator or AttributeSelector element in a policy selects an attribute value from a Request. In the case of an AttributeDesignator, the value will be selected only if the attribute id, category and datatype all match (Rules 1 and 2). For AttributeSelectors, an AttributeValue is selected by evaluating the xpath function in the selector against the Request (Rule 3). Rules 4 and 5 are for cases when no AttributeValue is selected, yet mustBePresent is set to true; in those cases, Indeterminate is returned. Table 4.6 contains the inference rules that determine how a Request is matched against a Target. Rule 1 matches a selected AttributeValue from the Request against the comparison function in the Match element. If the comparison function is true, the Request RQ matches the Match element M. The rest of the rules in Table 4.6 show how this match can be propagated through ConjunctiveMatch and DisjunctiveMatch to Target elements. In Table 4.7, the semantics of matching a Request against a Rule are presented. Notice that in Rule 1, the rule firing depends on the evaluation of its Condition ele- 56 ment. Note that in XACML v3.0, a total of 237 di erent functions are allowed in the Condition. The semantics of these functions has already been covered in [68], so I omit their discussion here. If a syntax error occurs during matching, in the specification Indeterminate is returned as result. Since this chapter focuses on the semantic properties of XACML, it is assumed that the policy and request in question are syntactically correct. Observe that even with a syntactically correct policy set, an Indeterminate could be returned ? e.g., if the mustBePresent attribute of an AttributeDesignator is true and there is no attribute in the request that matches it (Rule 3 in 4.5). Rule 1 attr-idAD = attr-idAT typeAVAT = typeAD 8issuerAD;issuerAT : issuerAD = issuerAT AD;ATj= AVAT Rule 2 9ATS2RQ;AT2ATS : catAD = catATS AD;ATj= AVAT AD;RQj= AVAT Rule 3 Value = xpath-select(RQ;contextPathAS ) AS;RQj= Value Rule 4 8ATS2RQ;8AT2ATS : AD;RQ6j= AVAT mustBePresentAD = True AD;RQj= Indeterminate Rule 5 AS;RQ6j= Value mustBePresentAS = True AS;RQj= Indeterminate Table 4.5: Matching AttributeDesignator and AttributeSelector with attributes in Request. 57 Rule 1 9AD2M : AD;RQj= AVAT fcnM(AVM;AVAT ) = True M;RQj= True Rule 2 9AD2M : AD;RQj= Indeterminate M;RQj= Indeterminate Rule 3 9AS2M : AS;RQj= AVAT fcnM(AVM;AVAT ) = True M;RQj= True Rule 4 9AS2M : AS;RQj= Indeterminate M;RQj= Indeterminate Rule 5 8MCM : MCM;RQj= True CM;RQj= True Rule 6 8MCM : MCM;RQj= Indeterminate CM;RQj= Indeterminate Rule 7 9CMDM : CMDM;RQj= True DM;RQj= True Rule 8 8CMDM : CMDM;RQj= Indeterminate DM;RQj= Indeterminate Rule 9 8DMT : DMT;RQj= True T;RQj= True Rule 10 9DMT : DMT;RQj= Indeterminate T;RQj= Indeterminate Table 4.6: Matching a Request(RQ) with a Target(T). Rule 1 TR;RQj= True CondR;RQj= True R;RQj= E ectR Rule 2 TR;RQj= Indeterminate R;RQj= Indeterminate Rule 3 R;RQ6j= EffectR R;RQ6j= Indeterminate R;RQj= NotApplicable Table 4.7: Evaluating a Rule against a Request. 58 4.2.2 Rules, Policies, PolicySets This section contains rules that capture the semantics of the four basic rule- and policy-combining algorithms: permit-overrides, deny-overrides, first-applicable and only- one-applicable. The rule- and policy-combining algorithms are very similar; the only dif- ference occurs when an Indeterminate is returned while evaluating a child element. In a PermitOverrides rule-combining algorithm, an Indeterminate decision over- rides a Deny, whereas in the equivalent policy-combining algorithm Deny decision would override Indeterminate. Table 4.8 contains the inference rules for Permit-Overrides and Deny-Overrides rule-combining algorithms. Because the rules for Permit- and Deny-Overrides are sym- metrical, I have presented only one set of them (using a shorthand notation to stand for Permit/Deny). Notice that for Permit-Overrides (resp. Deny-Overrides) if a Permit (resp. Deny) Rule returns Indeterminate, then assuming that there are no Deny (resp. Permit) rules that fired, the parent Policy would return Indeterminate as well. This subtle behavior was missed in previous formalizations of XACML [121]. Tables 4.9 and 4.10 present the semantics for First-Applicable and OnlyOne- Applicable rule-combining algorithms, respectively. While evaluating First-Applicable, the Rules are ordered according to their position in the Policy element. Given such or- dering, as soon as a decision is returned from a Rule, that decision is returned and all subsequent Rules are ignored. In Table 4.11, the semantics for Permit-Overrides and Deny-Overrides are shown. Note that unlike their rule-combining counterparts, Permit-Overrides and 59 Rule 1 9i : Ri;RQj= T;RQj= True (Policy -Overrides T R1;:::;Rn);RQj= Rule 2 9i : Ri;RQj= Indeterminate^E ectRi = T;RQj= True 8j : Rj;RQ6j= (Policy -Overrides T R1;:::;Rn);RQj= Indeterminate Rule 3 8i : Ri;RQ6j= Indeterminate_E ectRi = ? 9i : Ri;RQj= ? T;RQj= True 8j : Rj;RQ6j= (Policy -Overrides T R1;:::;Rn);RQj= ? Table 4.8: -Overrides Rule Combining Algorithm. stands for Permit or Deny, and ? for the opposite. Rule 1 Effect2fPermit;Deny;Indeterminateg T;RQj= True 9Ri s.t. Ri;RQj= Effect 8Rjs.t. j < i : Rj;RQj= NotApplicable (Policy First-Applicable T R1;:::;Rn);RQj= Effect Table 4.9: First-Applicable Rule Combining Algorithms. 60 Rule 1 9i : Ri;RQj= Indeterminate T;RQj= True (Policy Only-One-Applicable T R1;:::;Rn);RQj= Indeterminate Rule 2 9i; j : (Ri;RQj= Deny_Ri;RQj= Permit)^ (Rj;RQj= Deny_Rj;RQj= Permit)^ i , j T;RQj= True (Policy Only-One-Applicable T R1;:::;Rn);RQj= Indeterminate Rule 3 9i : Ri;RQj= Effect 8j s.t. j , i : Rj;RQj= NotApplicable T;RQj= True (Policy Only-One-Applicable T R1;:::;Rn);RQj= Effect Table 4.10: Only-One-Applicable Rule Overriding Algorithm. Deny-Overrides are not symmetrical. The Only-One-Applicable and First-Applicable policy-combining algorithms are same as for Rules, so they are not shown here. Finally, Table 4.12 contains the generic rules that hold regardless of the combining algorithm in question. These rules are used to infer Indeterminate or NotApplicable and are always applied with lowest priority, only in cases when no access decision was made using other inference rules. 4.2.3 Multiple Resource and Hierarchical Profile While an important part of XACML, the Multiple Resource [20] and Hierarchical Profile [18] profiles do not actually add any expressive power to the language. Instead, they introduce abbreviated syntax that can be used to express access requests covering multiple resource in a concise manner. The semantics of such requests is given by ?un- 61 Rule 1 9i : Pi;RQj= Permit T;RQj= True (PolicySet Permit-Overrides T P1;:::;Pn);RQj= Permit Rule 2 9i : Pi;RQj= Deny T;RQj= True 8j : Pj;RQ6j= Permit (PolicySet Permit-Overrides T P1;:::;Pn);RQj= Deny Rule 3 9i : Pi;RQj= Deny_Pi;RQj= Indeterminate T;RQj= True (PolicySet Deny-Overrides T P1;:::;Pn);RQj= Deny Rule 4 9i : Pi;RQj= Permit T;RQj= True 8j : Pj;RQ6j= Deny^Pj;RQ6j= Indeterminate (PolicySet Deny-Overrides T P1;:::;Pn);RQj= Permit Table 4.11: Permit-Overrides and Deny-Overrides Policy Combining Algorithms. Rule 1 Comb , Deny-Overrides 9i : Pi;RQj= Indeterminate T;RQj= True 8j : Pj;RQj= Indeterminate_Pj;RQj= NotApplicable (PolicySet Comb T P1;:::;Pn);RQj= Indeterminate Rule 2 9i : Ri;RQj= Indeterminate T;RQj= True 8j : Rj;RQ6j= Permit^Rj;RQ6j= Deny (Policy Comb T R1;:::;Rn);RQj= Indeterminate Rule 3 P;RQ6j= Permit P;RQ6j= Deny P;RQ6j= Indeterminate P;RQj= NotApplicable Table 4.12: Generic Indeterminate rule for policies and rules. 62 wrapping? them into individual access requests, and then evaluating each request sep- arately. Without any loss of generality, the discussion is focused on individual access requests. 4.2.4 Administrative Profile So far, I have only been discussing access policies, i.e., policies that specify the situations under which users are granted or denied access. An administrative policy, on the other hand, specifies who (and under what conditions) is authorized to write access policies. For example, an administrative policy might state that members of group Ad- ministrators are allowed to write access policies about Files. Following, I describe the basic processing model of administrative XACML. When a new access request R is to be checked against a XACML policy, it is first applied against all access policies in the set. If some policy applies to R and yields an access decision, then the access decision needs to be authorized by a trusted policy using a process defined in [114] as reduction. Reduction is performed by applying the access request against any administrative policy Ps which is sibling of P, generating administrative requests ARQ. Then, using the administrative requests and other policies reduction edges are generated between the policies. The semantics of reduction is shown in Table 4.13. Finally, a search is performed through the reduction graph starting from the original access policy P, following reduction edges until a trusted policy is reached. The access decision of P is authorized only if the graph search reaches a trusted policy. The propagation rules (pertaining to the graph 63 search) are shown in Table 4.14. Rule 3 ARQ = (Request Delegated Del-Info Delegate ATS-Admin) ARQ;Pj=red (Request ATS-Admin IssuerP ;) Rule 1 8Pi;Pj;s:t:parent(Pi) = parent(Pj) RQ;Pi j=red AR AR;Pj j= P(Pi;Pj) Rule 2 8Pi;Pj;s:t:parent(Pi) = parent(Pj) RQ;Pi j=red AR AR;Pj j= Indeterminate I(Pi;Pj) Table 4.13: Reduction Rules. stands for a Permit or Deny. Rule 1 RQ;Pj= 9path = (P;:::;Pn) s.t.81 i < n : P(Pi;Pi+1)^issuerPn = trusted RQ;Pj=auth Rule 2 RQ;Pj= _RQ;Pj= Indeterminate 9path = (P;:::;Pn) s.t.81 < i < n : ( P(Pi;Pi+1)_ I(Pi;Pi+1))^ issuerPn = trusted RQ;Pj=auth Indeterminate Table 4.14: Propagation Rules 4.3 Discussion This chapter presented a proof theoretic semantics for XACML v3.0 using natural deduction rules. These deduction rules closely follow the o cial XACML specification ? in cases of ambiguities, I consulted the public XACML mailing list1. To verify the correctness of my interpretation of XACML, I also used Sun?s reference implementation2 of a XACML policy engine. 1OASIS XACML mailing list is available at http://lists.oasis-open.org/archives/xacml/ 2Project information (including source code) available at http://sunxacml.sourceforge.net 64 The operational semantics is a contribution in itself since it presents a concise, un- ambiguous version of the o cial XACML specification (which, including the Adminis- trative Profile specification, is over 150 pages) and it extends and improves previous work by covering more XACML features and fixing errors from previous semantics proposals (e.g., treatment of Permit-Overrides rule-combining algorithm as discussed in Section 4.2.2). For the purpose of this dissertation, this operational semantics is crucial since it is used to prove the correctness of the Datalog and Description Logic mappings presented in Chapters 5 and 6. 65 Chapter 5 Datalog-Based Theoretical Foundation of XACML The first version of XACML was published in 2003, and since then there has been ongoing work on new versions ? currently, XACML 3.0 [113] is close to standardization. Despite the amount of interest in XACML, the language does not have an o cial formal semantics that could clarify the o cial (informal) language specification and provide a comparison to other formal access control languages. There has been previous work on providing formal treatments of XACML [66, 131, 117, 50, 36], mostly for the purpose of providing analysis services such as formal veri- fication. Additionally, there has been work on providing a formal semantics for an early version of XACML [68], as well as an investigation of the compositional properties of the language [121]. While previous work does provide insight into some formal properties of the language, the following questions have still remained open: What is the complexity of access request checking in XACML (given an access request R and a policy P, determining the access decision of P for R) ? If access request checking is intractable for full XACML, then what are the subsets that make it polynomial? Which language features lead to intractability? How does XACML compare to other logic-based access control languages such as the Flexible Authorization Framework (FAF)? Can we extend XACML with fea- tures from FAF without compromising the worst case complexity of the language? 66 To answer the above questions, in this chapter I present a semantics of XACML based on a variant of Datalog. This formalization covers the latest version (3.0) of the language [113], including its Administrative Policy Profile [114]. Using this semantics, I provide complexity bounds for full XACML and various fragments. Additionally, using this Datalog semantics I discover features of XACML that are underspecified and am- biguous in the o cial specification, such as cyclic references of PolicySets. Finally, using the Datalog mapping I provide a comparison of XACML to other rule-based pol- icy frameworks such as FAF and show how XACML can be extended with features from FAF while preserving the desirable computational properties of Datalog (polynomial data complexity and unique model property). 5.1 Mapping XACML to Datalog This section provides a polynomial time reduction of XACML to the logic pro- gramming language Datalog such that access request checking in XACML is reduced to entailment in Datalog. Using this mapping, I show which fragments of XACML have provably polynomial data complexity and provide a comparison to other Datalog-based policy languages. In this section, I will use a Prolog-like syntax to represent Datalog rules: H0:-B0^:::Bn;c where Bi represents a literal, and c a boolean constraint. Datalog is a well-studied logic programming language [37], with a clear and concise semantics and polynomial data 67 complexity. There is a variant of Datalog that allows limited negation of predicates in bodies of rules, called stratified Datalog ? this variant maintains the desirable computa- tional properties (i.e., unique minimal model and polynomial data complexity) [43]. More information about stratified Datalog can be found in Chapter 2. The mapping takes a policy set PS and request RQ as input and generates a Datalog programP. It is organized as follows: A set of extensional (EDB) predicates is generated to represent the relations be- tween the policies in PS and their child elements. In this step, EDB predicates such as hasRule and hasTarget are instantiated for each Policy element. A series of rules and intensional (IDB) predicates are added to P to represent the semantics of matching access Requests against Targets, and the propagation of access decisions made by Rules to Policies and PolicySets. These first two steps are independent of the request; they are done before the policy is deployed. During runtime, each Request is compiled to a set of extensional predicates and these are added toP. The access decision is retrieved after computing the unique minimal model ofP. 5.1.1 Mapping XACML policy structure to Datalog I assume that each policy element ? not only Rules, Policies and PolicySets but also AttributeDesignators, AttributeSelectors, and all other Target syntax elements ? has a unique ID, so it can be distinguished it from the other elements. For an element P, Pid is used to refer to P?s identifier. 68 To capture the parent/child relationship between policy elements in XACML, facts (binary predicates) are added to the Datalog program. For example, if a Policy P con- tains a Rule element R, then hasRule(Pid;Rid) is added to the Datalog program. To capture these relationships, I start from the root policy element and traverse the whole policy. Given a policy element S which contains of a list of children elements of type Xi: S ::= (Element X1 :::Xn) the following facts are generated: If Xi is a terminal node, then the fact hasXi(S id;Xival) is added where S id is the identifier of S and Xival is the value of the child element. If Xi is non-terminal, then the fact hasXi(S id;Xiid) is added where Xiid is the identifier of the child element Xi. Similarly to above, for a Request R and for each attribute AT in the request, unique IDs are generated. For a Request R and each of its Attribute elements AT, the following predicate symbols are added: hasAT(R-id;AT-id), hasCat(AT-id;cat), hasAttrID(AT-id;attr-id), hasIssuer(AT-id;issuer) and hasValue(AT-id;AV). Example 5.1.1.1 Consider the following Rule element. (Rule () (Target (DisjunctiveMatch (ConjunctiveMatch (Match (AttributeValue 25 integer) (AttributeDesignator subject-cat age integer () false) 69 integer-equal)))) Permit)) Assume that r-id, t-id, dm-id, cm-id, m-id, ad-id are the unique ID?s generated for the Rule, Target, DisjunctiveMatch, ConjunctiveMatch, Match and Attribute- Designator elements above, respectively. The following facts would be added for the Rule: hasEffect(r-id, Permit) and hasT(r-id, t-id), linking the rule with its Target element. To capture the relationship be- tween Target and its children, the following facts are added: hasDM(t-id, dm-id), hasCM(dm- id, cm-id) and hasM(cm-id, m-id). hasValue(m-id, 25), hasValueType(m-id, integer) are added to denote the relationship between the Match element above and its Attribute- Value. Finally, the following relations are added to P to initialize the Attribute- Designator: hasAD(m-id, ad-id), hasCat(ad-id, subject-cat), has-attr-id(ad-id, age), hasType(ad-id, integer), mustBePresent(ad-id, false), hasMatchFcn(m-id, integer-equal). 5.1.2 Mapping Rules, Policies and PolicySets To capture access decisions, I use four intensional (head) predicates (permit, deny, indet, na) for each policy element type. For example, for Rules the following predi- cates are introduced: permitR(?P, ?RQ), denyR(?P, ?RQ), indetR(?P, ?RQ) and naR(?P, ?RQ). The semantics of these predicates is such that inferring P(Rid, RQid) for a rule Rid and request RQid corresponds to Rid;RQid j= in the natural semantics1. I present a translation of the natural deduction rules presented in Chapter 4 to Dat- alog. The mapping consists of three Datalog programs: 1 is shorthand for any one member offpermit, deny, indet, nag 70 A programPR capturing the rules needed to match a Request against a Rule. A Datalog programPP that contains the rules needed to propagate an access deci- sion from Rules to Policies. A programPPS that contains the rules needed to propagate access decisions through Policies and PolicySets. The final result of this translation will be a Datalog programP = PR [PP [PPS s.t. for any policy element P, request RQ and access decision , Pj= P(Pid;RQid)$Pid;RQid j= 5.1.2.1 Matching Requests to Rules For the purposes of matching requests to Targets, the following intensional pred- icates are added: matchAD, matchM, matchCM, matchDM, matchT (indet predicates are added as well). These elements have similar meaning to the e ect predicates used for Rules and Policies; the only di erence being that matchAD in addition to matching it also selects an attribute value from the request, so it is a ternary predicate: matchAD(?AD,?RQ, ?V). All other intensional predicates in this section are binary, having only the matching element and the request as arguments. The Datalog rules that are used to match a request against an AttributeDesignator and a Target are shown in Table 5.1 and 5.2 respectively. Note that fcn(?V;?VM) is the only constraint function that occurs, and is treated as a boolean constraint, i.e., both ar- guments will be ground by the time the fcn is being evaluated. Finally, the rules used to 71 determine the access decision for a Rule are shown in Table 5.3. The Condition element is omitted here since its discussion warrants a separate section (Section 5.1.4). matchAD(?AD;?RQ;?V) :? hasAttribute(?RQ;?AT) ^ hasValue(?AT;?V) hasAttrID(?AD;?id) ^ hasAttrID(?AT;?id)^ hasType(?AT;?type) ^ hasType(?AD;?type)^ hasIssuer(?AT;?issuer) ^ hasIssuer(?AD;?issuer)^ hasCat(?AT;?cat) ^ hasCat(?AD;?cat)^ indetAD(?AD;?RQ) :? :matchAD(?AD;?RQ;?V) ^ mustBePresent(?AD;true): Table 5.1: Matching a request (?RQ) against an AttributeDesignator (?AD) in Data- log. To handle AttributeSelectors, I pre-process the policies in the following way: whenever an AttributeSelector AS encountered used, it is replaced it with a set of AttributeValues that are returned when AS is applied against the request. I use a predicate selected(?AS, ?RQ, ?V), which is instantiated with values (?V) selected when applying the AttributeSelector against the Request ?RQ. Because this operation is request-dependent, it might be considered an overhead at runtime. However, during the normal operation of a XACML engine these evaluations will have to be performed regardless, so I believe that such preprocessing does not add any substantial overhead. Rules 3 and 4 in Table 5.2 capture the semantics of matching AttributeSelectors. The following lemma shows the Datalog mapping of Rules is consistent with re- spect to the XACML semantics presented earlier in this chapter. Lemma 1 For a XACML Rule RQ, a request R, and one of findeterminate, not- applicable, permit, denyg: Pj= P(Rid;RQid)$Rid;RQid j= : 72 matchM(?M;?RQ) :? matchAD(?AD;?RQ;?V) ^ hasValue(?M;?VM); f cn(?V;?VM) = True: indetM(?M;?RQ) :? indetAD(?AD;?RQ) ^ hasAD(?M;?AD): matchM(?M;?RQ) :? selected(?AS;?RQ;?V) ^ hasValue(?M;?VM); fcn(?V;?VM) = True: indetM(?M;?RQ) :? indetAS(?AS;?RQ) ^ hasAS(?M;?AS ): matchCM(?CM;?RQ) :? VMi2CM(matchT(?Mi;?RQ)) indetCM(?CM;?RQ) :? indetM(?M;?RQ) ^ hasM(?CM;?M): matchDM(?DM;?RQ) :? matchCM(?CM;?RQ) ^ hasCM(?DM;?CM): indetDM(?DM;?RQ) :? VCMi2DM (indetCM(?CMi;?RQ)) matchT(?T;?RQ) :? VDMi2T (matchT(?DMi;?RQ)) indetT(?T;?RQ) :? indetDM(?DM;?RQ) ^ hasDM(?T;?DM): Table 5.2: Matching a request (?RQ) against a target (?T) in Datalog. indetR(?R;?RQ) :? indetT(?T;?RQ) ^ hasT(?R;?T): R(?R;?Q) :? matchT(?T;?RQ) ^ hasT(?R;?T)^ hasEffect(?R; ): naR(?R;?RQ) :? :indetR(?R;?RQ) ^ :denyR(?R;?RQ) ^ :permitR(?R;?RQ): Table 5.3: Matching a Request (?RQ) against a Rule (?R) in Datalog. Proof Sketch The proof is fairly simple since the Datalog rules presented in this chapter are a rewrite of the natural deduction rules from Chapter 4. The correspondence between the deduction rules used to infer that Rid;RQid j= and the Datalog rules used to inferPj= P(Rid;RQid is shown in Table 5.4. For brevity, instead of the whole rules, only references to their definitions are provided. Natural Deduction Rule Datalog Rule Rule 1 and Rule 2, Table 4.5 Rule 1, Table 5.1 Rule 4, Table 4.5 Rule 2, Table 5.1 Rule i (1 i 10), Table 4.6 Rule i (1 i 10), Table 5.2 Rule i (1 i 3), Table 4.7 Rule i (1 i 3), Table 5.3 Table 5.4: Correspondence of Natural Deduction rules and Datalog rules for XACML request matching 73 Lemma 2PR is a Datalog program with a unique minimal model and polynomial data complexity. Proof 1 The lemma is proved by showing that PR is a Datalog program with stratified negation. First, notice that in all rules inPR, negated predicates occur only in the body. Second, it can be shown that the negation is stratified by presenting a valid stratification, as presented in Table 5.5. Stratum Predicate 0 hasAttribute, hasT, etc. (EDB predicates) 1 matchAD 2 indetAD 3 matchM, indetM matchCM, indetCM matchDM, indetDM matchT, indetT 4 indetR, permitR, denyR 5 naR Table 5.5: Strata ordering ofPR. 5.1.2.2 Matching Requests to Policies In this section, I show how access decisions are propagated from Rules to Poli- cies. This section is categorized by the type of rule-combining algorithm. Permit-Overrides and Deny-Overrides Note that Permit- and Deny-Overrides are essentially symmetrical in their meaning. Thus, in Table 5.6 I only show one overriding algorithm ? a placeholder variable is used to stand for either Permit or Deny, and ? to stand for the opposite of . 74 P(?P;?RQ) :? hasT(?P;?T) ^ matchT(?T;?RQ)^ hasRule(?P;?R) ^ R(?R;?RQ)^ hasComb(?P; -Overrides): indetP(?P;?RQ) :? : P(?P;?RQ) ^ indetR(?R;?RQ)^ hasT(?P;?T) ^ matchT(?T;?RQ)^ hasRule(?P;?R) ^ hasEffect(?R; )^ indetR(?R;?RQ) ^ hasComb(?P; -Overrides): ? P(?P;?RQ) :? : P(?P;?RQ) ^ :indetP(?P;?RQ)^ hasT(?P;?T) ^ matchT(?T;?RQ)^ hasRule(?P;?R) ^ ? R(?R;?RQ)^ hasComb(?P; -Overrides): Table 5.6: Mapping Permit- and Deny-Overrides rule-combining algorithm to Data- log. First-Applicable Again, is used to stand for Permit, Deny or Indeterminate, to avoid repeating similar rules. Given a policy P with n rules, for each rule at position i, the rule from Table 5.7 is generated. P(?P;?RQ) :? hasT(?P;?T)^matchT(?T;?RQ) ^ hasComb(?P;First-Applicable) ^ hasRule(?P;?Ri)^ R(?R;?RQ) ^V hasRule(?P;?R j);j PPS_A.xml PPS_N.xml Consider what happens if a new PolicySet is added (PPS B), which is associated with people who have activated the roles of both Nurse and Admin. Since doctors inherit the privileges of nurses and admins in this example, they should be able to access this policy set. However, for this to happen, the doctor policy will have to be manually updated 91 and the PPS B set added to its list of references. It is unfortunate that every time a new permission is added, this manual updating is required to make sure the hierarchy still works. Obviously, an automatic approach would be preferred where the policy engine is smart enough to realize that a Doctor role inherits the privileges of both Nurse and Admin, and is therefore able to access PPS B. There is support in FAF for this functionality, using hierarchy predicates. Given my XACML-to-Datalog semantics, these predicates can be added to XACML as well, essen- tially adding a new feature to the language without sacrificing computational properties. Adapting the hierarchy predicates from FAF has to be done at the attribute matching level in XACML, for example: hasAttrValue(role;Nurse) :- hasAttrValue(role;Doctor) hasAttrValue(role;Admin) :- hasAttrValue(role;Doctor) The above rules state that whenever a Request arrives with a value of Doctor for the role attribute, then the engine will automatically infer it has values Nurse and Admin as well, so the permissions written for nurses and admins will be inherited. With this simple addition, added for each role relationship, the policy engine would automatically infer that Doctor has access to PPS B without any need to modify its policy. Other useful feature of FAF is its history table , i.e., a table whose rows describe the access requests processed. A history table can be used to model various policy constraints such as the Chinese Wall security policy, and will not change the computa- tional complexity of XACML if it were added. Additionally, FAF provides other sug- gestions for future extensions of XACML. For example, combining algorithms such as 92 most-specific-overrides and no-overriding can also be easily adapted to XACML: most- specific-overrides can be performed by comparing the Targets of the two policy ele- ments to be combined, whereas for no-overriding a clause can be added to throw Indeterminate whenever conflicting access decisions are returned. The mapping I have presented in this section provides a framework for experimenting with such extensions. 93 Chapter 6 XACML Analysis Services In the previous chapter, I described a formal framework for XACML based on Dat- alog where access request checking was provided in PTIME in the case with no cyclical references between policies. That chapter, however, did not address the lack of support for comparing and debugging policies nor the lack of compile-time services for XACML in general. The following example scenario illustrates some of these services (note that formal verification services were discussed in Chapter 1). Analysis Service Example Consider an access control policy for a bank for this ex- ample. There is a general, high-level access control policy assigned by the bank?s main branch (headquarters), which must be followed by the policy of each branch. Each local branch policy subsumes the general one and extends it appropriately, essentially customiz- ing the general policy for its own needs. The main requirement is that each local policy conforms to the general policy; namely, for any given access request, whenever the gen- eral policy returns Permit (or Deny), the local branch policy should also return Permit (or Deny). This scenario motivates the need for automated policy comparison. Checking policy subsumption, such as in this example, is one type of comparison, others include: checking policy disjointness (i.e., there is no access request s.t. both policies apply) and equivalence (for any access request, both policies will yield the same decision). For large policy sets written in an expressive language, performing these services manually would 94 be very tedious and error-prone, so an automated approach is preferred [118]. Federated Policies Example Continuing on the access control policy of a bank exam- ple, consider what happens when access control is federated across multiple, (to some ex- tent) independent branches of the bank. Each branch might use di erent attribute schemes to describe subjects, actions and resources that comprise its access policy. For example, keeping in mind that XACML is an attribute based language, one bank branch might use a boolean attribute adultAge to represent adult customers, whereas another might use a numeric constraint on an integer attribute age. In a large organization with many di erent departments, reconciling such vocabulary information is non-trivial. Thus, there exists a need for a mechanism that will simplify specification and management of policies from heterogeneous sources - and as importantly, support all of the common analysis services discussed here and in previous work: change analysis (policy comparison), formal verifi- cation and redundancy checking. In this chapter, I present a logic-based analysis framework that can reason about ex- pressive XACML policies and provide services such as above. As a basis for this frame- work I use Description Logics (DL), which are a family of formalisms that are decidable subsets of First-Order logic, and are the formal basis for the Web Ontology Language [45]. Because of the correspondence of policy analysis services to DL reasoning services (e.g., policy comparison can be reduced to concept subsumption, whereas formal verifi- cation can be reduced to concept satisfiability), the framework can leverage o -the-shelf DL reasoners optimized to provide the above-mentioned analysis services. An important benefit of using a logic compatible with OWL is that we can leverage 95 OWL being a W3C standard for representing information on the Web. Thus, I extend previous work of coupling XACML with OWL ontologies [40] by providing a unified reasoning framework about that covers both XACML and OWL. This chapter is organized as follows. In Section 6.1 the algorithm to map a XACML policy set to a Description Logic knowledge base is presented. The mapping covers XACML Policy Elements (PolicySet, Policy, Rule, Target, Request), along with Datatypes and Administrative Policies. Given this mapping, Section 6.2 describes how formal veri- fication, policy compariosn and redundancy checking can be provided. In Section 6.3, the mapping is extended with support for OWL, which in turn provides a semantic extension of XACML (supporting data integration and rich policy models). Finally, Section 6.4 contains a discussion of limitations of the analysis framework as well as a comparison to other analysis approaches. 6.1 Mapping XACML This section will provide details of the mapping of XACML policy elements to Description Logic (DL) concept expressions. At the core of the mapping there are two translation functions. Given a DL KB K, decision type 2fPermit;Deny;Indeterminateg, policy element P 2fPolicySet, Policy; Ruleg, and Target element T, the translation functions are defined as: : T )C : P K)K0 The function ( ;T) takes an access decision and a target element T as input, and 96 returns a concept expression C s.t. whenever the mapping of the access request is of type C, the original request will also yield the access decision when evaluated against T, and vice-versa. The translation function (P;K) takes a policy element P and a DL KB K , and generates axioms in K to capture the semantics of P. More specifically, for each policy element P (Rule, Policy or PolicySet) three DL concepts are introduced: Permit-P, Deny-P and Indeterminate-P. Informally, whenever the mapping of the request is of type -P, that means that when evaluated against P, the original request will return , and vice-versa. In the remainder of this section, I will present formal descriptions of and . First, the translation function will be discussed in detail; I will describe how a XACML access request and a Target are mapped to Description Logics. After that, the presentation will move on to and types of axioms added to the KB to capture the semantics of XACML combining algorithms. After these results for core XACML, I will discuss the more ad- vanced parts of the language (administrative policies, datatypes, hierarchical resources) and their corresponding DL mapping. Note that from now on, unless specified di erently, K is assumed to refer to the DL KB that we?re mapping the XACML policies into. 6.1.1 Mapping Requests XACML access requests represent a conjunction of attribute-value pairs. For illus- trative purposes, an example of a request containing a single subject-id attribute and value is shown below: 97 Julius Hibbert A XACML access request is mapped to a DL concept expression; details of the DL mapping are presented in Table 6.1. Note that no matching functions are allowed in requests, so the only data-type restriction used type-equal. Syntax Mapping RQ ::= (Request ATS ) (ATS1)u:::u (ATSn) ATS ::= (Attributes (AT content) cat) (AT1;cat)u:::u (ATn;cat) AT; cat ::= (Attribute AV attr-ID Issuer) 9r: (typeAV-equal; AV) where r2Rs.t. name(r) = concat( (attr-ID); (Issuer); (cat); (TypeAV)) Table 6.1: Mapping Request to a DL concept expression This mapping is not complete because of the open world assumption present in Description Logics. The following additions to the concept expression corresponding to the request essentially close-o the information carried in a request: 1. To make sure that the request RQ is not augmented with additional attributes (apart from the ones it initially contains), for each attribute A that occurs in the policy P but not in RQ I add: (RQ) (RQ)u8 (A):? 98 2. To make sure that the request RQ is not augmented with additional values for the attribute it already contains, for each attribute that occurs in RQ the following is added: (RQ) (RQ)u=nA , where n stands for the number of distinct attribute values for A that occur in RQ. In a concise format, a full mapping of a Request RQ would be the following: (RQ) AV2RQ 9r AV: (typeAV-equal; AV) u ATis used, which in DL represents the whole interpretation domain, so it will match any possible attribute value. Syntax Elements E Mapping (True;E) T ::= (Target DM ) (True;DMi) DM ::= (DisjunctiveMatch CM+) F (True;CMi) CM ::= (ConjunctiveMatch M+) (True;Mi) M ::= (Match (AV AD fcn)) 9 (AD): (fcn; AV) AD ::= (AttributeDesignator Cat attr-ID r2Rs.t. name(r) = Type Issuer? MustBePresent?) concat( (attr-ID); (Issuer); (cat); (Type)) Table 6.2: Mapping access requests that match Target to a DL concept expression Syntax Elements E Mapping (Indeterminate;E) T ::= (Target DM ) F (Indeterminate;DMi) DM ::= (DisjunctiveMatch CM+) (Indeterminate;CMi) CM ::= (ConjunctiveMatch M+) F (Indeterminate;Mi) M ::= (Match (AV AD MatchFcn)) 8 (AD):? AD ::= (AttributeDesignator Cat attr-ID r2Rs.t. name(r) = Type Issuer? MustBePresent?) concat( (attr-ID); (Issuer); (cat); (Type)) Table 6.3: Mapping access requests that return Indeterminate when matched against Target to a DL concept expression The next lemma states the correspondence between my DL mapping of Target elements and the proof-theoretic semantics from Chapter 4. In particular, the lemma shows that if the mapping of the Request (RQ) is subsumed by the mapping of the Target element (T), then RQ will match T according to the proof-theoretic semantics (and vice-versa). 101 Lemma 6 For a Target element T, and a Request RQ: Kj= (RQ)v (True;T),RQ;Tj= True Kj= (RQ)v (Indeterminate;T),RQ;Tj= Indeterminate (6.2) Proof. The proof of this lemma is in Appendix A. Lemma 7 For a Target element T, and a Request RQ: Kj= (RQ)v: (True;T),RQ;T6j= True Kj= (RQ)v: (Indeterminate;T),RQ;T6j= Indeterminate (6.3) Proof. If case We know that (RQ) v: (True;T). This proof is done by contradiction: as- sume that if (RQ)v: (True;T), then RQ;Tj= True. However, in that case, according to Lemma 6, for the same request the following will hold as well: (RQ) v (True;T). Note that (RQ) cannot be subsumed by both (True;T) and : (True;T) at the same time since I have assumed that (RQ) is satisfiable, so we have reached a contradiction. Thus, Kj= (RQ)v: (True;T),RQ;T6j= True It can be shown for Indeterminate in the same manner. Else case. Else case is more involved, since in DL KB 6j= (RQ) v (True;T) (which can be easily shown) is not the same as K j= (RQ) v: (True;T) (which needs to be 102 shown). The proof can be done by induction on the XACML deduction rules in Section 4.2. The full proof is available in the Appendix. 6.1.3 Mapping XACML Rules For each XACML Rule R, I introduce a Permit-R, Deny-R and Indeterminate-R concept. The general idea is that for a request RQ, if (RQ) is of type Permit-R, then RQ would yield a Permit when evaluated against R (and vice-versa). Rules in XACML consist of an identifier (ID), Target representing the types of request the rule matches, Condition representing additional conditions that need to be satisfied for the rule to fire and an Effect, representing the head of the rule (can be either Permit or Deny). The Permit and Deny concepts for a rule depend on the e ect of the rule itself. For example, for a rule R that yields a Permit, the Deny-R concept will be equal to?, because there cannot be an access request where R will yield a Deny. Assuming there there is no Condition element, the Permit-P concept for R will be equal to the mapping of the Target of R. Definition 5 Mapping a Rule Element. For a rule (Rule ID T Permit), (K;R) is defined as follows: (K;(Rule ID T Permit)) = K[ 8>> >>>> >>>> >< >>>> >>>> >>>: Indeterminate-ID (Indeterminate;TR) Permit-ID (True;TR) Deny-ID ? 9>> >>>> >>>> >= >>>> >>>> >>>; 103 Analogously, for a rule (Rule ID T Deny), (K;R) is defined as: (K;(Rule ID T Deny)) = K[ 8>> >>>> >>>> >< >>>> >>>> >>>: Indeterminate-ID (Indeterminate;TR) Permit-ID ? Deny-ID (True;TR) 9>> >>>> >>>> >= >>>> >>>> >>>; Example 6.1.3.1 I present here a running example (similar to Chapter 1) that will be used to illustrate the main concepts underlying this mapping. In this toy example, initially there are two security roles, Manager and Developer; one resource: Report; and two ac- tions: read, write. The root policy set contains two policy sets which are combined using First-applicable combining algorithm. Assume there are no complicated matching functions; in each Target, the matching function is simply string-equal. The policy is presented in graphical form in Figure 6.1. Figure 6.1: Example Policy 104 The Rules in this example are mapped to: Permit-R1 9role:Manageru9resource:Report u(9action:readt9action:write) Deny-R1 ? Indeterminate-R1 ? Permit-R2 9role:Developeru9action:read u9resource:Report Deny-R2 ? Indeterminate-R2 ? Permit-R3 ? Indeterminate-R3 ? Deny-R3 > Permit-R4 9role:Developeru9action-type:write u9resource:Report Deny-R4 ? Indeterminate-R4 ? For brevity, this example is slightly simplified by omitting the data-type, category and issuer information for each attribute. Lemma 8 For a Rule R and Request RQ: RQ;Rj= Effect ,Kj= (RQ)vEffect-R (6.4) where Effect2fPermit;Deny;Indeterminateg. Proof. Proof can be found in the Appendix. 105 Lemma 9 For a Rule R and Request RQ: RQ;R6j= Effect ,Kj= (RQ)v:Effect-R (6.5) where Effect2fPermit;Deny;Indeterminateg. Proof. If case This proof is done by contradiction: assume that if (RQ) v:Effect-R, then RQ;Rj= Effect. However, in that case, according to Lemma 6, for the same request RQ the following will hold: (RQ)vEffect-R. Since RQ cannot be of type Effect-R and :Effect-R at the same time, we have reached a contradiction. Thus, Kj= (RQ)v:Effect-R)RQ;R6j= Effect Else case. Else case is more involved; the proof is done by structural induction on the XACML semantics rules in Section 4.2, and is available in the Appendix. 6.1.4 Mapping Policies A Policy contains a Target element, a collection of rules, and a rule combining algorithm that specified how the access decision of the children Rules are to be com- bined. For a Policy P, the Permit and Deny concepts have to take into account the Target, and in addition the Permit- and Deny- concepts of P?s children. This is because 106 the access decision a Policy yields depends on the Target and the results of its chil- dren?s decisions. Intuitively, a Permit-P is matched by a request only if P?s Target is matched and at least one of its children?s Permit concepts is matched as well. However, depending on the overriding algorithm, for each child policy element, we might need to make sure that whenever it yields a Permit it will not be overridden by a Deny from a di erent child element. Given these considerations, the mapping function for XACML Policies is developed based on the semantics of the rule-combining algorithms (see Tables 4.8, 4.9, 4.10). In this section, first I discuss the case of Permit-Overrides rule combining al- gorithm: P = (Policy Permit-Overrides T R1;:::;Rn) . The logic axioms that result from the mapping and are added to K are presented in the definition below. The concept Permit-P has somewhat obvious semantics, since we only need to infer that at least one of the child Rules returns a Permit. However, the axiom for Deny-P is not as straightfor- ward, since if a rule returns an Indeterminate, and the e ect of the rule is Permit, then according to the XACML semantics, that rule will override all sibling rules that returned a Deny. Definition 6 Mapping Axioms for P = (Policy Permit-Overrides T R1;:::;Rn) 107 Permit-P (True;T)u 0B BBBB B@ G Ri2P Permit-Ri 1C CCCC CA Deny-P (True;T)u 0B BBBB BB@ G Ri2P Deny-Riu 0B BBBB BB@ R j2P :Permit-Rj 1C CCCC CCAu 0B BBBB BB@ Rk2P; E ectRk =Permit :Indet-Rk 1C CCCC CCA 1C CCCC CCA Indet-P (True;T)u 0B BBBB BB@ G Ri2P;E ectRi =Permit Indet-Riu 0B BBBB BB@ R j2P :Permit-Rj 1C CCCC CCA 1C CCCC CCA (6.6) For Deny-Overrides, the axioms for the mapping concepts are very similar as in the Permit-Overrides case (it is enough simply to swap Permit and Deny in the definitions). Definition 7 Mapping Axioms for P = (Policy Deny-Overrides T R1;:::;Rn) Deny-P (True;T)u 0B BBBB B@ G Ri2P Deny-Ri 1C CCCC CA Permit-P (True;T)u 0B BBBB BB@ G Ri2P Permit-Riu 0B BBBB BB@ R j2P :Deny-Rj 1C CCCC CCAu 0B BBBB BB@ Rk2P; E ectRk =Deny :Indet-Rk 1C CCCC CCA 1C CCCC CCA Indet-P (True;T)u 0B BBBB BB@ G Ri2P;E ectRi =Deny Indet-Riu 0B BBBB BB@ R j2P :Deny-Rj 1C CCCC CCA 1C CCCC CCA (6.7) For First-Applicable, the single axiom states that, for some access decision made by a rule Ri, the parent policy will return that access decision only if all of the rules Rj prior to Ri did not not apply. 108 Definition 8 Mapping Axioms for P = (Policy First-Applicable T R1;:::;Rn) E ect-P (True;T)u 0B BBBB BB@ G Ri2P E ect-Riu 0B BBBB BB@ R j2P :Deny-Rju:Permit-Rju:Indet-Rj 1C CCCC CCA 1C CCCC CCA where i > j; E ect2fPermit;Deny;Indetg (6.8) For Only-One-Applicable, the only way a policy to return a Permit(resp. Deny) is for exactly one rule to apply and return Permit (resp. Deny). In the case when two or more rules apply, Indeterminate is to be returned. Also, if at least one rule returns Indeterminate, then the parent policy will return Indeterminate as well. Definition 9 Mapping Axioms for P = (Policy Only-One-Applicable T R1;:::;Rn) Indet-P (True;T)u 0B BBBB B@ G Ri2P Indet-Ri 1C CCCC CA Indet-P (True;T)u 0B BBBB BB@ G Ri2P; R j2P ((Permit-RitDeny-Ri)u(Permit-RjtDeny-Rj)) 1C CCCC CCA where i , j Permit-P (True;T)u 0B BBBB BB@ G Ri2P Permit-Riu 0B BBBB BB@ R j2P; j,i :Deny-Rju:Permit-Rju:Indet-Rj 1C CCCC CCA 1C CCCC CCA Deny-P (True;T)u 0B BBBB BB@ G Ri2P Deny-Riu 0B BBBB BB@ R j2P; j,i :Deny-Rju:Permit-Rju:Indet-Rj 1C CCCC CCA 1C CCCC CCA (6.9) 109 Lemma 10 For a Policy P and Request RQ: RQ;Pj= Effect , Kj= (RQ)v (Effect;P) (6.10) Proof. Proof can be found in the Appendix. Lemma 11 For a Policy P and Request RQ: RQ;P6j= Effect , Kj= (RQ)v: (Effect;P) (6.11) where Effect2fPermit;Deny;Indeterminateg. Proof. If case This proof is done by contradiction: assume that if (RQ) : :Effect-P, then RQ;P j= Effect. However, in that case, according to Lemma 10, for the same request RQ the following will hold: (RQ) : Effect-P. Since RQ cannot be of type Effect-P and:Effect-P at the same time, we have reached a contradiction. Thus, Kj= (RQ)v:Effect-P)RQ;P6j= Effect Else case. Proof is available in the Appendix. 110 6.1.5 Mapping PolicySets The Permit and Deny concepts for PolicySets are somewhat simpler from the Policy ones. In this section, I present the mappings for DenyOverrides and Permit- Overrides only, since the semantics for the other two combining algorithms is same as in the Policy case. First, I will discuss the case of P = (PolicySet Permit-Overrides T P1;:::;Pn). The mapping axioms that are to be added to K are presented below. Definition 10 Mapping Axioms for PS = (PolicySetPermit-Overrides T P1;:::;Pn) Permit-PS (T)u 0B BBBB B@ G Pi2PS Permit-Pi 1C CCCC CA Deny-PS (T)u 0B BBBB BB@ G Pi2PS Deny-Piu 0B BBBB BB@ P j2PS :Permit-Pj 1C CCCC CCA 1C CCCC CCA (6.12) The axioms for Deny-Overrides are very similar with Permit-Overrides; only di erence is that when a child element returns an Indeterminate, the parent must return a Deny access decision. Definition 11 Mapping Axioms for PS = (PolicySet Deny-Overrides T P1;:::;Pn) Deny-PS (T)u 0B BBBB B@ G Pi2PS Deny-RitIndet-Ri 1C CCCC CA Permit-PS (T)u 0B BBBB BB@ G Pi2PS Permit-Piu 0B BBBB BB@ P j2PS :Deny-Pju:Indet-Pj 1C CCCC CCA 1C CCCC CCA (6.13) 111 Example 6.1.5.1 The policies and policy sets in our running example are mapped below. Note that a) for brevity, I have assumed that 8P : Indeterminate P ?, and b) the targets of all of the policies and policysets in the examples are empty, thus (T;True) > for all of them. Permit-PS 1 >uPermit-P1t(Permit-PS 2u:Deny-P1) Deny-PS 1 >uDeny-P1t(Deny-PS 2u:Permit-P1) Permit-P1 >uPermit-R1tPermit-R2 Deny-P1 >uDeny-R3u:(Permit-R1tPermit-R2) Permit-PS 2 >uPermit-P2 Deny-PS 2 >uDeny-P2 Permit-P2 >uPermit-R2 Deny-P2 >uDeny-R4 Lemma 12 For a PolicySet PS and Request RQ: RQ;PSj= Effect ,Kj= (RQ)v (Effect;PS) (6.14) Proof. Proof can be found in the Appendix. 112 Lemma 13 For a PolicySet PS and Request RQ: RQ;PS6j= Effect ,Kj= (RQ)v: (Effect;PS) (6.15) where Effect2fPermit;Deny;Indeterminateg. Proof. If case This proof is done by contradiction: assume that if (RQ) v :Effect-PS, then RQ;PS j= Effect. However, in that case, according to Lemma 12, for the same request RQ the following will hold: (RQ) v Effect-PS. Since RQ cannot be of type Effect-PS and:Effect-PS at the same time, we have reached a contradiction. Thus, Kj= (RQ)v:Effect-PS)RQ;PS6j= Effect Else case. Else case is more involved; the proof is done by structural induction on the XACML deduction rules in Section 4.2, and is available in the Appendix. 6.1.6 Mapping Administrative XACML The Administrative Policy Profile[113] adds support for administrative/delegation policies to XACML 3.0. In this version of XACML, after a policy element yields an access decision, that decision might need to be authorized by an administrative policy. In contrast, in previous versions of XACML all access decisions were assumed to be 113 authorized by default. An overview of administrative policies in XACML is provided in Section 2.1.3, and the formal semantics is given in Chapter 4. In this section, I will discuss their translation to DL. The mapping uses the same data structure, a reduction graph, as the o cial XACML Administrative Profile Specification. Definition 12 Reduction Graph A reduction graph is a directed graphG=fV;Egwhere each v2V corresponds to a XACML Policy and has four labels: target;issuer, delegate and trusted. For a node v, v:target corresponds to the situation (target) to which v applies, v:issuer holds the attributes that describe the issuer of v and v:delegate contains informa- tion about the issuer to whom v can be delegated. In addition, v:trusted is a boolean field that indicates if v was issued by a trusted issuer. For two nodes v;w that correspond to two sibling policy elements, a directed edge (v;w)2E exists if and only if v:issuervw:delegate. Intuitively, the edges in G indicate whether the issuer and delegate of two policy nodes are compatible. If (v;w) < E, that means it is not possible to reduce an admin- istrative request from v to w. Target elements of each node in the reduction graph are mapped to DL concept expressions in a similar manner as Targets of access policies (presented in Section 5.1). In cases when the node is an access policy, the delegate field is empty. 114 6.1.6.1 Extending the XACML Mapping Permit-P, Deny-P and Indet-P concept definitions are augmented with the con- straints from the administrative policies in the following manner: Permit-P-Auth Permit-Puget admin expr(P;G) Deny-P-Auth Deny-Puget admin expr(P;G) The function get admin expr generates a concept expression that is a disjunction of all unique reduction paths from the current policy (P) to a policy with a trusted issuer. Since according to the o cial semantics of XACML, this is the only way a policy decision can be authorized, the result of get admin expr is added as a constraint to the existing Permit-P and Deny-P concepts. Details of get admin expr are shown in Algorithm 1. The function takes the re- duction graph G and the node corresponding to policy being authorized P as input, and generates a disjunction of all unique possible paths from P to a trusted policy, following the XACML semantics. The algorithm that generates the paths (lines 5-11) performs a depth first search on the reduction graph. It starts with the policy being authorized, and tries to build a path consisting of administrative policies to a trusted node, accumulat- ing constraints along the way. These constraints come from the Target elements of each administrative policy, since administrative policies can restrict the cases where they are applied. When the accumulated constraints become unsatisfiable at a point in the path, the algorithm backtracks and tries a di erent node. All unique paths are added to the Permit-P-Auth or Deny-P-Auth concept. 115 Algorithm 1 get admin expr(node;G) Input: node: node in graph corresponding to input policy G: reduction graph of composed of node?s sibling policies Output: b: returns an expression that corresponds to all possible ways node can be authorized 1: paths [] 2: if node has trusted issuer then 3: paths.add(constraint) . found a new path, remember constraint 4: else 5: for nbor in n.getnbors() do 6: if !nbor.getVisited() and constraintunbor:target6j=? then 7: nbor.setVisited(true) 8: searchGraph(nbor;constraintunbor:target; paths) 9: nbor.setVisited(false) 10: end if 11: end for 12: end if 13: result ? 14: for expr in paths do 15: result resulttexpr 16: end for 17: return result 6.1.7 XACML Datatypes and Functions XACML supports the XML schema data-types and in addition it defines four data- types of its own: ipAddress, dnsName, rfc822Name, x500Name. As part of the process- ing model, it also supports a wide variety of functions over these datatypes, ranging from comparison, arithmetic, regular expression and Xpath matching to higher order map func- tions. In this section I will discuss how these datatypes and functions are handled by this XACML-to-DL mapping. Datatype Support in Description Logics Horrocks and Sattler [64] presented an ap- proach of combining DLs and types systems that allows for deriving new datatypes from 116 existing ones. DLs already provide support for the various datatype comparison func- tions in XACML (such as datetime-greater-than) by way of user-defined XML schema datatypes. This support is currently being standardized in OWL 1.1 [105] and is imple- mented in Fact++ and Pellet. User-defined (restricted) datatypes are supported through the datatypeRestriction constructor, which creates a restricted range by applying a facet to a particular data range. Built-in XML schema facets include: length, minLength, maxLength, pattern, minInclusive, minExclusive, maxInclusive, maxExclusive, totalDig- its, and fractionDigits. These facets cover the numeric and non-numeric comparison func- tions in the XACML specification (Appendix A.3 in [113]). Since DL reasoners such as Pellet[109] and Fact++[120] already have built-in reasoning support for XML schema datatypes, mapping the encountered datatypes at- tribute values in XACML is trivial: for each datatype attribute value I create the same datatype value in the DL KB. Given this, the mapping supports the following XML schema datatypes: string, boolean, integer, double, time, date, datetime, anyURI, hexBi- nary and base64Binary. More detailed information about the mapping is presented in Table 6.1.7. For brevity, the table only contains integer datatypes; comparison functions involving the other XML schema datatypes can be mapped in the same manner. Since the OWL func- tional syntax is already standardized for user-defined datatypes, it is used instead of a more concise DL syntax. For a XACML attribute matching function f cn, attribute a, and value v, I map a to a DL datatype role and map v to a datatype value (with the appropriate type) in the KB. In addition to the above unary datatype predicates, some DL reasoners also support 117 Matching function f cn (AV;fcn) type-equal DatatypeRestriction (type valueAV) type-greater-than DatatypeRestriction (type minExclusive valueAV) type-greater-than-or-equal DatatypeRestriction (type minInclusive valueAV) type-less DatatypeRestriction (type maxExclusive valueAV) type-less-than-or-equal DatatypeRestriction (type maxInclusive valueAV) type-regexp-match DatatypeRestriction (type pattern valueAV) xpath-node-match DatatypeRestriction (xpath-expression pattern valueAV) Table 6.4: Mapping matching functions. more advanced datatype functions such as n-ary datatype predicates. For example, the DL reasoner RacerPro [124] supports natural numbers, integers, reals, complex numbers and strings. The types of predicates supported are shown in Table 6.1.7. The predicates below can capture a subset of XACML?s functions; e.g., linear inequality predicates cover the XACML integer comparison and arithmetic functions. Datatype Domain Predicates N linear inequations with order constraints and integer coe cients Z interval constraints R linear inequations with order constraints and rational coe cients Strings equiality and inequality Table 6.5: Predicates supported by Racer (table taken from RacerPro user guide [82]). Example 6.1.7.1 Mapping the XPath-Node-Match Function. The xpath-node-match function is used to write policies that apply to multiple nodes. This function is used as part of the ResourceMatch object, as shown below: /md:record In the above example, both the attribute value of resource:xpath and ?/md:record? are treated as XPath expressions; the matching succeeds i the at least one of the nodes selected by ?/md:record? matches at least one node selected by the ResourceAttribut- eDesignator. A resource match element with an attribute value of AV, an attribute ID of AttrID and an xpath-node-match function would be mapped to9 (AttrID): (AV), where (AttrID) generates a DL role to correspond to the attribute. To map AV, I generate a unary predicate in the XPath concrete domain. Note that I am able to use XPath data-types in the static analysis framework since it was shown in [55] that the XPath fragment covered by XPAT H is closed under negation and the problem of satisfiability of a conjunction of predicates is decidable. A prototype XPath reasoner (developed by Geneves et al. [55]) was used as a data-type reasoner for the purpose of my analysis framework. 6.1.7.1 AttributeSelector Another element of XACML that warrants discussion in this section is the Attribute- Selector, which selects attribute values from a request (similarly to an Attribute- Designator). The main di erence is that the AttributeSelector uses an XPath ex- pression to locate the attribute value in the request. Consider the following example: 119 application=webservicesJwsSimpleEar, contextPath=/jws_basic_simple, webService=SimpleSoapPort In this case, the expression in RequestContextPath is applied against the XML content element that is piggybacked on the access request and a bag of values is returned. The match is successful if at least one of the returned values matches the above attribute value. A resource match element with an attribute selector (with an xpath expresion X) and an attribute value AV is mapped to the following DL expression: 9 (Attr-ID):PAV, which looks the same as the mapping for xpath-node-match. However, note that there might be some interaction (e.g., subsumption, disjointness) between the di erent xpath expressions used as in the attribute selectors. As an example, consider the following two attribute selectors: In this case, the first expression selects all descendants of the root node that are of type Role, whereas the second expression will select all Role descendants of root, and 120 additionally the root itself, if it is a Role node. The result set of the second expression will always subsume the result set of the first one - this type of relationship will not be captured by the mapping described above. To capture these subsumption relations between Attribute Selectors, I pre-process the policy set, and for each pair of Selectors I compare their XPath expressions using an XPath reasoner [55]. Then, if there is a subsumption, i.e., the expressions in AS 1 and AS 2 subsume each other, I add the following axiom in the DL KB: (AS 1)v (AS 2) 6.2 Services This section will discuss the analysis services provided by the DL mapping de- scribed in the previous section. 6.2.1 Formal Verification Formal verification is the most commonly o ered analysis service for access poli- cies. In most previous work, the security property to be verified is specified program- matically using the particular analysis tool?s API, thus requiring users to be familiar with the internals of the tool. My approach, on the other hand, allows users to specify their security properties in XACML and also presents the verification results back in XACML. To accomplish this, the verification service is exposed as an adaptation of the well known software engineering technique of unit testing. 121 Traditional unit testing applied to policies amounts to users creating an access re- quest (the unit test) and specifying its expected value (Permit, Deny, NotApplicable or Indeterminate). Then, whenever changes are made to the access policy, all of the test requests are run against a XACML engine to make sure no bugs (security holes) are intro- duced. However, writing such unit tests in this manner is tedious and error-prone, since it is di cult to think of all possible conditions that need to be tested. Consider our running example (Figure 1.1 in Chapter 1): it could happen that a user logs in with both a de- veloper and a manager role ? activating both of these grants him write access to reports. Since the unit test I used in the example in Chapter 1 only tests for a request containing the developer role by itself, this violation will not be caught. A verification-based approach to testing overcomes the above limitations. Instead of taking the access request literally and performing a shallow test based on the explic- itly mentioned attributes in the request, the verification approach proposed in this thesis attempts to build a logic model where the attributes in the original request produce a test failure. While building this model the DL reasoner explores all possible combinations of additional attributes in the request that could lead to a test failure. The test condition holds only when such a model cannot be built. The input for this service consists of a XACML policy file P (for the access policy being tested), a XACML file that contains the test condition T, and a string denoting the type of test condition. Supported types of properties are alwaysPermit, alwaysDeny, neverPermit and neverDeny - these are similar to assertions for unit tests. Details on how these are reduced to entailment checking in Description Logics are presented in Table 6.2.1. If the policy fails, output is in the form of a XACML access request, which consists 122 of the counter example that brings about the test failure. Type of Property Entailment Check alwaysPermit (T:target)u:Permit-P j=? alwaysDeny (T:target)u:Deny-P j=? neverPermit (T:target)uPermit-P j=? neverDeny (T:target)uDeny-P j=? Table 6.6: Mappings of Common Types of Policy Tests. T refers to the test policy (containing the security property) and P refers to the top level policy set. Property holds if and only if the entailment holds, i.e., the concept expression is not satisfiable. 6.2.1.1 Tracing In cases when the test fails, the analysis framework extracts the counter example directly from the logic model, maps it back to XACML and presents it as an access re- quest. The procedure that extracts a counter-example XACML policy from a DL concept expression is shown in Algorithm 2. However, with large policy sets, it can be di cult to find out exactly which policy elements were responsible for the error. For this purpose, I provide a ?stack trace? output of every policy that was fired while generating the counter example. Generating the trace is straightforward, assuming the counter example XACML request is available - the re- quest is run against the policy using a XACML engine (Sun?s reference implementation1 is used), and the access decisions at each policy element are stored. 1http://sunxacml.sourceforge.net 123 Algorithm 2 extract request(x) Input: x: individual used generated to check satisfiability of concept Output: LAT : list of attributes and values that represent a valid XACML Request 1: if type expressions of the form9P:Q2L(x) then 2: for each9P:Q2L(x) do 3: P= getAttribute(P) . from the name of the DL role P we retrieve the important attribute information:category, issuer, ID and datatype 4: V= getValue(Q) . if Q is a datatype predicate that maps to multiple values, then a value is randomly selected from the value space characterized by Q 5: LAT = LAT [(P;V) 6: end for 7: else . no9P:Q occur in concept expression 8: Select a DL role P corresponding to a attribute in the policy s.t. L(x)\9P:Q is satisfiable 9: P= getAttribute(P) . from the name of the DL role P we retrieve the important attribute information:category, issuer, ID and datatype 10: V= getValue(Q) . if Q is a datatype predicate that maps to multiple values, then a value is randomly selected from the value space characterized by Q 11: LAT = LAT [(P;V) 12: end if 13: return LAT 6.2.2 Policy Comparison The Permit-P and Deny-P concepts defined previously allow us to easily compare the behaviors of two policies. For example, we can check for policy subsumption: P2 subsumes P1 i if whenever P1 produces access decision , P2 also yields the same ac- cess decision. We can restrict our attention to Permit, Deny or both. In my framework, policy subsumption is reduced to checking subsumption between the Permit and/or Deny concepts. For example, to check if P2 subsumes P1 w.r.t Permit, we ask the DL reasoner if Kj= Permit-P1 vPermit-P2. To illustrate the service, consider adding a new role , LeadDeveloper, to our run- ning example. The updated policy now contains an additional Rule (R3): 124 Figure 6.2: Updated Policy (with LeadDev role) To check whether we have given any unintended access to the other roles, we use the policy subsumption algorithm, that is, we generate the following concept expressions: Permit-PSold;Deny-PSold and Permit-PSnew;Deny-PSnew. Subsumption holds only if both of the following hold: Permit-PS old vPermit-PS new Deny-PS old vDeny-PS new The analyzer reports the first subsumption holds , which is rather obvious from since the Rule added in PS new yields a Permit). However, the analyzer reports subsumption does not hold w.r.t. Deny. In cases of non-subsumption, it is useful to know what are the counter examples, i.e., to show the user a request where PS new and PS old would yield di erent decisions. Since I use a tableau-based DL reasoner for policy analysis, to check whether Av B, the reasoner tries to build a model for Au:B. If a model can be built, it means the subsump- 125 tion does not hold. In that case the model that was just built can easily be extracted from the internals of the reasoner and used as a counter example. Here we get a number of counter-examples: 1) role=LeadDev, action=read, resource=report, action=write, resource=report 2) role=LeadDev, action=write, resource=report 3) role=LeadDev, role=Developer, action=write, resource=report The first two are expected (because of the new Permit rule), however the third counter example represents a potentially dangerous access leak to a person who is a mem- ber of role Developer. It is possible to fix this bug by adding a separation of duty con- straint for the roles of Developer and LeadDev. The constraint is presented below, in DL syntax. 9role:LeadDevv:9role:Developer Note that separation of duty constraints can also be serialized in XACML. To ac- complish this, a new Policy should be created, having the two disjoint roles in its Target. Since we want to prohibit a requester that has both of the roles, the e ect of this new is Deny. Finally, this new policy needs to be set with highest priority (e.g., add it at the beginning of the root policy set and use First-Applicable algorithm) to ensure that the separation of duty constraint can never be overridden. The technique used for policy subsumption can be generalized to policy compari- son. For two policies P1 and P2, we first specify the access decisions we are interested in 126 (say, Deny for the first policy and Permit for the second), and then check satisfiability of the corresponding concept expressions for those decisions : Deny-P1uPermit-P2 If the above expression is not satisfiable, then there cannot be an access request s.t. the first policy yields a Deny and the second one yields a Permit. If it is satisfiable, there is such a request, and we can extract the counter example from the reasoner. To get all counter examples, we need to retrieve all consistent models that the concept expression admits; this involves saturation of the tableau, a technique for which DL reasoners are not particularly optimized. Change verification was introduced in [50], and I show here that it can be accom- plished in DL as well. Because the policy di erences are expressed as concept descrip- tions, performing verification of changes is no di erent than performing verification of policies themselves. The safety properties to be verified are simply added to the change expression. For example, if we want to verify that all changes from Permit to Deny in the above policy involved the LeadDev role, we could test the following concept expression: map(Permit-PS old)umap(Deny-PS new)u8role::LeadDev 6.2.3 Redundancy Checking Another service provided by the analysis framework is finding redundant Rules2. A redundant rule is one that whenever fires, it is always overridden by some other rule or policy with higher priority. A simple way to check redundancy of a rule r is to perform 2The technique can be easily generalized to Policies or PolicySets ? for brevity I focus on Rules only. 127 Algorithm 3 is redundant(r;D) Input: r = (ID T ): XACML Rule Output: b: returns true if r is redundant, false otherwise 1: J ? 2: rold r . cache r 3: while r , null do 4: for policy element q s.t. q , r and q:parent = r:parent do 5: if overrides(Permit;q;r) then .Permit decision of q overrides r 6: J JtPermit-q 7: end if 8: if overrides(Deny;q;r) then .Deny decision of q overrides r 9: J JtDeny-q 10: end if 11: end for 12: r r:parent 13: end while 14: if rold:targetv J then . request is subsumed 15: return true 16: else 17: return false 18: end if change impact analysis for a policy with and without the rule. Here I present a more guided approach for checking redundancy, by building a concept expression that ignores the policy elements that cannot override the rule being checked. Algorithm 3 contains the pseudo-code. The function starts with an input Rule r and works its way up to the root policy element. At the same time, it builds a disjunction that consists of the concept expressions for every Policy or PolicySet that can override the access decision made by r. In line 5, overrides(Permit;q;r) functions returns true if when q yields a Permit decision, it will always override the decision made by r (no matter what it is). If r is subsumed by this disjunction of overriding policies, then the access decision of r will always be covered by 128 some policy element. In this case, r is redundant. Redundant rules do not have to be evaluated, and can be safely removed from a policy file. This simplifies the policy and improves runtime performance of the policy evaluator because there are less rules to match requests against. Please note that in a policy set, there may be multiple possible minimal non-redundant subsets. As an example, consider a policy set containing of three policies: P1 applies to Students of GraduateStudents, P2 applies to GraduateStudents of Professors, and P3 ap- plies to Professors or Students. In this example,fP1,P2gandfP2,P3gare minimal redun- dant subsets. To find such minimal redundant subsets, a modified version of the minimal set cover algorithm can be used, which is NP-complete. Finding and evaluating minimal redundant subsets of a policy set is not handled by my thesis, although it is an interesting area of future work and is discussed in Chapter 9. 6.3 Analyzing Heterogeneous XACML Policies Given that one of the crucial requirements for this analysis framework was rea- soning about heterogeneous policy domains, in this section I will show how this can be accomplished by leveraging Semantic Web technologies. Recently, there has been a great amount of interest in extending the expressive power of XACML with Semantic Web technologies [40, 41, 21] for the purposes of het- erogeneous policy integration. This is because the Semantic Web provides a data sharing and re-use framework for applications across enterprise and community boundaries. One of the foundational languages of the Semantic Web is the Web Ontology Language (OWL) 129 [45], which is a W3C standard for representing shared information. Previous work has focused on extending XACML with support for rich ontology- based models representing subject and resource information. These extensions were ac- complished by adding new matching functions and extended conditions to refer to the background ontologies. While these extensions do increase the expressive power of XACML, they do not o er analysis support for such ontology-extended XACML poli- cies. In this section, I will present a generalization of previous work by providing a unified formal framework for OWL ontology-extended XACML policies. To add the functionality, I extend the XACML policy syntax with a new matching function, called ontology-match. Following is an example of a Match element with a semantic-match function. http://policy#Administrator The semantics of the above extension is explained here: consider that we have already mapped the policy set P to DL using the above mapping , so there exists a DL KB K that contains the mapped concepts for each policy element in P and the request is mapped to a DL individual i in K . Given this, the Match element M above is mapped to a triple: (i (ATADM ) (AVM)) where i is the individual corresponding to the request, (ATADM ) is the DL role corresponding to the attribute id, and (AVM) is the individual 130 corresponding to the attribute value. Then, to check if the ontology-match applies, we simply check if: Kj= (i (ATADM ) (AVM)) The ontology-match function extends XACML with support for expressive policy vocabularies based on OWL ontologies. Given the XACML mapping to Description Log- ics (DL) provided in this section, and the fact the semantics of OWL is grounded in DL, it follows that all of the analysis services described in this section can be seamlessly ap- plied to ontology-extended XACML policies as well. To the best of our knowledge, the DL mapping provided in this paper combined with the ontology-based XACML extension discussed above is the first unified analysis framework that can reason about XACML ex- tended with ontology support. Following I will discuss how some common policy idioms that are not easily expressible in XACML can be captured in these ontology-based policy models. 6.3.1 Representing Policy Idioms In this section, I will discuss how a domain ontology can be used to provide seman- tic descriptions for the entities used in the access policy. For the policy in our running example, we could develop an ontology that describes the company domain, and link the policy entities with concepts in the ontology using subclass relationships. For example, we can state that a Manager is of type Employee who is a boss of at least one Person: ManagervEmployee u9boss:Person 131 Using such ontologies, I show how common policy idioms can be expressed in De- scription Logics. DL syntax is used for brevity, but the following can be easily serialized in OWL: 1. Role hierarchies are easily captured with subclass axioms. For example ,stating that a LeadDeveloper inherits all of the access privileges of the Developer role can be expressed as: 9role:LeadDeveloperv9role:Developer 2. Hierarchies on Attributes, can be captured using property hierarchies in DL. For example, to state that if a person is a CIO of a company, that means he is also an employee of that company, we write: CIO-o f vemployee-o f 3. Separation of duty constraints can be captured with disjoint axioms. To state sepa- ration of duty for two role types A and B, we use: 9role:Av:9role:B 4. Cardinality constraints can be expressed on any given attribute. To state that the role attribute cannot have more than k values, we can write: k role:>v? We can even specify maximum number of users that a role can have, with a combi- nation of inverses and cardinality constraints. For example, the following says that a role cannot have more than k users: 132 k role :>v? 6.4 Discussion This chapter provided a framework for practical analysis services for XACML based on a mapping to Description Logics. Using this mapping, I showed how formal verification, change analysis and redundancy checking can be provided. The mapping covers XACML v3.0 including delegation policies and attribute matching functions using datatypes. Additionally, I showed how the framework can also reason about ontology- extended XACML policies, which have attracted attention in previous work. One issue not fully covered in this chapter is all of XACML?s 200+ datatype func- tions (I showed how subsets of these functions can be handled using OWL-DL datatypes). Because of the expressiveness of the functions in XACML, covering all of them can easily lead to undecidability. For example, using only the following three functions: urn:oasis:names:tc:xacml:1.0:function:integer-multiply urn:oasis:names:tc:xacml:1.0:function:integer-add urn:oasis:names:tc:xacml:1.0:function:integer-equal it is possible to construct a system of non-linear Diophantine equations, which have been shown to be undecidable. Thus, there cannot exist a sound, complete and terminating reasoning procedure that covers all XACML functions. Note that in this chapter, I showed how there exists a mechanism that allows us to couple data-type reasoners with Description Logics reasoners. My implementation of a XACML analyzer, does not provide a separate data-type reasoner for all possible 133 decidable data-type domains; instead, it is designed such that XACML developers can extend it with their own specific data-type reasoners. The only restriction to keep in mind is that the data-type domain has to be closed under negation and there needs to be an algorithm that checks for satisfiability of arbitraty conjunctions of predicates in the domain. Another valid question is how OWL-DL reasoners fare as XACML policy engines. Description Logics su er from bad worst case complexity - even the limited subset we need for this mapping (ALCQ) is EXPTIME. This seems significantly worse than the polynomial data complexity of the formalization in the previous section - however, dif- ferent problems are tackled this section. In the previous chapter, the main problem we investigated was access request checking - which is done at run-time, so fast performance is crucial. The services discussed in this section are meant to be performed at compile- time, before the policies are even used, so I assume that the performance requirements for my analysis tool are not as stringent. Given this, the empirical evaluation described in Chapter 8 shows that OWL-DL reasoners are surprisingly e cient at reasoning about XACML policies, and are comparable even to binary decision diagram (BDD)-based pol- icy engines. 134 Chapter 7 Formalizing and Analyzing Web Service Policies So far in thesis, the formal methods and techniques have been applied to access control (authorization) policies only. This chapter generalizes the approach by applying it to a di erent domain: web service policies. In the web services (WS) domain, WS-Policy [129] has emerged as a standard for specification of constraints and capabilities (i.e., policies) of WS clients and service providers. In WS-Policy, a policy is defined to be a collection of one or more assertions; WS-Policy defines operators that build policy expressions on top of these assertions. A policy assertion represents an individual requirement placed on a web service - it contains domain-specific information (e.g., a client needs to use a particular encryption in order to be able to access the web service). Specifying syntax and semantics for assertions is not covered by the WS-Policy standard. WS-XACML [95] provides an expressive, domain-independent language for spec- ification of WS-Policy assertions. WS-XACML is a profile of XACML: it essentially specifies ways to use XACML in the context of web services for authorization, access control and privacy policies. While WS-Policy provides the processing model and opera- tors for combining individual assertions, WS-XACML provides a language for specifying the assertions themselves. WS-Policy and WS-XACML provide a run-time model for matching policies and 135 assertions, respectively. However, there is no defined ?compile-time? support for analyz- ing and debugging web service policies. Similarly to the XACML issues, because of the expressiveness of WS-Policy and WS-XACML, it is non-trivial for a policy developer to understand the implications of all of the policies in the system. Mapping both WS-Policy and WS-XACML languages into the same background formalism could potentially pro- vide the first static analysis and verification tool that covers both languages. Additionally, by providing a formal foundation for these policy languages it is possible to acquire a clear semantics, as well as a good sense of the computational aspects. It was shown in Chapters 5 and 6 how a logic-based formalization of policy lan- guages (XACML) can provide a theoretical and practical foundation for static analysis of access control policies. In this chapter, the analysis framework is applied to web service policies by presenting an OWL-DL mapping for both WS-Policy and WS-XACML. The mapping is built on top of the XACML transformation described in Chapter 6, and it pro- vides the same services: consistency checking, policy verification and policy comparison (containment). Organization of this chapter is as follows: Section 7.1 presents the WS-Policy to OWL-DL mapping. This includes discussion of the WS-Policy operators (wsp:ExactlyOne and wsp:All), the operations supported (merge and intersection) along with the analysis services provided by the mapping. The second half of this chapter provides a similar treatment for WS-XACML: the syntax and semantics of the language is presented in Sec- tions 7.2.1 and 7.2.2, and the OWL mapping is shown in Section 7.2.3. Finally, in Section 7.3 I show how both of the mappings can be integrated in a single reasoning framework where WS-Policy specifies the high-level processing model for policies and WS-XACML 136 specifies individual policy assertions. 7.1 WS-Policy WS-Policy provides a general purpose model and syntax to describe the policies of a Web service. It specifies a base set of constructs that can be used and extended by other Web service specifications to describe a broad range of service requirements and capabilities. This section will present the WS-Policy mapping to OWL-DL that allows us to use o -the-shelf OWL editors and reasoners to do policy administration and processing tasks. 7.1.1 Mapping WS-Policy Operators to OWL-DL In this section, I present a formalization of the WS-Policy constructs by mapping a normal form policy expression to OWL class expression. A policy in a normal form is represented as an XML document, where a root Policy element enumerates each of its alternatives, and each alternative in turn enumerates its assertions. Following is a schema outline for the normal form of a policy expression: [ [ ]* ]* Listing 1. Normal form of a policy expression 137 Policy expressions can also be represented in more compact forms, using additional operators such as wsp:Optional, however as shown in [129] the policy expressions can all be expanded to normal form. Therefore we only provide a mapping of the constructs used in a normal form policy expression: wsp:ExactlyOne and wsp:All. First, policy assertions are mapped directly into OWL-DL class expressions. In- stead of mapping separately each domain-specific assertion language into OWL, I provide a mapping of domain-independent WS-XACML instead. The mapping of WS-XACML is discussed in Section 7.2. Mapping wsp:All to OWL is straightforward because wsp:All means that all of the policy assertions enclosed by this operator have to be satisfied in order for commu- nication to be initiated between the endpoints. Thus, it is a logical conjunction and can be represented as OWL intersection. Each of the members of the intersection is a policy assertion, and the resulting class expression is a custom-made policy class that expresses the same semantics as the WS-Policy one. Because the description of wsp:exactlyOne in the WS-Policy specification is am- biguous, there are here are two possible interpretations for the operator: wsp:ExactlyOne as an exclusive OR wsp:ExactlyOne means that only one, not more, of the alternatives should be supported in order for the requester to support the policy. This is supported by the o cial specification[129], where it is stated that although policy alternatives are meant to be mutually exclusive, it cannot be decided in general whether or not more than one alternative can be supported at the same time. To cover this more com- plicated case, I translate Wsp:ExactlyOne in the following way: for n di erent policy 138 WS-Policy Construct OWL Expression Wsp:All (policies A and B) owl:intersectionOf(A B) Wsp:ExactlyOne intersectionOf( (policies A and B) complementOf(intersectionOf(A B)) unionOf(A B) ) Table 7.1: Mapping of WS-Policy Constructs to OWL assertions, expressed as OWL classes themselves, wsp:ExactlyOne is the class expres- sion consisting of those individuals in each separate policy class that do not also belong to another policy class. In OWL terms, it is the union of all of the classes with the complement of their pair-wise intersections. Because of the pair-wise intersections there is a quadratic increase in the size of the OWL construct that is used as a mapping for wsp:ExactlyOne. wsp:ExactlyOne as an inclusive OR However, due to the open world assumption present in OWL-DL, the above mapping produces non-intuitive results. For example, if a request r comes in such that r : A, and the policy P contains only two alternatives, A and B, we will not be able to infer that the request r satisfies P (i.e., r is of type (AtB)u:(AuB)) unless we explicitly state that r ::B. To overcome this issue, I o er a simplified mapping to represent as logical disjunction (inclusive OR), and in addition I have made the classes representing the alternatives pair-wise disjoint, so even though a requester supports more than one alternative, he cannot use more than one at a time. This updated translation is more concise than the one presented above (compare At B with (At B)u:(Au B)). In this scenario, if a requester comes in that is a member of two alternatives, a logical inconsistency will occur. 139 (01) (02) (03) (04) (05) (06) (07) (08) (09) (10) (11) (12) Figure 7.1: Example policy Example 7.1.1.1 Consider the example policy in Figure 7.1. For each policy assertion, a separate OWL class (RequireDerivedKeys, WssUsernameToken10, WssUsernameTo- ken11) is generated. Then, each alternative is simply the conjunction of its constituent assertions. Alt1 RequireDerivedKeysuWssUsernameToken10 Alt2 RequireDerivedKeysuWssUsernameToken11 Finally, the policy class P is equivalent to the disjunction of the alternative classes: P Alt1tAlt2 If, for example, these two alternatives have to be disjoint, then a disjoint axiom is added: Alt1 v:Alt2. With this mapping, checking whether a web service requester satisfies a particular policy can then be reduced to instance checking: simply checking whether the OWL in- dividual representing the requester is a member of the OWL class representing the policy. 140 To more compactly express complex policies, WS-Policy allows nesting of opera- tors. To convert a policy from a compact to a normal form, the properties of wsp:ExactlyOne and wsp:All can be used. To show that the OWL translation correctly captures the meaning of wsp:ExactlyOne and wsp:All, I need to prove that the mappings from Table 7.1.1 have the same properties as the WS-Policy operators. wsp:ExactlyOne and wsp:All have the following properties: commutativity, associativity, idempotency and distributivity. It can be easily shown that the logical constructs corresponding to wsp:ExactlyOne and wsp:All, which are essentially a logical conjunction and disjunc- tion, also satisfy these properties. 7.1.2 Mapping Policy Assertions to OWL Web Services Policy assertions indicate domain-specific capabilities and require- ments and are defined in separate specifications.The WS-Policy standard does not define the syntax and semantics of assertions - this task is delegated to experts in their respective domains. Recently, there has been a proposal of a generic, domain-independent policy lan- guage that is able to capture the above domains. The proposal is WS-XACML, and it uses a subset of the functions of core XACML. Instead of formalizing and analyzing all of the domains separately, this chapter provides a mapping of domain-independent WS- XACML. The mapping is presented in Section 7.2. 141 7.1.3 WS-Policy Merge and Intersection As part of the specification, WS-Policy also defines two operations on policies: merge and intersection. Merge Merge is the process of combining sub-policies together to form a single pol- icy. This operation is needed because a policy might be specified in a distributed way, having its fragments defined in separate files. It is necessary to combine all these policy fragments together to form a single merged policy which could be processed further. Merge works on policies already converted to normal form. The merged policy is a Cartesian product of the alternatives in the first policy and the alternatives in the second policy. There is a straightforward way of doing the Merge operation in OWL-DL. First, we translate each of the input policies into OWL-DL as described above. Then, the merged policy is simply the intersection of the input policies. Thus, Merge also maps cleanly onto OWL-DL. An outline of the proof is shown in [84]. Intersection Policy intersection is used when a web service requester and provider both express policies and want to compute the compatible policy alternatives between them. Like in Merge, the process of coming up with an intersection is carried out in a cross product fashion, comparing each alternative from the first policy with every alternative from the other one. However, in the case of Intersection, if the two alternatives that are being combined do not agree on the same vocabulary, then the combined alternative is not added to the new policy. A vocabulary of an alternative is simply defined as the set of QNames of the assertions in that alternative. If the alternatives do agree on the same 142 vocabulary, then as defined in [129], two alternatives are compatible if each assertion in the first alternative is compatible with an assertion in the second, and vice-versa. Checking whether two assertions are compatible is outside of the scope of WS- Policy. To overcome this, I use WS-XACML to represent the individual policy asser- tions, since WS-XACML defines a processing model that checks if two assertions are compatible. More information is presented in Section 7.2. 7.1.4 Policy Processing One benefit of expressing policies using OWL is the ability to reason about policy containment - i.e., checking if the requirements for supporting one policy are a subset of the requirements for another. That would allow us to be more flexible in determining whether a particular requester supports a policy, in the cases where the requester supports a superset of the requirements established by the policy. Policy containment is only one of the services supported out of the box; a full listing follows: 1. policy equivalence (A owl:equivalentTo B); 2. policy incompatibility (if x meets policy A then it cannot meet policy B; a.k.a, A owl:disjointWith B); 3. policy incoherence (nothing can meet policy A; a.k.a., A is unsatisfiable) 4. policy conformance (x meets policy A; a.k.a, x rdf:type A) 5. policy containment (if x meets policy A then it also meets policy B; a.k.a., A rdfs:subClassOf B); 143 There is an additional reasoning service that is useful for policies and warrants more discussion. It can been argued that explanation is a crucial requirement for a policy lan- guage. To address this requirement, we can use recent advances in the field of debugging OWL ontologies [80], esp. in providing explanations for both ontology inconsistencies and arbitrary entailments for OWL-DL. For example, if a user asks why the requester r satisfies (or does not satisfy) the policy P, then the debugging framework is simply asked to provide justification for the type assertion r:P. On the other hand, if a web service request causes an inconsistency (for example because of violating a domain disjointness constraint), then the debugging framework can provide explanation of why the inconsis- tency occurred. More specifically, if an OWL-DL ontology is inconsistent, the work by Kalyanpur et al. [80] provides an algorithm to extract the minimal set of axioms in the ontology that causes the inconsistency. Thus, with a fairly simple mapping, one can use an o -the-shelf OWL reasoner as a policy engine and analysis tool, and an o -the-shelf OWL editor as a policy devel- opment and integration environment. OWL editors can also be used to develop domain specific assertion languages (essentially, domain ontologies) with a uniform syntax and well specified semantics. This mapping can also be used to experiment with extensions to WS-Policy, by using more expressive constructs from OWL as the policy language and assertion language level. We can experiment with policy language extensions without having to write yet another policy engine for them. Furthermore, ontology development techniques can be useful for policy develop- ment as well. Iterative development is a popular ontology engineering approach [119], where specializations are added to the class tree over time. Similarly, we can build up our 144 XA ::= (XACMLAssertion REQ CAP ) REQ ::= (Requirements VocabRef (SjCONS )) CAP ::= (Capabilities VocabRef (RQjpolDocjCONS )) CONS ::= (AttributeDesignator AV AD fcn)j (AttributeSelector AV AS fcn) Table 7.2: Syntax of Web Service Profile of XACML. policies from more general ones. A general policy could be very restrictive, setting tough guidelines for all organization?s policies - then di erent departments could subsume and extend this general policy. 7.2 WS-XACML This section will focus on WS-XACML, which is a XACML profile for web ser- vice policy assertions. Concise syntax and semantics is presented first, followed by a presentation of the WS-XACML to OWL-DL formal mapping. 7.2.1 Syntax of WS-XACML The top-level element of a WS-XACML policy is an assertion. A XACML-based Web Services Policy Assertion is a description of an entity?s Web Service?s policy w.r.t. to some policy domain. An assertion in WS-XACML can be used to express both require- ments and capabilities. Requirements The requirements for an assertion element can be expressed in terms of a Policy, PolicySet or a Constraint. Additionally, the Requirements element con- tains a VocabularyRef, which contains the URI?s associated with a given policy vocab- 145 ulary. Each XACML attribute referenced in Requirements must be defined in one of the policy vocabularies specified by a VocabularyRef. Capabilities Capabilities of a web service endpoint are expressed in terms of Requests or Constraints. Requests can be reduced to Constraints as follows: for each Attribute A in the Request a new Constraint is generated. The Constraint con- tains all attribute values occurring in the Request for A. Constraint A Constraint is represented by a boolean function. The attribute refer- enced using an AttributeDesignator or AttributeSelector is one of the arguments to the function. A Constraint is satisfied if the function used in the constraint evalu- ates to True when evaluated against a given value for the Attribute. The set of values for which the function evaluates to True is the set of acceptable values for the policy vocab- ulary variable.Exactly one attribute must be referenced by each Constraint. Following is an example of a constraint: 90 Only a limited number of comparison functions are allowed in Constraints and Constraints themselves cannot be nested. Finally, note that a Constraint can easily be translated to a XACML Rule element with the same semantics, simply by generating a Rule with an empty target and including the Constraint in the Rule?s Condition. 146 7.2.2 Semantics of WS-XACML This section presents an intuitive description of the semantics of WS-XACML as- sertion matching, along with a more formal presentation based on natural deduction rules. WS-XACML can be used to check if the constraints and capabilities of a web ser- vice provider are compatible with the constraints and capabilities with a web service con- sumer; thus, the main service WS-XACML provides is assertion matching. The rules for matching XACML Assertions are shown in Table 6.4. Two Assertions A and B match if at least one Requirements element in A matches one Capabilities element in B, and vice-versa. A missing Requirements (resp. Capabilities) in one assertion matches any Capabilities (resp. Requirements) element in the other assertion. The semantics of matching Requirements against Capabilities is presented in Table 6.3. Intuitively, it is done in the following way: A match between Policy or PolicySet p from Requirements and a Request r from Capabilities is successful i P yields a Permit on r. A match between Constraint c from Requirements and a Request r from Ca- pabilities is successful i the translation of c to a Rule P returns a Permit for r. A match between Constraint cr from Requirements and a Constraint cc from Capabilities is successful i the intersection of the two is nonempty. In the pres- ence of multiple Constraint elements in Requirements, they are treated as a log- ical AND, i.e., all Constraints must be satisfied in order for the Requirements element to be satisfied. Thus, for each Constraint in Requirements, there 147 should be at least one matching Constraint from Capabilities for the match to be successful overall. Intersection of Constraints is defined in the next section. fcn-2(AD;AV-2)\fcn-1(AD;AV-1)6j=? (Constraint AV-1 AD fcn-1) (Constraint AV-2 AD fcn-2) j= match 8CONSi : 9CONSjs.t.CONSi;CONSj j= match (Requirements VocabRef (CONS ));(Capabilities VocabRef (CONS ))j= match 8CONSi : 9RQs.t.CONSi;RQj= Permit (Requirements VocabRef (CONS ));(Capabilities VocabRef RQ)j= match 8S : 9RQs.t.S;RQj= Permit (Requirements VocabRef S);(Capabilities VocabRef RQ)j= match (Requirements);CAPj= match REQ;(Capabilities)j= match Table 7.3: Matching Requirements with Capabilities. 7.2.2.1 Matching Constraints If the constraints Ca and Cb that are matched do not refer to the same XACML at- tribute, the match still succeeds; however, the intersection is then defined as a conjunction of Ca and Cb. If the constraints refer to the same attribute (a), then matching is done by checking if the specified values for a are compatible. The constraints are compatible i there exist some value v for a that satisfies both Ca and Cb. Consider the following two constraints: 148 REQi 2REQ-1;CAPj 2CAP-2 REQi;CAPj j= match (XACMLAssertion REQ-1);(XACMLAssertion REQ-2 CAP-2)j= match REQk 2REQ-2;CAPl 2CAP-1 REQl;CAPl j= match (XACMLAssertion CAP-1);(XACMLAssertion REQ-2 CAP-2)j= match REQi 2REQ-1;CAPj 2CAP-2 REQi;CAPj j= match REQk 2REQ-2;CAPl 2CAP-1 REQl;CAPl j= match (XACMLAssertion REQ-1CAP-1);(XACMLAssertion REQ-2 CAP-2)j= match Table 7.4: Matching XACML Assertions. 90 and 45 Intersecting the two constraints, we see the allowed values for max-data-retention-days are between 45 and 90, so the constraints are compatible. Since the allowed compari- son functions are limited (mostly of type-equal, type-less-than, type-greater-than, etc.) and Constraints cannot be nested, computing the intersection of two Constraints is relatively straightforward. A detailed listing of supported constraint functions in WS- XACML and a decision procedure for computing intersection of Constraints can be found in Appendix A in the WS-XACML specification [95]. 149 7.2.3 Mapping WS-XACML Similarly to the XACML-to-DL mapping, I introduce a mapping function that takes WS-XACML expresions as input and returns DL concept expressions. For a XACML assertion A we will refer to its set of requirements and capabilities as A:req and A:cap, respectively. A XACML assertion A = (XACMLAssertion (REQ1;:::;REQn) (CAP1;:::;CAPn)) is mapped in the following manner: (A) = ( (REQ1)t;:::;t (REQn))u( (CAP1)t;:::;t (CAPm)) Mapping Requirements There are three cases for a Requirements R element: R is empty; in which case (R) = >, since R being empty is compatible with everything. R is of type Policy or PolicySet; for this case, the mapping function (R) is already defined in Chapter 6. R contains one or more Constraints c1;:::;cn; (R) (c1)u;:::;u (cn). Mul- tiple Constraints in a Requirements element are treated as a conjunction in the specification. The mapping function for constraints is defined in the next section. Mapping Capabilities There are three cases for a Capabilities element C: 150 C is empty; in which case (C) = >, since an empty Capabilities element is compatible with everything. C is of type Request; then (C) is already defined in Chapter 6. C contains one or more Constraints c1;:::;cn; (R) (c1)t;:::;t (cn). Mul- tiple Constraints in a Requirements element are treated as a disjunction in the WS-XACML specification. The mapping function for constraints is defined in the next section. Please note that WS-XACML also allows for PolicyDocument elements, that con- tain an XML document with domain specific policy vocabulary information. The seman- tics of PolicyDocument elements is outside the scope of the WS-XACML profile, hence it is not covered in this thesis. 7.2.3.1 Mapping Constraints A Constraint is simply a datatype function f performed on a single XACML attribute a and attribute value(s) v. (I will use shorthand f (a;v) to represent Constraints henceforth.) A WS-XACML Constraint is very similar to a Match element in XACML, with the only di erence being the type of comparison functions supported. For the basic matching functions, the behavior (and hence the OWL-DL mapping) is the same. For example, given a Constraint where the comparison function f is of type string-equal, and the attribute value v is of type string, the mapping generates a concrete (datatype) OWL-DL property to capture the attribute a, and a user-defined string datatype to capture v. For other basic comparison functions that occur in Constraints and Match elements, 151 the mapping is shown in Table 7.5. Matching function f cn (AV;fcn) type-equal DatatypeRestriction (type valueAV) type-greater-than DatatypeRestriction (type minExclusive valueAV) type-greater-than-or-equal DatatypeRestriction (type minInclusive valueAV) type-less DatatypeRestriction (type maxExclusive valueAV) type-less-than-or-equal DatatypeRestriction (type maxInclusive valueAV) type-regexp-match DatatypeRestriction (type pattern valueAV) xpath-node-match DatatypeRestriction (xpath-expression pattern valueAV) Table 7.5: Mapping matching functions. However, there are some additional matching functions that are allowed in Constraints, but not in Match elements: type-set-equals, type-subset, time-in-range. Given a Constraint f (a;v), type-subset is easiest to map since it simply corresponds to creating a conjunction of all of the attribute values in vi 2 v. This is because for a request to satisfy this con- straint, all of the values in v must occur in that request (additional ones are allowed as well). Type-subset-equals is more involved, since we have to make sure no additional val- ues for that attribute are present (apart from the ones in v). For this purpose, a cardinality constraint on attribute a is added , which essentially limits the number of possible values to #v. Finally, time-in-range is handled by generating a user defined date-time datatype (using min and max facets of XML schema). Formal representation of mapping in Table 7.6. 7.2.3.2 Analysis Services The OWL-DL mapping of WS-XACML presented in this section allows us to pro- vide a variety of reasoning services for WS-XACML assertions out of the box, similarly 152 Matching function f (a;v) ( f (a;v)) type-subset(a;v) u9 (a):vi for each vi 2v type-set-equals (type-subset(a;v))u=n (a):>where n = #v time-in-range(a;v1;v2) (DataHasValue( (a) DatatypeRestriction (type min- Inclusive v1)) DataHasValue( (a) DatatypeRestric- tion (type maxInclusive v2)) must-be-present(a) 9 (a):> must-not-be-present(a) 8 (a):? Table 7.6: Mapping Constraint functions. to WS-Policy: assertion containment - given two XACMLAssertions A and B, checking contain- ment (subsumption) is reduced to checking if (A)v (B) assertion incompatibility - if a request matches assertion A , then it will not match assertion B. This is reduced to checking disjointness of (A) and (B) : (A) u (B)j=? assertion satisfiability (nothing can match the assertion A, reduced to satisfiability check of (A)) formal verification of a policy. In particular, we?re presented with a set of WS assertions that must be satisfied and a set of assertions that have to be filtered by our XACMLAssertion. This is similar to verification for policies, where a set of tests (in form of access requests) and expected outcomes for those tests are provided. In order to make sure there is no possible instantiation of the XACMLAssertion that can break the properties, for a policy A and test input (in the form of an assertion, 153 too) C we perform the following satisfiability check: (A:req)u (C:cap) (C:req)u (A:cap) If the assertion C needs to be compatible with A, then the verification test succeeds when both expressions above are satisfiable, whereas for an incompatibility test, verification is successful when at least one of the expressions above are be unsatis- fiable 7.3 Putting it All Together To illustrate how the mappings of WS-Policy and WS-XACML can be integrated, consider the following example (01) (02) (03) (04) (05) (06) (07) (08) (09) (10) (11) (12) Figure 7.2: Example policy Example 7.3.0.1 This example contains a revised version of the policy from Figure 7.1. 154 Instead of domain-specific assertions, here WS-XACML policy assertions are used (be- cause of their verboseness, only the ID element is included in the description). Each WS- XACML assertion is mapped to an OWL class expression using the mapping function described in this section. Given this, each WS-Policy alternative is simply a conjunction of its constituent assertions. Alt1 (XA-1)u (XA-2) Alt2 (XA-3)u (XA-2) Finally, the policy class P is equivalent to the disjunction of the alternative classes: P Alt1tAlt2 As it can be seen from this example, given that both WS-Policy and WS-XACML are mapped to OWL-DL, their integration is straightforward. 7.4 Summary This chapter generalized the framework presented in Chapters 4 and 5 by applying it to a di erent domain (web service policies). The main di erence between the access control policies discussed earlier and the web service policies discussed here is that both web service requesters and web service providers can have policies of their own, unlike in access control where the requesters usually does not have an access policy. Because of this, checking whether two web service policies match each other in our framework is done using a satisfiability check, i.e., by trying to find a model where both policies will be satisfied. 155 Given this generalization the analysis framework was applied to web service poli- cies by presenting an OWL-DL mapping for both WS-Policy and WS-XACML. The map- ping was built on top of the XACML transformation described in Chapter 5 and it provides formal verification of policies, policy comparison (containment) and checking coherency (consistency) of web service policies. 156 Chapter 8 Implementation and Evaluation In this chapter, I show the logic-based framework presented in Chapters 6 and 7 can provide analysis tasks such as formal verification, policy comparison and redundancy checking for large and expressive XACML policies in a practical manner. For this pur- pose, I have implemented the XACML mapping as a policy analysis tool that is based on OWL-DL reasoners. An overview of the analysis tool and its novel optimizations are discussed in Section 8.1. Most of this chapter contains a discussion on the extensive empirical evaluation performed on my policy analysis tool. The empirical evaluation consists of two parts. The first part (Section 8.2) consists of a policy test suite where the performance of my ap- proach is compared to two of the most scalable XACML analyzers: BDD-based Margrave[50] and a SAT-based analyzer by Hughes et al. [67]. The policy test suite contains 5 non- trivial real-world XACML policies with limited expressiveness so the other tools can process them; the evaluation shows that the performance of my analyzer is comparable to the other approaches for these policies. The second part of the evaluation (Sections 8.3 and 8.4) uses two real world ac- cess control policies that employ more expressive features such as policy vocabulary do- mains, datatype functions and policy constraints: NASA Federated Data Access Use Case [118] and RBAC policies from the healthcare domain [62]. I converted these policies in 157 XACML and showed by empirical testing of formal verification and policy comparison service that my analysis tool can load and analyze these large policy sets in a practical manner. 8.1 Implementation The three main components of the analysis framework are a mapper, which converts XACML policies to DL knowledge bases, an analyzer, which reduces policy analysis services to DL reasoning tasks, and an output generator, which extracts counter examples from the internals of the reasoner and converts them to XACML access requests. I have provided an API so di erent DL reasoners can be plugged in and used as analyzers; so far, I have used the open source reasoners Pellet [110] and Fact++ [120]. An architectural diagram of the implemented prototype is presented in Figure 8.1. Figure 8.1: Architecture of Analysis Framework. I also implemented a few optimizations in the mapper to improve performance of 158 analysis services - these are briefly discussed below: Grouping by categories - A practical performance gain can be achieved by assum- ing the attributes for di erent categories are disjoint (which was the case for every XACML policy that I have used in the evaluation). This is because we can group the attributes based on the category they belong to, and then minimize unnecessary interaction between attributes in di erent categories (this idea is similar to con- junctive partitioning in model checking [130]). The partitioning is accomplished by introducing an additional (functional) DL role for each category like Subject, Resource, Action, and then adding the attribute values as role fillers of the corre- sponding category roles. To illustrate how it works, consider the mapping of a rule before: Deny-R3 9role:(ManagertDeveloper)t 9action-type:(readtwrite)t 9resource-type:Report and after: Deny-R3 9sub ject:9role:(ManagertDeveloper)t 9action:9action-type:(readtwrite)t 9resource:9resource-type:Report 159 Simplification of concept expressions. To improve performance, tableau reasoners reduce concept expressions to a simplified normal form before checking for concept satisfiability. Due to the size of the Permit-P and Deny-P axioms returned from the mapping function, simplifying the DL concepts as they?re generated by the mapping, before reasoning, reduces the amount of work the policy analyzer has to perform during reasoning. An example of output of the tool is shown in Figure 8.2. The service ran is formal verification, and the analyzer found a counter-example which is presented in XACML syntax. Additionally, a stack trace of policies that produced the counter-example is pro- vided. Figure 8.2: Sample Output of Formal Verification Service. 160 8.2 Policy Test Suite This section presents the first part of the evaluation: applying the analysis frame- work to a data set consisting of publicly available real-world XACML policies. To eval- uate the performance of the analysis tool, I tested the following services: formal verifi- cation, policy comparison (change analysis) and redundancy checking. The reason for testing only these services is that all the others (policy equivalence, disjointness, formal verification of policy di erences) can be reduced to either formal verification or policy comparison; thus, the running time for the other services should not di er substantially. The empirical dataset consists of XACML policies being used in various applica- tions; each of these policies is briefly described below: Continue [11] is a web application for paper submissions, reviews, and PC meet- ings. Continue contains 26 policy files (each one representing a PolicySet) in the set, with a total of 13 attributes and 36 attribute values. Although it does not have many attributes and/or values, the policies are fairly interconnected and nested (up to 5 levels), which makes it non-trivial to analyze. Fedora [4] is an open source digital management repository. It provides an exten- sible architecture for digital asset management (DAM), upon which many types of digital library, institutional repositories, digital archives, and digital libraries sys- tems might be built. Out-of-the-box, the Fedora repository is configured with a default set of XACML access control policies that provide for a highly restricted management service and an open access service for digital objects. 161 Generic Authorization, Authentication and Accounting Framework (GAAA [1]) is aimed at developing a Web Services-based open source toolit that will enable ap- plication developers to incorporate access control functions as part of workflow management in a Grid environment. In particular, the research uses the problem of on demand provisioning of network connections across multiple domains as a proof of concept. As part of the prototype, a set of policies is developed and made publicly available. eXist [3] is an open source XML Database. It supports XACML as means of spec- ifying access control for XML resources, and it provides a default XACML policy set to control access to Java methods from XQuery Network [67] is a set of non-trivial access control policies used in testing the SAT- based XACML analyzer developed by Hughes et al [67]. The general characteristics of the policies are shown in Table 8.1. Name Attributes/Values PolicySet Elements Depth Continue 14/36 26 5 Fedora 7/15 14 2 eXist 9/37 5 2 Network 5/10 6 2 GAAA 3/47 2 2 Table 8.1: General Information on Policies in Test Suite. In addition to testing my prototype, I also processed these policies using other XACML analyzers such as Margrave [50] and the analyzer described by Hughes et al [67] (referred to as HSAT from now on). These two were chosen since they are the fastest available XACML analyzers. Margrave is based on a mapping of a XACML policy to a 162 multi-terminal binary decision diagram (MTBDD) which is a data structure used to com- pactly represent boolean formulas. Similarly to Margrave, HSAT also translates policy verification queries to Boolean satisfiability problems; the di erence is that they use a SAT solver (zcha [102]) to obtain an answer. Both Margrave and HSAT are less expressive than my analyzer; in particular they lack the support for vocabulary domains in policies, data-types (HSAT has some incom- plete support) and non-trivial Condition elements in Rules. The policies were chosen so that at least one other analyzer (other than mine) can process them ? the goal being to investigate on how my approach would fare against analyzers optimized for less expres- sive policies. Note that the expressive policies discussed in Sections 7.3 and 7.4 cannot be handled by the other approaches. The experiments where run on a Linux machine with 2Gb of RAM and a 3.06GHz Intel Xeon CPU. In all of the figures, the X-axis corresponds to the policy being analyzed, while the Y-axis is the average time in seconds for performing the analysis service in question. 8.2.1 Formal Verification Results In order to perform formal verification, the following inputs are needed: a policy to be verified, a test case (represented as a XACML policy as well), and the expected outcome of the test case (e.g., NeverPermit, AlwaysDeny, etc.). Fortunately, the Continue policy contains 11 test cases and outcomes already specified by its security developers. For the other policies, however, I developed synthetic test cases based on the information 163 in the input policy. Essentially, I generated test properties as boolean functions consisting of attribute and values taken from the input policy being tested. The generated boolean functions were serialized to a XACML policy set and an expected outcome also randomly chosen. The results for verification are shown in Figure 8.3. Due to expressiveness limita- tions, Margrave was able to load only the Continue and Network policies, which consist of simple prerequisites in Target and no data-type functions. Please note that the loading ? which includes parsing the policy and converting it to the corresponding logic format ? for my approach is relatively stable; i.e., in in all cases it takes a few seconds to parse the policy and convert it to an OWL-DL knowledge base. The conversion time for HSAT, on the other hand, varies wildly: in the cases of eXist, Fedora and GAAA which use func- tions in the Condition element, it takes 100+ seconds (HSAT timed out while loading the GAAA policy after 16 minutes). With respect to verification time only, my approach exhibits the slowest performance, however notice that in all cases it still takes only around a second, which is acceptable performance for compile-time policy analysis; also, notice that the dominant component in all approaches seems to be policy loading and conversion time. 8.2.2 Policy Comparison Results Policy comparison refers to checking for semantic di erences between two poli- cies, i.e., finding all possible access requests where the policies would return di erent decisions. To evaluate this service, for every policy in the test suite, I performed 1) a 164 Figure 8.3: Verification results for OWL-DL-based, HSAT and Margrave. Times shown are for formal verification of security properties. Top left figure contains the time for parsing the XACML policy and loading/converting into the appropriate struc- ture (BDD, conjunctive formula, OWL-DL ontology). The top right figure contains the verification time, once the structure is converted. Bottom figure contains aggregate (load- ing+verification) timings. comparison of the policy against a copy of itself and 2) a comparison of the policy against a modified version of itself (5 randomly selected rules were removed to produce this modified copy). The results are shown in Table 8.4; they represent the average of 5 runs. Notice that the results for policy comparison results are similar to the ones for verification, since in all approaches the services are reduced to the same basic reasoning tasks. The main di erence between HSAT and my approach (DL) on one hand, and Margrave on the other is that Margrave finds all possible di erences between policies in a very fast manner. My analysis framework is not optimized for finding all di erences, so it only presents the first di erence between the two policies that it finds (if a di erence 165 Figure 8.4: Policy comparison results for OWL-DL-based, SAT and Margrave. Times shown are for checking policy equivalence. The figure contains the aggregate (load- ing+comparing) timings. exists). 8.2.3 Redundancy Checking Results Finally, I also performed redundancy checking of each Rule, Policy and PolicySet element in the policy test suite. Since the other tools do not support this services, only the results of my analyzer are shown in Table 8.5. Notice that Continue takes significantly more time than the others because of its nesting and interlinking; a single Policy element might be included in di erent PolicySets, so it becomes more involved to check all of the possible implications if the particular Policy element is removed. Interestingly, the analyzer did find a redundant Policy and Rule in Continue?s pol- icy: the third Policy in PPS paper-assignments rc PolicySet. Upon closer inspection, it seems that whenever the prerequisite of the third Policy is matched, the first Policy in that set will fire as well, and since the PolicySet is using the First-Applicable 166 combining algorithm, the decision of the first Policy will always override the third one. Figure 8.5: Checking redundancy of Rule, Policy and PolicySets. Times shown are aggregate (loading the policy, converting it to OWL-DL form and processing each policy element). 8.2.4 Extended Policies Since the performance of my approach was on the order of few seconds for all of the policies in the suite, I decided to test its scalability for larger versions of the test suite policies. For this purpose, I implemented a tool that for a given input policy generates a ?slightly? modified version of the policy. In particular, the modified policy has the same structure as the original (same number of Rules,Policies and PolicySets and same relationships between them); the only di erence is that the constants that are used as attribute values in the policies are randomly permuted and new attribute values are added. Using this tool, for each policy set (such as Continue), I generated a meta-policy that 167 combines the original one with a number of slightly modified versions of it. An example of such meta-policy is shown below : continue continue1 continue2 continue3 In the example above, continue refers to the original policy, whereas continue1, continue2, continue3 point to slightly modified versions. The goal of extending policies in such manner is to test the analyzers on larger policy sets that still preserve the structure of the original policy. The formal verification results for extended versions of Continue and Fedora are shown in Tables 8.6 and 8.7. As the size of Fedora and Continue increases, my approach scales very well. Most of the performance degradation comes from increased verification time, while the loading and conversion time remains stable. In the case of Continue, notice that Margrave is unable to load the larger policies. This is because each attribute/value pair from the policy is mapped to a node in the BDD structure used by Margrave. BDDs trade memory for speed, so the size of the structure is exponential to the number of variables (i.e., attribute-value pairs) in the worst case ? this causes memory problems when loading larger policies. 168 Figure 8.6: Testing the policy analyzers on an extended version of Continue. con- tinuex1 refers to the original version of the policy, continuexn denotes a policy that is n times large than the original. The Y-axis denotes the total time needed to load the policy and verify all 11 security properties. 8.2.5 Summary To show that the performance of my analysis framework is comparable to that of the fastest XACML analyzers available (Margrave and HSAT), in this first part of the evalua- tion I used a policy test suite consisting of 5 publicly available real XACML policies. The selected policies selected are relatively inexpressive but also non-trivial: they use a lim- ited set of XACML features (so the other approaches can process them), but each policy contains dozens of XACML Rule and Policy elements and they are fairly nested and interconnected. The results from this section show that even for these limited fragments of XACML where the propositional-logic based approaches are expected to dominate, my tool performs surprisingly well and is comparable overall to the other approaches. 169 Figure 8.7: Testing the policy analyzers on an extended version of Fedora. fedorax1 refers to the original version of the policy and fedoraxn denotes a policy that is n times large than the original. The Y-axis denotes the total time needed to load the policy and verify 5 randomly generated security properties. 8.3 NASA Federated Data Access Use Case In order to evaluate the more expressive features of the analysis framework, such as policy domains and datatypes, I collaborated with NASA HQ to develop an expressive set of realistic XACML policies [118]. Given the immense amount of heterogeneous data generated in di erent parts of the agency, information management is a major challenge for NASA. Several e orts are underway across the agency to use semantic technologies, including RDF and OWL, to respond to this information integration challenge. Some examples of Semantic Web applications at NASA include: BIANCA [2], an RDF-based data integration application, POPS [81] which provides faceted browsing across di erent domains and the NASA Taxonomy [49], which is a controlled vocabulary consisting of 7 hierarchies used to facilitate interoperability and search. The di culties of integrating and managing information across di erent organiza- 170 tions in the agency is manifested in the domain of access policy management. In par- ticular, integrating from multiple data sources presents challenges in policy management since the data sources typically have heterogeneous access control policies. Determin- ing how the policies of the constituent sources align and the subsequent specification of a policy for the integrated data is a labor-intensive process that is time consuming and error-prone. Because of these issues (referred to as the NASA HQ Federated Data Ac- cess Use Case) NASA HQ is interested in approaches that provide flexible and expressive policy management for heterogeneous and distributed policy sets [118]. For the purpose of this dissertation, I collaborated with representatives from NASA HQ to develop a set of policies for the Federated Data Access Use Case. The application we investigated was BIANCA (the name is an acronym for Business Impact Analysis for Networked Computer Assets). BIANCA provides a single integrated view of information about (including relationships between) applications, servers, network services, networks and change items for NASA HQ. BIANCA analyzes dependencies between these assets in order to provide services like repair plans, outage cost estimates, and dependency reports. Users can query across the federated information store and browse the data in a web browser in order, for example, to track the impact that a failure of one system, subsystem, or application would have on other systems and customers. BIANCA has an RDFS data reference model that can be reused by other applications. 171 8.3.1 BIANCA Policy Set This section contains a description of the BIANCA Policy set that we developed. The policy follows the Role-Based Access Control (RBAC) model; thus, there is a sepa- rate XACML PolicySet that contains the set of permissions for each role. Additionally, the permissions are split among the di erent types of resources ? these include the four broad categories of networks, network services, servers and applications. A fragment of the BIANCA policy is shown in Table 8.2. Department Role Action Resource Decision Financial Operations Intern Read ExpenseReport Permit Employee Read OR Write ExpenseReport Permit Project Manager Write or Read Any Permit Any Any Any Deny Missions & Projects Scientists(Internal) Read InternalPaper Permit Scientists(Internal) Write InternalPaper Permit Scientists(External) Read PublicDoc Permit Project Manager Read OR Write Any Permit Any Any Any Deny Institutions and Management CivilServant Write OrgHierarchy Permit Employee Read OrgHierarchy Permit Project Manager Write Any Permit Any Any Any Deny Table 8.2: Fragment of BIANCA Policy Set. We used the NASA Taxonomy [49] to describe policy entities such as types of resources. The Taxonomy includes seven facets, some of which can be used as policy vocabularies to express roles, access controls, competencies and organizations in NASA. Given that the taxonomy is in SKOS format, for this evaluation I converted it to OWL first and used the XACML-OWL coupling mechanism described in Chapter 6 to extend the XACML policy set. 172 In total, there are 4 main policy sets: a general, agency-wide policy representing rules that each department-specific policy has to conform to and three department policies for Institutions and Management, Missions & Projects and Financial Operations. Each departmental PolicySet in turns contains a policy for each type of role (the number of roles ranges from 5 to 50). 8.3.2 Empirical Results Given the BIANCA policy set described above, the analysis services I tested were formal verification and policy containment. For formal verification, I used a number of queries that emerged from our discussion with representatives from NASA: Q1 ? PII: For a policy Pa, check if there is a way for an access request to get a Permit from Pa without disclosing personally identifiable information (PII). PII is expressed as a XACML Policy containing a combination of attributes: SSN, street address, full name, IP address, email, etc. Q2 ? Compliance of department-specific policies to general policy: whenever the base policy yields a Permit (resp. Deny), check if the department-specific policy will also return a Permit (resp. Deny). Q3 ? Disjointness query : For two policies P1 and P2, check if there can exist an access request s.t. both policies apply to it. The results of evaluating these queries are shown in Figures 8.8,8.9 and 8.10. No- tice that even in the case with the largest policy set, the total processing time for all of the 173 queries was less than 10 seconds, which the NASA engineers felt was more than accept- able given the size of the policies and the task at hand. Most of the running time is spent on loading and converting the Policy; this is because the policy refers to various segments of the OWL-based NASA Taxonomy, so the NASA ontologies are also loaded during this step. Because the ontologies are relatively inexpressive, reasoning about them is very fast (order of milliseconds), so the only noticeable overhead is during loading the policy. Figure 8.8: Analysis time for the Personally Identifiable Information Query on vari- ous policies addressing the NASA HQ federated data access use case. 8.4 Healthcare Access Policy This final section of the chapter presents an empirical evaluation of my framework using a real-world access control policy from the healthcare domain. Similarly to the NASA access use case, the healthcare policy motivates the need for vocabulary domains and datatypes in policies; unlike the NASA policy, this use case is fully developed as part 174 Figure 8.9: Analysis time for the Policy Comparison (compliance) query on various policies addressing the NASA HQ federated data access use case. Figure 8.10: Analysis time for the Policy Disjointness Query on various policies ad- dressing the NASA HQ federated data access use case. 175 of an ongoing international standardization e ort (HL7 1). In the following, I provide a brief background on the developments of standards for accessing patient?s electronic health records and then present the RBAC policy that is provided as part of the HL7 standard. I converted this RBAC policy to XACML form and used it to evaluate my XACML analysis tool. The empirical results along with some discussion are presented in Section 8.4.4. 8.4.1 Background: HL7 and Electronic Health Records Health Level 7 (HL7) is an international community of healthcare subject experts and information scientists collaborating to create standards for the exchange, manage- ment and integration of electronic healthcare information. The goal of HL7 is to have a degree of interoperability among healthcare providers such that health information can be exchanged so that a patients medical information can be made portable and available to his/her clinicians (at least to the extent that the patient allows it to be). The aspect of guarding patient?s privacy and confidentiality is crucial in this set- ting. Because of this, a major component of HL7 called the Security Technical Commit- tee2 deals with specifying security policies for controlling access to patient?s confidential information. The standardization work produced by this committee includes a set of role- based permissions [62] and recommended access policy scenarios [5] that were directly used to evaluate the performance of my policy analysis framework. 1Health Level 7 is an accredited Standards Developing Organizations operating in the healthcare arena. HL7s domain is clinical and administrative data. 2http://www.hl7.org/Special/committees/secure/index.cfm 176 8.4.2 HL7 RBAC Policy Representatives from HL7 have worked closely with the US Department of Veteran A airs (VA) to develop a standard set of permissions for healthcare access policies. The reason is that VA currently has the largest electronic health record system in the country, with more than 4 million patients, 180,000 medical personnel and deployed in more than 160 hospitals throughout the US [7]. Working with representatives from VA, the HL7 committee has published a stan- dard of role-based access control (RBAC) permissions [62] recommended as building blocks for access control policies for health information systems. This set of permissions will be referred to as HL7-RBAC. An RBAC policy associates a role in the organization with a set of permissions for that role. Since users are not assigned permissions directly, but only acquire them through their role (or roles), management of individual user rights becomes a matter of simply assigning the appropriate roles to the user. As part of HL7-RBAC, two general categories of roles are allowed: structural and functional roles. Functional Roles consist of all the permissions needed to perform a task. Functional role names are associated with groups of permissions for convenience in assigning to users. Structural roles, on the other hand, denote the placement of people in the organizational hierarchy as belonging to categories of healthcare personnel warranting di ering levels of access control. Examples of structural roles include Clinician, Patient, PhysicalAssistant, etc. There are no permissions associated with structural roles ? they are simply used as prerequisites for functional roles. 177 8.4.3 Converting HL7-RBAC to XACML HL7-RBAC is specified using a tabular format in [62], so I converted the policy to XACML first in order to evaluate my analyzer. The conversion was done as follows: a functional role with an associated set of permissions was converted to a XACML Policy which contains the permissions as part of its Target elements. For example, the func- tional role PPD-036 which contains create permissions for New Patient/Family Prefer- ences is expressed in XACML as: create Patient_Preferences 178 Since structural roles are prerequisites for the permissions in functional roles, they are added to the Target element of a policy representing a functional role. Because XACML does not have built-in support to express the type of semantic hierarchies needed for structural roles [15], I used an OWL ontology to capture these hierarchical relation- ships. In addition to expressing relationships between structural roles, I also used OWL to provide integer and date-time datatype support (e.g., Regular Doctors can access Patient Records during business hours, whereas ER Doctors should have access at all times) and role-based cardinality constraints (e.g., Chief-of-Sta role has cardinality of 1). 8.4.4 Empirical Results The standard documents discussed above present the basic building blocks of an access policy: a set of permissions and a set of roles that are to be associated with those permissions. Given these permissions, the Department of Veteran A airs has presented a reference collection of RBAC scenarios [5] that denotes the access control policies used in their health information system. The reference collection contains 39 scenarios, and each of them describes a situation where a particular structural role (or a combination of roles) is presented and set of permissions is given that is required for that role. I converted these RBAC scenarios to a XACML policy by associating the structural roles referenced in the scenarios with the corresponding functional roles described in the previous section. The end result of this conversion is a large and expressive XACML pol- icy (referred to as HL7-RBAC) that was used to evaluated the analysis services provided by my framework. HL7-RBAC contains a total of 107 PolicySets. It uses only 3 di erent attributes 179 (action-type, subject-role-type and resource-type), however it has 102 di erent values: 5 values for action attributes (create, read, update, delete, execute), 51 attribute values to represent objects(resources) and 46 attributes to represent subject roles types (Physician, Patient, Clerk, etc.). The two analysis services tested against HL7-RBAC were formal verification and policy comparison. The results for these services are shown in Figure 8.11 and Figure 8.12, respectively. Since for both of these services, the analyzer performed surprisingly well (a few seconds to verify properties and perform comparison), I also experimented with an extended version of the policy. Thus, HL7x2 and HL7x3 in the figures refers to a policy that is two and three times larger than the original HL7-RBAC. I should note that the the analysis framework scales very well as the size of these policies increases. Also, I should note that these are very large policies ? HL7x5 for example, refers to a dataset with 535 PolicySet elements, and 250 attribute values. Figure 8.11: Formal Verification of HL7 policy. Please note that HL7x1 refers to the original policy whereas HL7xn refers to a meta-policy containing n policies of the same size and structure as HL7. 180 Figure 8.12: Policy Comparison timings for HL7 policy. Please note that HL7x1 refers to the original policy whereas HL7xn refers to a meta-policy containing n policies of the same size and structure as HL7. 8.4.5 Summary The healthcare policy described in this section is a great use case for my analysis framework: it is large, with dozens of roles and hundreds of attribute values and it is ex- pressive (with RBAC constraints, data-types and domain vocabularies for heterogeneous policies). By evaluating my analysis tool on this policy (after I converted it to XACML) I showed that my approach can formally verify and compare large, real-world policies in a practical manner. This use case also demonstrates the benefits of grounding the analysis framework on OWL-DL, since I used OWL ontologies to represent structural role hierar- chies. Note that there has already been interest in formalizing the HL7 reference model in OWL [108] ? I leveraged some of this previous work to develop the role hierarchies. Finally, I have made my XACML version of the HL7-RBAC policy publicly available 3 so it can be used as a benchmark to evaluate other XACML processors. 3Available at http://www.mindswap.org/~kolovski/hl7rbac.zip 181 8.5 Discussion The second part of the evaluation used real world access control policies with ex- pressive features such as policy vocabulary domains, datatype functions and policy con- straints. The policies used (NASA HQ Data Access Use Case and Healthcare RBAC Policy) are a great match for the analysis framework since they both motivate the need for expressive background domains (ontologies) in order to facilitate information exchange and interoperability across di erent parts of an enterprise system. Both of the policies are quite large: 100s of PolicySet elements and 100+ attribute values in each case. I showed through empirical testing that the analysis framework scales very nicely as the size of these policies increases. Considering that the framework is supposed to be used at development time, before the policies are deployed (so the performance requirement is not as critical as a deployed policy engine), the empirical results shown in this section prove that my analyzer is practical for very large and expressive policy sets. 182 Chapter 9 Conclusions and Future Work In this thesis, I identified some important challenges facing XACML; namely, a lack of understanding of its formal properties, and a lack of automated, design-time analysis services that provide support for distributed and heterogeneous policies. To address the first issue above, in Chapter 4 a formal, proof-theoretic semantics for XACML 3.0 was given using natural deduction rules. The semantics covers the core of XACML along with its Administrative Profile, and represents a concise and formal version of the informal semantics given in the o cial language specification. To deter- mine XACML?s complexity properties, I provided a translation of various subsets of the language to locally stratified Datalog in Chapter 5, thus establishing its polynomial data complexity and close relationship to other logic-based languages such as the Flexible Au- thorization Framework. Additionally, I showed that access request checking in XACML with cyclical references between policies is NP-complete. The other issue addressed in this dissertation is the lack of compile-time services that can detect inconsistencies in the presence of distributed and heterogeneous XACML policies. This issue has been motivated by recent interest in extending XACML with both distributed policies (Administrative Policy Profile in XACML v3.0) and rich policy domain models that provide additional expressiveness [13, 47] and support for integration of policies about di erent types of data resources [40, 21, 118]. Given these requirements, in Chapter 6 an analysis framework was presented that can reason about both distributed and heterogeneous XACML policies. In particular, I 183 showed how with a mapping to Description Logics, we can do change analysis, formal verification and coverage checking for XACML policies using DL reasoners. Since De- scription Logics are the logical formalism underlying the OWL-DL sub-language, the analysis framework presented in this thesis can easily cover XACML policies extended with OWL ontologies [40]. This compatibility with OWL ? which is a W3C standard for representing information on the Web ? and the full mapping of the Administrative Profile presented in Chapter 6, enables the analysis framework to cover the expressive features of XACML that allow for distributed and heterogeneous policies. In Chapter 7, I demonstrated that the analysis framework can be applied to domains other than access control. In particular, I mapped WS-Policy ( a web services policy language) to OWL-DL and provided the same analysis services as for XACML. Finally, in Chapter 8 I presented my prototype implementation of a XACML-to-DL mapper and policy analyzer. Since DLs in general have very bad worst case complexity, I showed through an extensive performance evaluation using real world policy sets that OWL-DL reasoners are practical for static policy analysis. The performance results were presented in Chapter 8. 9.1 Contributions The contributions of this thesis are as follows: A formal, proof-theoretic semantics of XACML v3.0 that covers the core specifi- cation and the Administrative Policy Profile. A mapping of XACML to Datalog that provides a model-theoretic semantics and 184 computational complexity results for full XACML and various fragments. Addi- tionally, an extensive comparison with other logic-based languages such as Flexible Authorization Framework and SecPal based on the Datalog mapping. A static analysis framework based on Description Logics that can reason about expressive XACML policies. Using a XACML-to-Description Logics mapping, a comprehensive set of services are provided: formal verification, policy comparison (change analysis) and redundancy checking. Demonstrated more general applicability of the framework by using it to formalize and analyze policies in the web services domain. An empirical evaluation of the scalability of the analysis framework using real world policy data sets. 9.2 Future Work In this section, I will discuss the limitations and open issues of this dissertation. Additionally, I discuss possible avenues of future work, split in two sections: extensions of theoretical framework and improvements to analysis services support. 9.2.1 Theoretical Framework 9.2.1.1 Dynamic Environment and Obligations In this dissertation, an assumption is made that the response to an access request is simply yes/no, i.e., it does not change the state of the policy environment. However, it has been recognized that a yes/no response to every scenario is insu cient for many modern systems and applications [33]. Many policies require certain conditions to be satisfied 185 and actions to be performed before or after a decision is made. Thus, there has been great amount of interest in policy languages that support dynamic environments [33, 48, 69]. For example, XACML allows for policy obligations, meaning that after being granted access, the subject must perform the actions associated with the grant. Most logic-based formalisms for dynamic policies are based on First-Order tem- poral logics [103, 94], which cannot be easily combined with Datalog (or Description Logics, for that matter). An interesting area of future work involves exploring decidable extensions of the logic-based formalization presented in this thesis with dynamic policies. 9.2.1.2 Extensions of XACML In Chapter 5 I showed that there exists a polynomial reduction of XACML to a variant of Datalog. Given this mapping, and the existence of numerous policy languages coming from academia and industry that are also based on Datalog, one possible direction of future work is to investigate extending XACML with features from these languages. A potentially useful feature of the Flexible Authorization Framework (FAF) is its history table , i.e., a table whose rows describe the access requests already processed. A history table can be used to model various policy constraints such as the Chinese Wall security policy, and will not change the computational complexity of XACML if it were added. Also, combining algorithms such as most-specific-overrides and no-overriding can also be easily adapted to XACML: most-specific-overrides can be performed by compar- ing the Targets of the two policy elements to be combined, whereas for no-overriding a clause can be added to throw Indeterminate whenever conflicting access decisions are returned. 186 Other, non-trivial features worth exploring are delegation constraints. While XAC- ML does have an Administrative Policy Profile, there is no explicit support in it for com- mon delegation constraints such as depth-bounded delegation (i.e., limiting the number of times an access decision can be delegated) or threshold-constrained trust (i.e., at least k out of n given principles must sign a given access request). Both of these features, among others, are supported by Datalog-based languages such as as SecPal [27] and Delegation Logic [87], so an interesting research problem would be how to incorporate them into XACML. 9.2.2 Analysis Services 9.2.2.1 Computing All Di erences between Policies One of the analysis services provided in Chapter 6 was change impact analysis. A limitation of the approach is that when comparing two policies, if the policies have dif- ferences among them, then the analyzer returns only one access request corresponding to one di erence. As part of future work, I would like to extend this approach in order to provide comprehensive change impact analysis, as done in Margrave [50]. To provide this service, I plan to use a technique based on computation of all models that admit a De- scription Logic concept expression, which is done by tableau saturation. Saturation of the tableau completion graph is done by continuing application of the completion rules until all choice points are explored and no more rules are applicable. While most DL reasoner optimizations are not applicable during saturation, there are still some optimizations that can be used (such as absorption), and it is possible that other significant optimizations could be applied due to the nature of the XACML-to-DL mapping. 187 9.2.2.2 Policy Repair Most of the analysis services discussed in the thesis help policy developers discover errors in their policies, be it unauthorized access after an update, or corner cases that do not satisfy given test cases. The next step is to help policy developers recover when they do find errors in their policies. To illustrate this service, consider the example in Figure 9.1 below. Figure 9.1: Example Policy The security property is : Developer should not be able to write to Report. When checking the policy against this property, our analyzer returns two counter examples: role=Manager, role=Developer, action=write, resource=report role=Developer, action=write, action=read, resource=report Thus, if a requester comes along that is a member of both roles (Manager and Developer), then she can gain write access to Report. The other way for a Developer to gain write access is if he tries to both read and write to Report at the same time. To 188 prevent unauthorized access in this example, two constraints can be added; first one to make Manager and Developer mutually exclusive roles, and the second one to make sure that only a singleton value for the action attribute of a request is admitted. However, there are also other ways to repair the policy. For example, if the goal is to add as few axioms as possible to fix the policy, then there exists a better solution, involving only one constraint: 9role:fDevelopergv:9action:fwriteg This axiom explicitly prohibits developers from writing to anything. This constraint is adequate for our toy policy because there is only one type of resource that can be written to (Report). In a larger policy, we might not necessarily want to prevent Developers from writing to other types of resources. In that case, we will need somehow to measure and to compare the impact of each individual repair strategy. The idea of policy repair was inspired by recent work by Kalyanpur et al. [79] in repairing unsatisfiable concepts in Description Logics. There the authors present a new DL service (ontology repair), which semi-automatically selects which axioms need to be removed (or rewritten) from the ontology in order to render the concept satisfiable. To select likely candidate axioms for removal, their work uses algorithms that rank the axioms depending on a set of criteria. There is one essential di erence between the work by Kalyanpur et al. and the future work proposed here: whereas in their case axioms are removed to fix errors in ontologies, in my case axioms (representing policy constraints) will be added to the KB in order to fix access control errors in policies. The problem of which axioms need to be added to make the policy concept unsat- 189 isfiable is hard since there are infinitely many solutions. However, for the purposes of access control policy repair, the search space could be constrained to DL axioms that cor- respond to policy constraints in the analysis framework. In that way, finding repair plans will be easier, and presenting them to policy developers will be easier since no knowledge of Description Logics will be required. As a first step, the following common types of policy constraints could be used: separation of duty, role cardinality constraints, single- ton values for attributes and role hierarchies. As part of future work, I plan to devise an algorithm to compute sets of axioms that need to be added and then investigate possible ranking strategies similar to the ones in [79], but adapted for our access control scenario. 9.2.2.3 Extending and Evaluating Redundancy Checking In Chapter 6 I presented an algorithm for determining if a policy is redundant. Ad- ditionally, I presented an algorithm for finding all non-redundant policy subsets for a given policy set. Considering that computing all of the non-redundant subsets is likely to be non-practical for large policies (e.g., with more than 20-30 PolicySets), a possi- ble next step would be to devise an approach that considers user input on which of the redundant policies to remove. For example, users could rank di erent policies based on specific criteria: size of policy, number of children, etc., and the analysis tool would gen- erate a non-redundant policy subset based on these criteria. A comprehensive evaluation (possibly through a user study) of such an approach would have to be performed to deter- mine whether the tool provides enough information to guide users during the process of removing redundant policies. 190 9.2.3 Analyzing Business Rules An interesting research problem to pursue would be applying the analysis frame- work to the domain of business rules. Business rules are much more general than access control policies; they specify the operations, definitions and constraints that apply to an organization. There exist a few business rule languages proposals [76, 6], and there has been a great amount of interest in rule engines that support verification, accountability and enforcement of business rules. 191 Appendix A Proofs Proof of Lemma 6, If case. For a request RQ, we need to show that: if RQ;Tj=m True then KBj= (True;T)( (RQ)) (A.1) The proof will be done by structural induction. We will show that (A.1) holds for Match elements first, and afterwards, by going through the XACML semantics rules, we will show it also holds for Target elements. Match Element I will show that the following holds: if RQ;Mj=m True then KBj= (True;M)( (RQ)) (A.2) In order to show that KBj= (True;M)( (RQ)) we need to show that the expression (RQ)u: (True;M) is unsatisfiable. In Sections 6.1.2 and 6.1.1 the DL mapping was defined as: (True;M) 9 (ADM): (fcn; AVM) (RQ) 9rAV: (typeAV-equal; AV) forall AV2AT;AT2ATS;ATS2RQ (A.3) 192 To prove (A.2), it needs to be shown that: 8 (ADM):: (fcnM; AVM)u 9rAVi: (typeAVi-equal; AVi) (A.4) is unsatisfiable for some AVi 2AT;AT2ATS;ATS2RQ. Assume that the left hand side of the implication in Equation A.2 holds. By the inference rules in Table 4.6, RQ;Mj=m True means there exists an attribute value AV s.t. the following holds: 1. AV 2AT;AT 2ATS;ATS 2RQ 2. typeADM = typeAV, attr-idADM = attr-idAT , issuerADM = issuerAT , catADM = catATS 3. fcn(AVM;AV) = True Condition 2) implies the DL role used in (ADM) will match the DL role used in the mapping of AV. (This is because the role names are generated as a function of attr-id, issuer, cat and Type, and they all match in this case.) Because of this match, the role filler of (ADM) will have the following DL expression occurring in its label: (typeAV-equal; AV)u: (fcn(AVM)) (A.5) From condition 6) above we know that the value of AV belongs in the value space characterized by fcn(AVM). However, note that in our mapping (fcn(AVM)) creates a user defined datatype that has the same interpretation as fcn(AVM). This is because the user defined datatype in our mapping has the same base XML schema type, and the facets 193 we use to limit the value space have the same semantics as the matching functions used in XACML (as shown in Table 6.1.7). Thus, (typeAV-equal; AV) will belong in the space defined by (fcn(AVM)) . That in turn implies that equation (A.5) will produce a clash, rendering the expression: (True;M)u (RQ) unsatisfiable and showing that: if RQ;Mj=m True then KBj= (True;M)( (RQ)) Indeterminate If RQ;M j=m Indeterminate, that means that there is no attribute AT 2 ATS;ATS 2 RQ that matches the attribute designator ADM; additionally, the mustBePresent property must be set to true. As shown in Section 6.1.1, whenever an attribute ADP is not present, we add (conjunct) the expression8 (ATP):?to (RQ). According to the mapping axioms in Section 6.1.2: : (Indeterminate;M) 9 (ADM):> Thus, to check satisfiability of: (Indeterminate;M)u (RQ), we have (RQ)u9 (ADM):> (A.6) Because RQ;M j=m Indeterminate, we know that the attribute designated by ADM does not occur in the request - thus, when checking for satisfiability of equation (A.6) we will get a clash, which proves that: if RQ;Mj=m Indeterminate then KBj= (Indeterminate;M)( (RQ)) 194 Extending the proof to ConjunctiveMatch, DisjunctiveMatch and Target Elements. First I will show that if RQ;CMj=m E then KBj= (E;CM)( (RQ)) where E2fTrue;Indeterminateg, and then inductively extend the proof for DM and T. I will only show for E = True - the proof for the Indeterminate is very similar Following the deduction rules in Table 4.2.1, if RQ;CM j=m True then it must be that8MCM : RQ;MCM j=m True. From the above proof for M, we also know that if RQ;Mj=m True then KBj= (True;M)( (RQ)) Taking the above axioms into account and using the mapping for (True;CM) defined in Section 6.1.2, we can conclude that KBj= (True;CM)( (RQ)). Following the inference rules again, if RQ;DM j=m True then exist at least one CMi 2 DM s.t. RQ;CMi j=m True. From the previous proof for CM, we know that for this CMi, KBj= (True;CMi)( (RQ)) Using the above result, and taking the mapping axiom for DM into account: (True;DM) (True;CM1)t:::t (True;CMn) implies that KBj= (True;DM)( (RQ)). 195 Finally, if RQ;T j=m True then 8DMT : RQ;DMT j=m True. From the previous step for DM, we know that for all DMT , 8DMT : RQ;DMT j=m True!8DMT : KBj= (True;DMT )( (RQ)) Taking the mapping axiom for T into account: (True;T) (True;DM1)u:::u (True;DMn) it follows that KBj= (True;T)( (RQ)). Proof of Lemma 6, Else case. We break down the proof by going through the case when KBj= (True;M)( (RQ)) first and then for KBj= (Indeterminate;M)( (RQ)). True case We know that KB j= (True;M)( (RQ)) In Sections 6.1.2 and 6.1.1 the DL mapping was defined as: (True;M) 9 (ADM): (fcn; AVM) (A.7) Thus, (RQ) is of type9 (ADM): (fcn; AVM). In Section 6.2.1.1 we see that: (ADM) is mapped back to an attribute AT that matches (in datatype, ID, category and issuer) the one specified by the attribute designator ADM. (fcn; AVM) is mapped nondeterministically to a value in the data value range that satisfies the function fcn(AVM). 196 Essentially, (ADM): (fcn(AVM)) maps back to an attribute AT and attribute value AV that will match the designator ADM and the attribute match function fcn, s.t.M;RQj=m True. To extend the proof to CM, consider that: (True;CM) (True;M1)u:::u (True;Mn) Thus, (RQ) is of type (True;M1)u:::u (True;Mn). It was shown above that (RQ) : (True;M)!M;RQj=m True so for each Mi 2M above we know that RQ will match it. However, if RQ matches all of Mi 2M, then by virtue of rule 1 in Table 4.2.1: CM;RQj=m True To extend the proof to DM, we use the mapping axiom from Section 6.1.2: (True;DM) (True;CM1)t:::t (True;CMn) Thus, (RQ) : (True;CM1)t:::t (True;CMn). It was shown above that (RQ) : (True;CM)!CM;RQj=m True 197 , so for at least one CMi 2 DM it follows that CMi;RQ j=m True . However, if RQ matches at least one of CMi 2DM, then by virtue of rule 4.2.1: DM;RQj=m True To extend to T, we use the mapping axiom from Section 6.1.2: (True;T) (True;DM1)u:::u (True;DMn) Thus, (RQ) : (True;DM1)u:::u (True;DMn). It was shown above that (RQ) : (True;DM)!DM;RQj=m True so for all DMi 2T above we know that DMi;RQj=m True . However, if RQ matches all of DMi 2 T, then by following the inference rules in Table 4.2.1:T;RQ j=m True. I have shown that: KBj= (RQ) : (True;T)!T;RQj=m True Indeterminate case We assume the attribute mustBePresent is set to true. In this case, KBj= (Indeterminate;M)( (RQ)). The mapping axioms for indeterminate is defined in Section 6.1.2 as: (Indeterminate;M) 8 (ADM):? 198 Thus, (RQ) will map back to a request RQ that has no values for the attribute specified by ADM. However, if RQ has no values for ADM then according to the inference rules in Table 4.2.1, M;RQj=m Indeterminate Extending the proof to CM, DM and T can be done in the same manner as for the True case above, we omit it here for brevity. Proof of Lemma 7. For a request RQ, we need to show that: if RQ;T6j=m True then KBj=: (True;T)( (RQ)) (A.8) True Case We will start with M, and show that the following holds: if RQ;M6j=m True then KBj=: (True;M)( (RQ)) (A.9) In order to show that KBj=: (True;M)( (RQ)) we need to show that the expres- sion (RQ)u (True;M) is unsatisfiable. In Sections 6.1.2 and 6.1.1 the DL mapping was defined as: (True;M) 9 (ADM): (fcn; AVM) (RQ) AV2RQ 9r AV: (typeAV-equal; AV) u AT j. Thus, there exists some rule Ri 2 P s.t. (RQ) : E ect-Ri. Additionally, for all Rj 2 P s.t. j < i : (RQ) : :Deny-Rju:Permit-Rju:Indeterminate-Rj , which in turn implies that Rj;RQ6j= Deny, Rj;RQ6j= Permit and Rj;RQ6j= Indeterminate for all j < i. The above conditions , together with Lemma 8 satisfy all of the prerequisites for the rule in Table 4.9, thus: KBj= (RQ) : E ect-P!P First-Applicable T Ri;RQj= E ect-P Only-One-Applicable In this case, we use E ect as a substitute for Permit or Deny. According to the mapping axioms in Section 6.1.4, KBj= (RQ) : E ect-P implies the following holds: 214 ? (RQ) : (True;T). ? (RQ) : E ect-Ri for some Ri 2P. ? (RQ) ::Deny-Rju:Permit-Rju:Indeterminate-Rj for all Rj 2P. The above three conditions together with Lemma 8 satisfy all of the prerequisites for rule 3 in Table 4.10, thus: KBj= (RQ) : E ect-P!P Only-One-Applicable T Ri;RQj= E ect-P Indeterminate. According to the mapping axioms in Section 6.1.4, KB j= (RQ) : E ect-P implies at least one of the following: ? (RQ) : (T) and (RQ) : Indeterminate-Ri for some Ri 2P. ? (RQ) : (T) and there exist Ri;Rj 2 P ;i , j s.t. (RQ) : E ect-Ri and (RQ) : E ect-Rj, where E ect-Ri;E ect-Rj can be Permit or Deny. Satisfying either of the above conditions , together with Lemma 8 is enough to infer that: KBj= (RQ) : E ect-P!P Only-One-Applicable T Ri;RQj= Indeterminate After covering all of the rule combining algorithms , I proved that: KBj= (RQ) : E ect-P!P;RQj= E ect 215 Proof of Lemma 11. This proof has a few sections, depending on what type of rule com- bining algorithm is being considered. Permit-Overrides P;RQ 6j= Permit. Considering that semantics rule 1 is the only one that can entail P;RQj= Permit in Table 4.8, we have: T;RQ6j= True_(8Ri 2P : Ri;RQ6j= Permit) which together with Lemmas 7 and 9 implies that (KBj= (RQ) :: (T;True)) OR (8Ri 2P : KBj= (RQ) ::Permit-Ri) Since Permit-P (T;True)u G Permit-Ri ; when we try to evaluate satisfiability of Permit-Pu(: (T;True)t( :Permit-Ri)) we will always get a clash, proving that KBj= (RQ) ::Permit-P P;RQ6j= Deny. The mapping axiom for Deny in Section 6.1.4 is defined as follows: Deny-P (True;T)u G Deny-Riu :Permit-Rj u( :Indeterminate-Rk) where E ectRk = Permit (A.19) 216 Since inference rule 2 in Table 4.8 is the only one that can entail P;RQ j= Deny, that means that at least one of the following holds: ? T;RQ 6j= True, which implies KB j= (RQ) : : (T;True). Notice that this expression will clash with the first conjunct in equation (A.19), rendering Deny-Pu (RQ) unsatisfiable. ? 8Ri 2 P : Ri;RQ 6j= Deny. This means that for each Ri 2 P, KB j= (RQ) : :Deny-Ri, which means that there always will be a clash with the first item in the second conjunct in equation (A.19) (F Deny-Ri), again ren- dering Deny-Pu (RQ) unsatisfiable. ? 9Ri 2 P : Ri;RQ j= Indeterminate where E ectRi = Permit. The map- ping of this expression will clash with the last item in the second conjunct ( :Indeterminate-Rk), which is only focused on rules where the e ect is Permit. ? 9Ri 2P : Ri;RQj= Permit ? this implies that for some Ri 2P, KBj= (RQ) : Permit-Ri which will clash with the second item in the second conjunct. Since I showed that in all three cases the expression Deny-Pu (RQ) will be unsat- isfiable, it will always follow that KBj= (RQ) ::Deny-P for this case. P;RQ 6j= Indeterminate. The mapping axiom for Indeterminate in Section 6.1.4 is: Indeterminate-P (T)u G Indeterminate-Riu :Permit-Rj where E ectRi = Permit (A.20) 217 This is the case of inference rule 3 in Table 4.8. If that rule did not fire, that means one of the following conditions holds: ? T;RQ 6j= True, which implies KB j= (RQ) : : (T;True). This expres- sion will clash with the first conjunct in equation (A.20), thus the expression Indeterminate-Pu (RQ) is unsatisfiable. ? 8Ri 2 P : Ri;RQ 6j= Indeterminate whereE ectRi = Permit. The mapping of this expression will be: 8Ri 2P : KBj= (RQ) ::Indeterminate-Ri where E ectRi = Permit; which will clash with (F Indeterminate-Ri), which is only focused on rules where the e ect is Permit. ? 9Ri 2P : Ri;RQj= Permit ? this implies that for some Ri 2P, KBj= (RQ) : Permit-Ri which will clash with :Permit-Rj , rendering Indeterminate-Pu (RQ) unsatisfiable. Deny-Overrides To show that: RQ;Pj= Effect then KBj= (Effect;P)( (RQ)) in the Deny-Overrides case the same approach as in Permit-Overrides can be used. First-Applicable The mapping axiom for First-Applicable is defined as: 218 E ect-P (T)u G E ect-Riu :Deny-Rju:Permit-Rju:Indeterminate-Rj where i > j (A.21) Since the deduction rules are the same regardless of the e ect decision, we will simply use E ect in this proof as substitute for Permit, Deny or Indeterminate. P;RQ 6j= Effect means one of the following things holds(according to inference rules in Table 4.9): T;RQ6j= True. This implies KBj= (RQ) :: (T;True). This expression will clash with the first conjunct in equation (A.21), thus the expression E ect-Pu (RQ) is unsatisfiable. 8Ri 2P s.t. Ri;RQ6j= Effect. This implies that 8Ri 2P : KBj= (RQ) ::E ect-Ri Which means that there will be a clash between the term F E ect-Ri from equation (A.21) and (RQ). 9Rjs.t. j < i : Rj;RQ j= Indeterminate_Rj;RQ j= Permit_Rj;RQ j= Deny which means that 9Rj 2P where j < i : KBj= (RQ) : Indeterminate-RjtDeny-RjtPermit-Rj 219 which will always clash with :Deny-Rju:Permit-Rju:Indeterminate-Rj , thus rendering E ect-Pu (RQ) unsatisfiable. I showed in any of the three conditions that implies P;RQ 6j= Effect, KB j= (RQ) ::E ect-P, thus (P;RQ6j= Effect)!(KBj= (RQ) ::E ect-P) Only-One-Applicable We will show for the Permit/Deny case first, then for Indetermi- nate. Permit/Deny. The mapping axiom for Permit/Deny in First-Applicable is de- fined as: E ect-P (T)u G E ect-Riu :Deny-Rju:Permit-Rju:Indeterminate-Rj where i , j (A.22) P;RQ 6j= Effect means one of the following things holds(according to inference rules in Table 4.10): ? T;RQ6j= True. This implies KBj= (RQ) :: (T;True). This expression will clash with the first conjunct in equation (A.22). 220 ? 8Ri 2P s.t. Ri;RQ6j= Effect. This implies that 8Ri 2P : KBj= (RQ) ::E ect-Ri Which means that there will be a clash between the term F E ect-Ri from equation (A.22) and (RQ). ? 9Rj 2 P s.t. Rj;RQ j= E ectx where E ectx is a Permit, Deny or Indetermi- nate. This in turn implies KBj= (RQ) : Permit-RjtDeny-RjtIndeterminate-Rj which will always produce a clash with :Deny-Rju:Permit-Rju:Indeterminate-Rj . P;RQ6j= Indeterminate. The mapping axioms are defined in Section 6.1.4 as: Indeterminate-P (T)u G Indeterminate-Ri Indeterminate-P (T)u G ((Permit-RitDeny-Ri)u(Permit-RjtDeny-Rj)) where i , j (A.23) According to the inference rules in Table 4.10 , there are only two cases s.t. P;RQ6j= Indeterminate: ? 8Ri 2 P : R;RQ 6j= Indeterminate. This implies 8Ri 2 P : KB j= (RQ) : :Indeterminate-Ri which , in conjunction with the first axiom in (A.23), will 221 produce a clash. ? 8Ri;Rj 2 P where i , j : R;RQ 6j= E ectx _ R;RQ 6j= E ecty where E ectx;E ecty are either a Permit or a Deny. This, together with the results from the previous proofs implies that: 8Ri;Rj 2P where i , j : KBj= (RQ) ::E ectxt:E ecty which in conjunction with the mapping axioms in (A.23) implies that the ex- pression (RQ)uIndeterminate-P will be unsatisfiable. By covering all possible rule combining algorithms, I have shown that (P;RQ6j= Effect)!(KBj= (RQ) ::E ect-P) Proof of Lemma 12, If case. As in the previous proof, we itemize by the type of combin- ing algorithm. Notice that we will only cover Permit-Overrides and Deny-Overrides, since the other two combining algorithms can be handled same as in the Policy proof. Permit-Overrides PS;RQ j= Permit. This means that there exist a policy Pi 2 PS s.t. Pi;RQ j= Permit, and also TP;RQj=m Permit. This, together with our previous proofs (10), in turn implies that KB j= (RQ) : (Permit-Pi) and KB j= (RQ) : (TP;True). 222 Combining the two results we get: (RQ) : (TP;True)u (Permit-Pi;RQ) which implies (RQ) : Permit-PS. PS;RQ j= Deny. This means that there exist a policy Pi 2 PS s.t. Pi;RQ j= Deny, and all other rules Pj do not yield a Permit: 8Pj : Pj;RQ6j= Permit. Taking these prerequisites into account we have: KBj= (RQ) : (TP;True)u (Deny-Pi;RQ) KBj=8j : (RQ) :: (Permit-Pj;RQ) which implies (RQ) : Deny-PS. Deny-Overrides PS;RQj= Deny. This means that there exist a policy Pi 2PS s.t. Pi;RQj= Deny or Pi;RQ j= Indeterminate, and also TP;RQ j=m True. Thus, one of the following conditions holds: KBj= (Deny-Pi;RQ) or KBj= (Indeterminate-Pi;RQ) which implies (RQ) : Deny-PS. 223 PS;RQ j= Permit. This means that there exist a policy Pi 2 PS s.t. Pi;RQ j= Permit, and all other rules Pj do not yield a Deny or Indeterminate: 8Pj : Pj;RQ 6j= Deny_Pj;RQ 6j= Indeterminate. Taking these prerequisites into ac- count we have: KBj= (RQ) : (TP;True)u (Permit-Pi;RQ) KBj=8j : (RQ) :: (Deny-Pj;RQ)u: (Indeterminate-Pj;RQ) which implies (RQ) : Permit-PS. Proof of Lemma 12, Else case. As in the Policy case, the proof is split based on the di erent types of policy combining algorithms. Permit-Overrides KBj= (RQ) : Permit-PS. Since Permit-PS (True;T)u G Permit-Pi this means that (RQ) : (T) and (RQ) : Permit-Pi for some policy Pi 2 PS . Combining these results with Lemmas 10 and 6 implies that RQ satisfies both of the prerequisites of inference rule 1 in Table 4.11, thus PS;RQj= Permit. 224 KBj= (RQ) : Deny-PS. Since Deny-PS (True;T)u G Deny-Piu :Permit-Pj (A.24) This implies all of the following: ? (RQ) : (True;T), which by virtue of Lemma 6 means one of the prerequi- sites of rule 2 in Table 4.11 is satisfied. ? There exist some policy Pi 2P s.t. (RQ) : Deny-Pi. ? For all policies Pj 2PS , (RQ) ::Permit-Pj. These statements together with Lemma 10 satisfy the last prerequisite of rule 2 in Table 4.11. I have shown how with the three conditions above all of the prerequisites of the rule that entails PS;RQj= Deny are satisfied, so: KBj= (RQ) : Deny-PS!PS Permit-Overrides T Pi;RQj= Deny Deny-Overrides KBj= (RQ) : Deny-PS. Since Deny-PS (T)u G Deny-RitIndeterminate-Ri this means that (RQ) : (T) and either (RQ) : Deny-Pi or (RQ) : Indeterminate-Pi for some policy Pi 2 PS . Combining these results with Lemmas 10 and 6 implies 225 that RQ satisfies both of the prerequisites of inference rule 3 in Table 4.11, thus PS;RQj= Deny. KBj= (RQ) : Permit-PS. Since Permit-PS (T)u G Permit-Piu :Deny-Pju:Indeterminate-Pj (A.25) This implies all of the following: ? (RQ) : (T;True), which by virtue of Lemma 6 means one of the prerequi- sites of rule 4 in 4.11 is satisfied. ? There exist some policy Pi 2PS s.t. (RQ) : Permit-Pi. ? For all policies Pj 2 PS , (RQ) : :Deny-Pj and (RQ) : :Indeterminate-Pj. These statements together with Lemma 10 satisfy the last prerequisite of rule 4 in Table 4.11. With the above three conditions above all prerequisites of the rule that entails PS;RQj= Permit are satisfied, so: KBj= (RQ) : Permit-PS!PS Deny-Overrides T Pi;RQj= Permit First-Applicable Can be done in same manner as the Policy proof. Only-One-Applicable Can be done in same manner as the Policy proof. 226 After covering all of the rule combining algorithms , I proved that: KBj= (RQ) : E ect-PS!PS;RQj= E ect Proof of Lemma 13. This proof has a few sections, depending on what type of rule com- bining algorithm is being considered. Permit-Overrides PS;RQ 6j= Permit. Since inference rule 1 is the only one that can entail PS;RQ j= Permit in Table 4.11, if that rule doesn?t hold then: T;RQ6j= True_(8Pi 2PS : Pi;RQ6j= Permit) which together with Lemmas 7 and 11 implies that (KBj= (RQ) :: (T;True)) OR (8Pi 2PS : KBj= (RQ) ::Permit-Pi) Since Permit-PS (True;T)u G Permit-Pi ; when we try to evaluate satisfiability of Permit-PSu(: (T;True)t:Permit-Pi) we 227 will always get a clash, thus proving that KBj= (RQ) ::Permit-PS PS;RQ6j= Deny. The mapping axiom for Deny in Section 6.1.5 is defined as: Deny-PS (True;T)u G Deny-Piu :Permit-Pj (A.26) Since inference rule 2 in Table4.11 is the only one that can entail PS;RQ j= Deny, that means that one of the following happened: ? T;RQ 6j= True, which implies KB j= (RQ) : : (T;True). Notice that this expression will clash with the first conjunct in equation (A.26). ? 8Pi 2 PS : Pi;RQ 6j= Deny. This means that for each Pi 2 PS, KB j= (RQ) : :Deny-Pi, which means that there always will be a clash with the first item in the second conjunct in equation (A.26) (F Deny-Pi). ? 9Pi 2 PS : Pi;RQ j= Permit ? this implies that for some Pi 2 PS, KB j= (RQ) : Permit-Pi which again will produce a clash so the expression Deny-PSu (RQ) will be unsatisfiable. Since in all three cases the expression Deny-PSu (RQ) will be unsatisfiable, it will always follow that KBj= (RQ) ::Deny-PS for this case. Deny-Overrides The proof is slightly di erent than the Permit-Overrides case. 228 PS;RQ 6j= Deny. Since inference rule 3 is the only one that can entail PS;RQ j= Deny in Table 4.11, that implies: T;RQ6j= True_(8Pi 2PS : Pi;RQ6j= Deny^Pi;RQ6j= Indeterminate) which together with Lemmas 7 and 11 implies (KBj= (RQ) :: (T;True)) OR (8Pi 2PS : KBj= (RQ) ::Indeterminate-Riu:Deny-Ri) Since Deny-PS (T)u G Deny-RitIndeterminate-Ri ; when we try to evaluate satisfiability of Deny-PSu(: (T;True)t(:Indeterminate-Riu:Deny-Ri)) we will always get a clash, thus proving that KBj= (RQ) ::Deny-IDPS PS;RQ 6j= Permit. The mapping axiom for Permit in Section 6.1.5 is defined as 229 follows: Permit-PS (T)u G Permit-Piu :Deny-Pju:Indeterminate-Pj (A.27) Since inference rule 4 in Table 4.11 is the only one that can entail PS;RQ j= Permit, that means that one of the following holds: ? T;RQ 6j= True, which implies KB j= : (RQ) : (T;True). Notice that this expression will clash with the first conjunct in equation (A.27), rendering Permit-PSu (RQ) unsatisfiable. ? 8Pi 2PS : Pi;RQ6j= Permit. This means that for each Pi 2PS, KBj= (RQ) : :Permit-Pi, which means that there always will be a clash with the expression in equation (A.27) (F Permit-Ri). ? 9Pj 2 PS : Pj;RQ j= Deny _ Pj;RQ j= Indeterminate. This means that there exists a Pi 2 PS s.t. KB j= (RQ) : Indeterminate-Pi tDeny-Pi, which means that there always will be a clash with the expression in equation (A.27) :Deny-Pju:Indeterminate-Pj . Since I showed that in all three cases the expression Permit-P u (RQ) will be unsatisfiable, that it will always follow that KBj= (RQ) ::Permit-P for this case. First-Applicable Proof can be done in same way as for the Policy case (since the semantics is the same). 230 Only-One-Applicable Proof is same as for the Policy case.. 231 Bibliography [1] Aaauthreach project information page. Available at http://staff.science. uva.nl/~demch/projects/aaauthreach/. [2] BIANCA Application. Available at http://clarkparsia.com/clients/. [3] eXist: Open Source Native XML Database. Available at http://exist. sourceforge.net/. [4] Fedora Authorization with XACML Policy Enforcement. Available at http://www.fedora.info/download/2.1b/userdocs/server/security/ AuthorizationXACML.htm. [5] Role-Based Access Control (RBAC) Scenarios. Available at http://www.va. gov/RBAC/scenarios.asp. [6] Semantics of Business Vocabulary and Business Rules (SBVR). Available at http://www.businessrulesgroup.org/sbvr.shtml. [7] Veterans Health Information Systems and Technology Architecture (VISTA). Available at http://www.va.gov/vista_monograph/. [8] Dod trusted computer system evaluation criteria. Technical Report CSC-STD- 00l-83, Department of Defense, 1985. Available at http://nsi.org/Library/ Compsec/orangebo.txt. [9] A guide to understanding discretionary access control in security systems. Techni- cal Report NCSC-TG-003, National Computer Security Center, 1987. Available at http://www.fas.org/irp/nsa/rainbow/tg003.htm. [10] Role based access control. Technical Report ANSI INCITS 359-2004, NIST, 2004. Available at http://csrc.nist.gov/rbac/. [11] Margrave Continue Example, 2005. Available at http://www.cs.brown. edu/research/plt/software/margrave/versions/01-01/examples/ continue/. [12] Mart??n Abadi, Michael Burrows, Butler Lampson, and Gordon Plotkin. A calcu- lus for access control in distributed systems. ACM Transactions on Programming Languages and Systems, 15(4):706?734, September 1993. [13] Dhiah el Diehn I. Abou-Tair, Stefan Berlik, and Udo Kelter. Enforcing privacy by means of an ontology driven xacml framework. Information Assurance and Security, 2007. IAS 2007. Third International Symposium on, pages 279?284, 29- 31 Aug. 2007. 232 [14] Dakshi Agrawal, James Giles, Kang-Won Lee, and Jorge Lobo. Policy ratification. In POLICY ?05: Proceedings of the Sixth IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY?05), pages 223?232, Washington, DC, USA, 2005. IEEE Computer Society. [15] A. Anderson. A comparison of two privacy policy languages: Epal and xacml, 2005. [16] Anne Anderson. XACML References, v1.65. Available at http://docs. oasis-open.org/xacml/references/xacmlRefsV1.65.html. [17] Anne Anderson. Core and hierarchical role based access control (rbac) profile of xacml v2.0, February 2005. Available at http: //www.docs.o\discretionary{-}{}{}asis-open.org/xacml/2.0/ access_control-xacml-2.0-rbac-profile1-spec-os.pdf. [18] Anne Anderson. Hierarchical resource profile of XACML, February 2005. Available at http://docs.oasis-open.org/xacml/2.0/access_ control-xacml-2.0-hier-profile-spec-os.pdf. [19] Anne Anderson. Domain independent, composable web services policy assertions. In IEEE POLICY Workshop, 2006. [20] Anne Anderson. Multiple resource profile of XACML, November 2007. Avail- able at http://www.oasis-open.org/committees/download.php/26154/ xacml-3.0-hie%2Cmul%2Cdsig%2Cpriv-profiles-wd01.zip. [21] Claudio Agostino Ardagna, Ernesto Damiani, Sabrina De Capitani di Vimercati, Cristiano Fugazza, and Pierangela Samarati. O ine expansion of xacml policies based on p3p metadata. In ICWE, pages 363?374, 2005. [22] Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementa- tion, and Applications. Cambridge University Press, 2003. [23] Franz Baader and Philipp Hanschke. A scheme for integrating concrete domains into concept languages. Technical Report RR-91-10, Deutsches Forschungszen- trum f?ur K?unstliche Intelligenz GmbH Erwin-Schr?odinger Strasse Postfach 2080 67608 Kaiserslautern Germany, 1991. [24] Franz Baader and Ulrike Sattler. An overview of tableau algorithms for description logics. Studia Logica, 69:5?40, 2001. [25] Chitta Baral and V. S. Subrahmanian. Stable and extension class theory for logic programs and default logics. J. Autom. Reasoning, 8(3):345?366, 1992. 233 [26] Lujo Bauer, Scott Garriss, and Michael K. Reiter. Distributed proving in access- control systems. In SP ?05: Proceedings of the 2005 IEEE Symposium on Security and Privacy, pages 81?95, Washington, DC, USA, 2005. IEEE Computer Society. [27] Moritz Becker, Cedric Fournet, and Andrew Gordon. Design and semantics of a decentralized authorization language. Computer Security Foundations Symposium, 2007. CSF ?07. 20th IEEE, pages 3?15, 6-8 July 2007. [28] David E. Bell and Leonard J. LaPadula. Secure computer systems: Unified expo- sition and multics interpretation. Technical report, The MITRE Corporation, July 1975. [29] Elisa Bertino, Piero Andrea Bonatti, and Elena Ferrari. Trbac: A temporal role- based access control model. ACM Trans. Inf. Syst. Secur., 4(3):191?233, 2001. [30] Elisa Bertino, Francesco Buccafurri, Elena Ferrari, and Pasquale Rullo. An autho- rization model and its formal semantics. In ESORICS ?98: Proceedings of the 5th European Symposium on Research in Computer Security, pages 127?142, London, UK, 1998. Springer-Verlag. [31] Elisa Bertino, Barbara Catania, Elena Ferrari, and Paolo Perlasca. A logical frame- work for reasoning about access control models. ACM Trans. Inf. Syst. Secur., 6(1):71?127, 2003. [32] Elisa Bertino, Pierangela Samarati, and Sushil Jajodia. Authorizations in relational database management systems. In CCS ?93: Proceedings of the 1st ACM confer- ence on Computer and communications security, pages 130?139, New York, NY, USA, 1993. ACM. [33] Claudio Bettini, Sushil Jajodia, X. Sean Wang, and Duminda Wijesekera. Provi- sions and obligations in policy management and security applications. In VLDB ?02: Proceedings of the 28th international conference on Very Large Data Bases, pages 502?513. VLDB Endowment, 2002. [34] Piero A. Bonatti, Sabrina De Capitani di Vimercati, and Pierangela Samarati. An algebra for composing access control policies. Information and System Security, 5(1):1?35, 2002. [35] D. Brickley and R.V. Guha. Resource Description Framework (RDF) Model and Syntax Specification. W3C Recommendation submitted 22 February 1999 http: //www.w3.org/TR/1999/REC-rdf-syntax-19990222/. [36] Jery Bryans. Reasoning about xacml policies using csp. In SWS ?05: Proceedings of the 2005 workshop on Secure web services, pages 28?35, New York, NY, USA, 2005. ACM Press. [37] S. Ceri, G. Gottlob, and L. Tanca. What you always wanted to know about datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering, 01(1):146?166, 1989. 234 [38] Jan Chomicki, Jorge Lobo, and Shamin Naqvi. A logic programming approach to conflict resolution in policy management. In Anthony G. Cohn, Fausto Giunchiglia, and Bart Selman, editors, KR2000: Principles of Knowledge Rep- resentation and Reasoning, pages 121?132, San Francisco, 2000. Morgan Kauf- mann. [39] Brickley D. and R.V. Guha. RDF Vocabulary Description Language 1.0: RDF Schema. http://www.w3.org/TR/rdf-schema/, February 2004. [40] Ernesto Damiani, Sabrina De Capitani di Vimercati, Cristiano Fugazza, and Pi erangela Samarati. Extending policy languages to the semantic web. In ICWE, pages 330?343, 2004. [41] Ernesto Damiani, Sabrina De Capitani di Vimercati, and Pierangela Samarati. New paradigms for access control in open environments. In Proceedings of the Fifth IEEE International Symposium on Signal Processing and Information Technology, December 2005. [42] Dan Lin and Prathima Rao and Elisa Bertino and Jorge Lobo and Ninghui Li. EXAM - a Comprehensive Environment for the Analysis of Access Control Poli- cies, 2007. [43] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expressive power of logic programming. In IEEE Conference on Computa- tional Complexity, pages 82?101, 1997. [44] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expressive power of logic programming. ACM Comput. Surv., 33(3):374?425, 2001. [45] Mike Dean, Dan Connolly, Frank van Harmelen, James Hendler, Ian Horrocks, Deborah L. McGuinness, Peter F. Patel-Schneider, and Lynn Andrea Stein. Web Ontology Language (OWL) Reference Version 1.0. W3C Working Draft 12 November 2002 http://www.w3.org/TR/2002/WD-owl-ref-20021112/. [46] John DeTreville. Binder, a logic-based security language. In SP ?02: Proceedings of the 2002 IEEE Symposium on Security and Privacy, page 105, Washington, DC, USA, 2002. IEEE Computer Society. [47] Sabrina De Capitani di Vimercati, Pierangela Samarati, and Sushil Jajodia. Poli- cies, models, and languages for access control. In In Proc. of the Workshop on Databases in Networked Information Systems, 2005. [48] Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. Specifying and reasoning about dynamic access-control policies. In 3rd International Joint Con- ference on Automated Reasoning (IJCAR), 2006. [49] Jayne Dutra. NASA Taxonomy 2.0. Available at http://nasataxonomy.jpl. nasa.gov/. 235 [50] Kathi Fisler, Shriram Krishnamurthi, Leo A. Meyerovich, and Michael Carl Tschantz. Verification and change-impact analysis of access-control policies. In ICSE ?05: Proceedings of the 27th international conference on Software engineer- ing, pages 196?205, 2005. [51] M. Fujita, P. C. McGeer, and J. C.-Y. Yang. Multi-terminal binary decision dia- grams: An e cient datastructure for matrix representation. Form. Methods Syst. Des., 10(2-3):149?169, 1997. [52] Rita Gavriloaie, Wolfgang Nejdl, Daniel Olmedilla, Kent Seamons, and Marianne Winslett. No registration needed: How to use declarative policies and negotiation to access sensitive resources on the semantic web. In European Semantic Web Symposium, May 2004. [53] A. Van Gelder. The alternating fixpoint of logic programs with negation. In PODS ?89: Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, pages 1?10, New York, NY, USA, 1989. ACM. [54] Michael Gelfond and Vladimir Lifschitz. The stable model semantics for logic programming. In Robert A. Kowalski and Kenneth Bowen, editors, Proceedings of the Fifth International Conference on Logic Programming, pages 1070?1080, Cambridge, Massachusetts, 1988. The MIT Press. [55] Pierre Genev`es, Nabil Laya??da, and Alan Schmitt. E cient static analysis of xml paths and types. In PLDI, pages 342?351, 2007. [56] Benjamin N. Grosof. Diplomat: Compiling prioritized default rules into ordinary logic programs, for e-commerce applications. In AAAI/IAAI, pages 912?913, 1999. [57] Dimitar P. Guelev, Mark Ryan, and Pierre-Yves Schobbens. Model-checking ac- cess control policies. In ISC, pages 219?230, 2004. [58] Volker Haarslev and Ralf M?oller. High performance reasoning with very large knowledge bases: A practical case study. In IJCAI, pages 161?168, 2001. [59] Joseph Y. Halpern and Vicky Weissman. Using first-order logic to reason about policies. In In Proceedings of the Computer Security Foundations Workshop (CSFW?03), Los Alamitos, CA, USA, 2003. IEEE Computer Society. [60] Joseph Y. Halpern and Vicky Weissman. A formal foundation for xrml. In CSFW ?04: Proceedings of the 17th IEEE workshop on Computer Security Foundations, page 251, Washington, DC, USA, 2004. IEEE Computer Society. [61] Michael A. Harrison, Walter L. Ruzzo, and Je rey D. Ullman. Protection in oper- ating systems. Commun. ACM, 19(8):461?471, 1976. [62] HL7 Security Technical Committee. Role Based Access Control (RBAC) Health- care Permission Catalog. Available at http://www.va.gov/RBAC/docs/Stds_ 20071129_SW_22_5_HL7_RBAC_Healthcare_Permission_Catalog_v3_38. pdf. 236 [63] C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666? 677, 1978. [64] I. Horrocks and U. Sattler. Ontology reasoning in the SHOQ(D) description logic. In Proceedings of the Seventeenth International Joint Conference on Artificial In- telligence, 2001. [65] Ian Horrocks. The fact system. http://www.cs.man.ac.uk/~horrocks/ FaCT/. [66] Graham Hughes and Tevfik Bultan. Automated verification of access control poli- cies (technical report). Technical Report 2004-22, Department of Computer Sci- ence, University of California, Santa Barbara, September 2004. [67] Graham Hughes and Tevfik Bultan. Automated Verification of XACML Poli- cies Using a SAT Solver. In Proceedings of the 7th International Conference on Web Engineering, Workshop on Web Quality, Verification and Validation (WQVV), pages 378?392, July 2007. [68] Polar Humenn. The Formal Semantics of XACML, October 2003. Available at http://lists.oasis-open.org/archives/xacml/200310/pdf00000.pdf. [69] Keith Irwin, Ting Yu, and William H. Winsborough. On the modeling and analysis of obligations. In CCS ?06: Proceedings of the 13th ACM conference on Computer and communications security, pages 134?143, New York, NY, USA, 2006. ACM. [70] Daniel Jackson. Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol., 11(2):256?290, 2002. [71] Sushil Jajodia, Pierangela Samarati, Maria Luisa Sapino, and V. S. Subrahma- nian. Flexible support for multiple access control policies. Database Systems, 26(2):214?260, 2001. [72] Sushil Jajodia, Pierangela Samarati, V. S. Subrahmanian, and Eliza Bertino. A unified framework for enforcing multiple access control policies. In SIGMOD ?97: Proceedings of the 1997 ACM SIGMOD international conference on Management of data, pages 474?485, New York, NY, USA, 1997. ACM Press. [73] Sushil Jajodia and Duminda Wijesekera. A flexible authorization framework for e-commerce. In ICDCIT, pages 336?345, 2004. [74] Rasool Jalili and Mohsen Rezvani. Specification and verification of security poli- cies in firewalls. In EurAsia-ICT ?02: Proceedings of the First EurAsian Con- ference on Information and Communication Technology, pages 154?163, London, UK, 2002. Springer-Verlag. [75] Trevor Jim. Sd3: A trust management system with certified evaluation. In SP ?01: Proceedings of the 2001 IEEE Symposium on Security and Privacy, page 106, Washington, DC, USA, 2001. IEEE Computer Society. 237 [76] Diane Jordan and John Evdemon. Business Process Execution Language (BPEL). Available at http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2. 0-OS.html. [77] L. et al Kagal. A policy language for a pervasive computing environment. In IEEE 4th International Workshop on Policies for Distributed Systems and Networks, June 2003. [78] Lalana Kagal, Tim Berners-Lee, Dan Connolly, and Daniel Weitzner. Using se- mantic web technologies for policy management on the web. In 21st National Conference on Artificial Intelligence (AAAI), 2006. [79] Aditya Kalyanpur, Bijan Parsia, Evren Sirin, and Bernardo Cuenca-Grau. Repair- ing unsatisfiable concepts in owl ontologies. In Proceedings of European Semantic Web Conference (ESWC), 2006. [80] Aditya Kalyanpur, Bijan Parsia, Evren Sirin, and James Hendler. Debugging un- satisfiable classes in owl ontologies. Journal of Web Semantics - Special Issue of the Semantic Web Track of WWW2005, 3(4), 2005. [81] Kendall Clark and Andrew Schain and Bijan Parsia. Semantic Web @ NASA. In XTech Conference, 2006. [82] Racer Systems GmbH & Co. KG. Racerpro user guide, October 2007. [83] Vladimir Kolovski, James Hendler, and Bijan Parsia. Analyzing web access control policies. In WWW ?07: Proceedings of the 16th international conference on World Wide Web, pages 677?686, New York, NY, USA, 2007. ACM. [84] Vladimir Kolovski, Bijan Parsia, Yarden Katz, and James Hendler. Representing Web Service Policies in OWL-DL. In Proc. of the Int. Semantic Web Conference (ISWC), 2005. [85] N. Li, B. Grosof, and J. Feigenbaum. A nonmonotonic delegation logic with pri- oritized conflict handling, 2000. [86] N. Li and J. Mitchell. Datalog with constraints: A foundation for trust management languages, 2003. [87] Ninghui Li, Benjamin N. Grosof, and Joan Feigenbaum. A practically imple- mentable and tractable delegation logic. In IEEE Symposium on Security and Pri- vacy, pages 27?42, 2000. [88] Ninghui Li, Benjamin N. Grosof, and Joan Feigenbaum. Delegation logic: A logic- based approach to distributed authorization. ACM Trans. Inf. Syst. Secur., 6(1):128? 171, 2003. [89] Ninghui Li and John Mitchel. Understanding spki/sdsi using first-order logic, 2003. 238 [90] Ninghui Li, John C. Mitchell, and William H. Winsborough. Design of a role-based trust management framework. In Proceedings of the 2002 IEEE Symposium on Security and Privacy, pages 114?130. IEEE Computer Society Press, May 2002. [91] Ninghui Li and Mahesh V. Tripunitara. Security analysis in role-based access con- trol. ACM Transactions on Information Systems Security, 9(4):391?420, 2006. [92] Ninghui Li, William H. Winsborough, and John C. Mitchell. Beyond proof-of- compliance: Safety and availability analysis in trust management. In IEEE Sym- posium on Security and Privacy, May 2003. [93] Dan Lin, Prathima Rao, Elisa Bertino, and Jorge Lobo. An approach to evaluate policy similarity. In SACMAT ?07: Proceedings of the 12th ACM symposium on Access control models and technologies, pages 1?10, New York, NY, USA, 2007. ACM. [94] Chuchang Liu, Patrick McLean, and Maris A. Ozols. Combining logics for mod- elling security policies. In ACSC ?05: Proceedings of the Twenty-eighth Aus- tralasian conference on Computer Science, pages 323?332, Darlinghurst, Aus- tralia, Australia, 2005. Australian Computer Society, Inc. [95] Hal Lockhart, Bill Parducci, and Anne Anderson. Web services pro- file of xacml,(ws-xacml) version 1.0. Available at http://www. oasis-open.org/committees/download.php/21490/xacml-3. 0-profile-webservices-spec-v1.0-wd-8-en.pdf. [96] C. Lutz. NExpTime-complete description logics with concrete domains. In Rajeev Gor?e, Alexander Leitsch, and Tobias Nipkow, editors, Proceedings of the Inter- national Joint Conference on Automated Reasoning, number 2083, pages 45?60, Siena, Italy, 2001. Springer Verlag. [97] C. Lutz. Description logics with concrete domains?a survey. In Advances in Modal Logics Volume 4. King?s College Publications, 2003. [98] Evan Martin, Tao Xie, and Ting Yu. Defining and measuring policy coverage in testing access control policies. In Proceedings of the 8th International Confer- ence on Information and Communications Security (ICICS 2006), pages 139?158, December 2006. [99] Fabio Massacci. Reasoning about security: A logic and a decision method for role- based access control. In First International Joint Conference on Qualitative and Quantitative Practical Reasoning ECSQARU-FAPR, pages 421?435, 1997. [100] Imtiaz Mohammed and David M. Dilts. Design for dynamic user-role-based secu- rity. Comput. Secur., 13(9):661?671, 1994. [101] Moritz Becker and Peter Sewell. Cassandra: Distributed access control policies with tunable expressiveness. In POLICY ?04: Proceedings of the Fifth IEEE 239 International Workshop on Policies for Distributed Systems and Networks (POL- ICY?04), page 159, Washington, DC, USA, 2004. IEEE Computer Society. [102] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Cha : engineering an e cient sat solver. In DAC ?01: Proceedings of the 38th conference on Design automation, pages 530?535, New York, NY, USA, 2001. ACM. [103] Till Mossakowski, Michael Drouineaud, and Karsten Sohr. A temporal-logic ex- tension of role-based access control covering dynamic separation of duties. time- ictl, 00:83, 2003. [104] Boris Motik. Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Univesitt Karlsruhe, Germany, January 2006. [105] Boris Motik, Peter F. Patel-Schneider, and Ian Horrocks. OWL 1.1 Web Ontology Language:Structural Specification and Functional-Style Syntax . Editor?s Draft of 23 May 2007. [106] Matunda Nyanchama and Sylvia Osborn. Role-based security, object oriented databases and separation of duty. SIGMOD Rec., 22(4):45?51, 1993. [107] Matunda Nyanchama and Sylvia Osborn. The role graph model and conflict of interest. ACM Trans. Inf. Syst. Secur., 2(1):3?33, 1999. [108] B. Orgun and J. Vu. HL7 ontology and mobile agents for interoperability in het- erogeneous medical information systems. Computers in Biology and Medicine: Special Issue on Medical Ontologies, 36(7):817?836, 2006. [109] Bijan Parsia and Evren Sirin. Pellet: An OWL DL reasoner. In Third International Semantic Web Conference - Poster, 2004. [110] Pellet. Pellet - owl dl reasoner, 2003. http://www.mindswap.org/2003/pellet. [111] Raghu Ramakrishnan and Je rey D. Ullman. A survey of research on deductive database systems. Journal of Logic Programming, 23(2):125?149, 1993. [112] Riccardo Pucella and Vicky Weissman. A Formal Foundation for ODRL. In In Proceedings of the Workshop on Issues in the Theory of Security (WITS-04), 2006. [113] Erik Rissanen. eXtensible Access Control Markup Language (XACML) Version 3.0 (Core Specification and Schemas), May 2007. Available at http://www.oasis-open.org/committees/download.php/23950/ xacml-3.0-core-wd-02.zip. [114] Erik Rissanen, Hal Lockhart, and Tim Moses. Xacml administra- tive policy version 1.0, working draft 17, May 2007. Available at http://www.oasis-open.org/committees/download.php/23951/ xacml-3.0-admininstration-v1-wd-17.zip. 240 [115] Ronald Rivest and Butler Lampson. A Simple Distributed Security Infrastructure (SDSI). [116] Ravi S. Sandhu, Edward J. Coyne, Hal L. Feinstein, and Charles E. Youman. Role- based access control models. IEEE Computer, 29(2):38?47, 1996. [117] Andreas Schaad and Jonathan D. Mo ett. A lightweight approach to specification and analysis of role-based access control extensions. In SACMAT ?02: Proceedings of the seventh ACM symposium on Access control models and technologies, pages 13?22, New York, NY, USA, 2002. ACM Press. [118] Michael A. Smith, Andrew J. Schain, Kendall Grant Clark, Arlen Gri ey, and Vladimir Kolovski. Mother, May I? OWL-based Policy Management at NASA. In Proc. of the Third International Workshop on OWL: Experiences and Directions (OWLED), June 2007. [119] Christoph Tempich, Helena Sofia Pinto, and Ste en Staab. Ontology engineering revisited: An iterative case study. In ESWC, pages 110?124, 2006. [120] Dmitry Tsarkov and Ian Horrocks. Description logic reasoner: System description. In IJCAR, pages 292?297, 2006. [121] Michael Carl Tschantz and Shriram Krishnamurthi. Towards reasonability prop- erties for access-control policy languages. In SACMAT ?06: Proceedings of the eleventh ACM symposium on Access control models and technologies, pages 160? 169, New York, NY, USA, 2006. ACM Press. [122] A. Uszokand and J. Bradshaw. Kaos policies for web services. In W3C Workshop on Constraints and Capabilities for Web Servies, October 2004. [123] Allen van Gelder, Kenneth Ross, and John S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3):620?650, 1991. [124] V.Haarslev and R.Moeller. Racer system description. In Proc. of the Joint Conf. on Automated Reasoning (IJCAR 2001). Volume 2083 of Lecture Notes in Artificial Intelligence, pages 701-705, 2001. [125] S. H. von Solms and Isak van der Merwe. The management of computer security profiles using a role-oriented approach. Comput. Secur., 13(9):673?680, 1994. [126] Daniel J. Weitzner, Jim Hendler, Tim Berners-Lee, and Dan Connolly. Creating a policy-aware web: Discretionary, rule-based access for the world wide web. [127] Marianne Winslett, Charles C. Zhang, and Piero A. Bonatti. Peeraccess: a logic for distributed authorization. In CCS ?05: Proceedings of the 12th ACM conference on Computer and communications security, pages 168?179, New York, NY, USA, 2005. ACM Press. 241 [128] Thomas Y. C. Woo and Simon S. Lam. Authorizations in distributed systems: A new approach. Journal of Computer Security, 2(2-3):107?136, 1993. [129] WS-Policy. Web services policy framework (ws-policy). http://www- 106.ibm.com/developerworks/library/specification/ws-polfram/. [130] Bwolen Yang, Randal E. Bryant, David R. O?Hallaron, Armin Biere, Olivier Coud- ert, Geert Janssen, Rajeev K. Ranjan, and Fabio Somenzi. A performance study of bdd-based model checking. In FMCAD ?98: Proceedings of the Second Interna- tional Conference on Formal Methods in Computer-Aided Design, pages 255?289, London, UK, 1998. Springer-Verlag. [131] Nan Zhang, Mark D. Ryan, and Dimitar Guelev. Evaluating access control poli- cies through model checking. In Eighth Information Security Conference (ISC05), 2005. [132] Chen Zhao, NuerMaimaiti Heilili, Shengping Liu, and Zuoquan Lin. Representa- tion and reasoning on rbac: A description logic approach. In ICTAC, pages 381? 393, 2005. 242