Technical Communications of ICLP 2015. Copyright with the Authors. 1 Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming JOOHYUNG LEE and YI WANG Arizona State University, Tempe, AZ, USA (e-mail: {joolee,ywang485}@asu.edu) YU ZHANG Intel, Chandler, AZ, USA (e-mail: yzhan289@asu.edu) submitted 29 April 2015; accepted 5 June 2015 Abstract XACML is an XML-based declarative access control language standardized by OASIS. Its latest version 3.0 has several new features including the concept of delegation for decentralized administration of access control. Though it is important to avoid unintended consequences of ill-designed policies, delegation makes formal analysis of XACML policies highly complicated. In this paper, we present a logic-based approach to XACML 3.0 policy analysis. We formulate XACML 3.0 in Answer Set Programming (ASP) and use ASP solvers to perform automated reasoning about XACML policies. To the best of our knowledge this is the first work that fully captures the XACML delegation model in a formal executable language. KEYWORDS: Policy, XACML, Delegation, Answer Set Programming 1 Introduction Policy-based computing is being widely adopted to accommodate security requirements for large, complex, distributed, heterogenous computing environments. Extensible Access Control Markup Language (XACML) is an XML-based declarative access control policy language, stan- dardized by the Organization for the Advancement of Structured Information Standards (OA- SIS). The latest version, XACML 3.0, was standardized in 2013, and is significantly more en- hanced and expressive than the previous version by introducing several new features, such as multiple decision profile, delegation, obligation/advice expressions, and more enhanced com- bining algorithms. In particular, delegation in XACML 3.0 is an important addition to facilitate decentralized administration of access control for a large scale distributed systems. In the previ- ous version of XACML, any policy is assumed to be trusted, but how to ensure such trust was not specified. This actually puts strict constraints on policy makers’ authority verification in practice and therefore restricts the number of policy issuers to be handful, which does not meet the need of modern distributed systems. In contrast, in XACML 3.0, anyone can write policies to permit or deny an access, but not all these policies would be trusted. XACML 3.0 provides a means of ensuring how untrusted policies are properly authorized by a delegation chain from trusted policies. This mechanism provides a flexible decentralized access control management reduc- ing the administration cost of the organization. On the other hand, it makes formal analysis of XACML 3.0 highly complicated. Lack of such analysis jeopardizes safety-critical applications by being vulnerable to unexpected consequences originating from complex dependencies among distributed policies. Due to the complexity, there are few implementations that fully support the delegation model in XACML 3.0. 2 J. Lee, Y. Wang and Y. Zhang In this paper, we present a logic-based approach to formal reasoning about XACML policies. We turn the semi-formal XACML 3.0 specification from the OASIS standard document (OASIS 2013) into a formal description, turn that further into the language of Answer Set Programming (ASP), and show how ASP solvers can be used to perform various logical reasoning and analysis of policies. Our goal is not on improving XACML, but on formalizing the language as described in the standard document as closely as possible.1 This is a challenging task. The syntax of XACML is XML, which is verbose. The semantics there is described in English, which reads human- friendly, but is lacking some precision and is sometimes ambiguous. In order to facilitate the formulation of XACML in ASP, we first construct an abstract syntax and the formal seman- tics of XACML. It is rather straightforward to turn that further into ASP, which illustrates the expressivity of ASP. In comparison with the previous work on formalizing XACML 2.0 (Ahn et al. 2010; Hughes and Bultan 2004; Bryans 2005; Fisler et al. 2005; Kolovski et al. 2007), which mostly focused on representing combining algorithms, our work provides a comprehensive coverage of XACML 3.0, such as delegation, the new structure of htargeti, new combining algorithms, and inde- terminate values. The combining algorithms of XACML 2.0 were formalized in other logical languages as well, such as description logic (Kolovski et al. 2007) and the language of Alloy (Hughes and Bultan 2004), but it is not apparent how those approaches can be extended to han- dle delegation, which requires reasoning about reachability. To the best of our knowledge, the work presented here is the first one that fully captures the XACML 3.0 delegation model in a formal executable language. Due to the space limit, we defer the description of other features in a longer version. 2 XACML 3.0 2.1 Access vs. Administrative Policies in XACML 3.0 In XACML 3.0, policies are either access policies or administrative policies. An access policy specifies access rights based on the attributes of possible access requests. This type of policies is present in XACML 2.0, but XACML 3.0 has added an optional new element hPolicyIssueri, whose authority needs to be verified. An example is “Bob says Alice can access printers,” where Bob is the policy issuer, Alice is the requesting subject, and printer is the requested resource. An administrative policy specifies the authorization of a delegate to issue policies regarding the attributes. This type of policies also has an optional element hPolicyIssueri, and may need to be further verified. An example is “Carol says Bob has the right to let Alice access printers.” This does not mean that the delegate Bob has the right unless the authority of the policy issuer Carol is verified. The process of finding a valid authorization of a delegation is called reduction. 2.2 Abstract Syntax of XACML 3.0 XACML is mainly an Attribute Based Access Control system (ABAC), in which attributes as- sociated with a user, an action, or a resource are inputs to the decision of whether the user may access the resource in a particular way. Table 1 summarizes each syntax component of XACML 3.0. An attribute consists of AttrIdentifier and AttrVal, and an AttrIdentifier in turn consists of an attrID, a category, and an issuer. The 1 Thus comparing XACML with other policy languages, such as SecPAL, is out of scope of this paper. Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming 3 Component Abstraction Component Abstraction PDP hh(Policy|PolicySet)* i, combAlgi Issuer {hAttrIdentifier, AttrVali* } PolicySet hTarget, h(Policy|PolicySet)+ i, Request {hAttrIdentifier, AttrVali+ } combAlg, Issuer, maxDelDepi maxDelDep a nonnegative integer or inf (∞) Policy hTarget, hRule+ i, combAlg, Issuer, combAlg po | do | pud | dup | fa | ooa | ... maxDelDepi attrID a string Rule hTarget, effect, conditioni attrIssuer a string ∗ Target {AnyOf } dataType string | integer | date |... AnyOf {AllOf + } value a value of the corresponding data-type AllOf {Match+ } effect permit | deny Match hmFunc, AttrRetriever, AttrVali condition a boolean function call AttrIdentifier hattrID, category, attrIssueri mFunc a boolean function AttrVal hdataType, valuei category subject | resource | action | ... AttrRetriever hAttrIdentifier, mustBePresenti mustBePresent true | false Table 1: XACML 3.0 elements abstraction AttrVal of the attribute is a value of a specific datatype. An attribute retriever (AttrRetriever) consists of an AttrIdentifier and a Boolean value mustBePresent. A request is formed by con- joining all the attributes in the request context. A match is a simple attribute matching condition. It contains an AttrRetriever for the attribute to be matched, a value (AttrVal) that the identified attribute is supposed to match, and a matching function (mFunc) for comparison between the actual value and the value specified in the match. An allOf represents the conjunction of matchs. An anyOf represents the disjunction of allOf s. A target represents the conjunction of anyOf s, and in this way it expresses a complex attribute matching condition. A rule represents a single statement about whether a request satisfying certain conditions (expressed by condition and target elements) should be granted access or not. The intended effect of the rule to applicable requests is specified by its effect. A policy consists of a set of rules, a target, a “rule-combining algorithm” (combAlg), which specifies the way how conflicting decisions from children rules are combined, a set of at- tributes describing the policy’s issuer, and a nonnegative integer called maximum delegation depth (maxDelDep), which limits the depth of any delegation that is authorized by this policy. The issuer of a policy can be null, indicating that the policy is trusted. A policy set is similar to a policy except that it contains a set of children policies and policy sets. The PDP consists of the set of all top level policies/policy sets and a policy-combining algorithm. pdp deny-unless-permit ps1 p1 ps2 Issuer: trusted Issuer: trusted Issuer: record_admin CombAlg: first-applicable Target: CombAlg: first-applicable Target: any Delegate: record_admin Target: any DelegatedResource: record MaxDep: 5 RuleEffect: permit MaxDep: 2 p6 p7 p3 p4 p5 Issuer: trusted p2 Issuer: trusted Issuer: trusted Issuer: trusted Issuer: hospital_manager Target: Issuer: trusted Target: Target: Target: Target: Delegate: doctor Target: Delegate: hospital_manager Subject: patient Subject: doctor Subject: doctor DelegatedSubject: patient Subject: patient DelegatedSubject: doctor Resource: record Resource: record Resource: record DelegatedResource: record Resource: record DelegatedResource: record Action: read Action: modify Action: modify/read DelegatedAction: read Action: modify DlegatedAction: modify/read IsBusinessHour: false IsBusinessHour: false IsBusinessHour: true DelegatedIsBusinessHour:true RuleEffect: deny RuleEffect: permit RuleEffect: deny RuleEffect: deny RuleEffect: permit RuleEffect: permit MaxDep:3 MaxDep: 5 Fig. 1: Policy Hierarchy of Example 1 Example 1 Access request 4 J. Lee, Y. Wang and Y. Zhang Consider the following access control requirements for patient records. (1) Record administrators can delegate any rights associated with records. (2) Hospital managers are allowed to delegate any right associated with records to doctors. (3) Patients cannot modify records. (4) Patients cannot read records during non-business hours. (5) Doctors cannot modify records during non-business hours. (6) Doctors are allowed to read or modify records during business hours. (7) Doctors may allow patients to read their records during business hours. Figure 1 shows the policy hierarchy of this example. Policy p1 expresses requirement (1) above. It is trusted with the maximum delegation depth 2, meaning that a delegation chain start- ing from p1 should be aborted if it goes through more than 2 policies or policy sets. Policy set ps1 is trusted and has the first-applicable policy-combining algorithm. Policies p2, p3, p4 are children policies of ps1, describing requirements (3), (4), and (5) above, respec- tively. Policy set ps2 is issued by record admin, again having the policy-combining algo- rithm first-applicable. Policies p5, p6 and p7 are children of ps2, describing (6), (7) and (2) respectively. 2.3 Semantics The semantics of XACML 3.0 describes how to make a decision on a request based on the policy description. A decision is any one of the following values: permit (p), deny (d), indeterminateP (ip ), indeterminateD (id ), indeterminateDP (idp ), and notApplicable (na). A decision is applicable if it is not na. Given an access request consisting of certain attributes, a rule evaluates to a single decision. A policy combines the decisions from its children rules to a single decision according to its rule combining algorithm. Similarly, a policy set combines the decisions from its children policies/policy sets into a single decision according to its policy combining algo- rithm. At the top level, the PDP returns a single decision as if it had evaluated a single policy set consisting of the set of all top level policies/policy sets. Below, for each element E, we formally define the function evalE (e, Rq) that maps to a value the specific instance of E denoted by e and the request Rq. 2.3.1 Evaluation of Rules In order to determine a rule’s decision, its target needs to be evaluated first, whose value is either match (m), no match (nm) or indeterminate (i). In XACML 3.0, a target is a Boolean combination of matchs using allOf s (conjunctions) and anyOf s (disjunctions). Due to lack of space, we skip the details of evaluation of Target and its descendants. Given a rule R = hTarget, eff , condi and a request Rq,  eff  if evalT arget (Target, Rq) = m and cond is true evalRule (R, Rq) = na if evalT arget (T arget, Rq) = nm or cond is false (1)  ieff otherwise.  2.3.2 Evaluation of Policies Given a policy P = hT, hR1 , . . . , Rn i, alg, Issuer, maxDelDepi, and a request Rq, we define combDec(P, Rq) = alg(DECP ), where DECP is the list of decisions hevalRule (R1 , Rq), . . . , evalRule (Rn , Rq)i, and alg denotes one of the combining algorithms specifying how the chil- dren rules’ decisions are combined. Combining algorithms in XACML 3.0 are more refined than those in XACML 2.0, but since they are not new, we skip the details. Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming 5 The evaluation of a policy P against a request Rq is defined as:  combDec(P, Rq) if evalT arget (T, Rq) = m   if evalT arget (T, Rq) = nm  na   evalP olicy (P, Rq) = na if evalT arget (T, Rq) = i and combDec(P, Rq) = na  i if evalT arget (T, Rq) = i and combDec(P, Rq) = e (e ∈ {p, d})     e  ie if evalT arget (T, Rq) = i and combDec(P, Rq) = ie (e ∈ {p, d, dp})  (2) The value of this function is discarded if the policy is not trusted. The next section explains how trust can be established. 2.3.3 The Reduction Process A policy/policy set is said to be trusted if it does not have an issuer (or its issuer is null); otherwise it is said to be untrusted. Any applicable decision from an untrusted policy/policy set should go through a process called reduction to get authorized before they are combined into their parent policy set’s decision. The reduction process is essentially a graph search to find a path from the untrusted policy/policy set whose decision is being reduced to a trusted policy/policy set. In XACML 3.0, a policy/policy set concerning delegation is called an administrative pol- icy/policy set. In these policy/policy set, attributes of the accesses that are allowed to be dele- gated have categories prefixed by “delegated:”, and a special category called “delegate” is used to specify the attributes of the delegate. The approach that XACML 3.0 uses to check if a decision of one policy/policy set PL is authorized by another policy/policy set PH, given the context of a request Rq, is to generate a special request called administrative request based on the content of Rq, a candidate decision (p or d), and the issuer of PL, and then check, using the same evaluation for access requests, if PH evaluates to permit or deny upon this administrative request. Intuitively, an administrative request is a request asking whether an issuer can authorize an access. This process is formally defined as follows.  administrative requests: Given a policy/policy set P , a request Rq, and a de- 1) Generating cision e ∈ p, d, id , ip , idp to be reduced, the administrative request ARP,Rq,d is constructed. Roughly speaking, the content is similar to the request Rq except that the categories of attributes in the original access request are prefixed with “delegated:” and the policy issuer of P be- comes the attribute of the administrative request with category “delegate.” 2) Constructing the reduction graph: In a policy set, once the administrative request w.r.t. a request for each child policy/policy set is constructed, the authorization relations between chil- dren policies/policy sets can be calculated by evaluating each administrative request against each policy/policy set. Based on the authorization relations, the reduction graph can be constructed. We write evalP (·, ·) to denote either evalP olicy (·, ·) or evalP olicySet (·, ·). Given a policy set PS and a request Rq, the reduction graph RGP S,Rq is defined as follows. • The nodes of RGP S,Rq are the immediate children policies and policy sets of PS. • There are 4 types of directed edges in the graph: PP, PI, DP and DI. For each or- dered pair (P1 , P2 ) of policies/policy sets in PS, from P1 to P2 , (i) there is a PP edge if evalP (P2 , ARP1 ,Rq,p ) = p; (ii) there is a PI edge if evalP (P2 , ARP1 ,Rq,p ) = id /ip /idp ; (iii) there is a DP edge if evalP (P2 , ARP1 ,Rq,d ) = p; (iv) there is a DI edge if evalP (P2 , ARP1 ,Rq,d ) = id /ip /idp ; In the graph, we say that a path is a (i) PP path if it consists of PP edges only; (ii) PI path if 6 J. Lee, Y. Wang and Y. Zhang it consists of PP and PI edges only; (iii) DP path if it consists of DP edges only; (iv) DI path if it consists of DP and DI edges only. 3) Reduction of policies: Let P be a policy or a policy set and PS be the parent policy set of P . We say that P is PP-authorized (DP-authorized / PI-authorized / DI-authorized, respectively) if there is a PP (DP / PI / DI, respectively) path of length ≤ maxDelDep from P to a trusted policy or policy set in RGP S,Rq , where maxDelDep is the maximum delegation depth of the trusted policy or policy set. We define the operator reduce(P, Rq) that maps a policy/policy set P to a decision or null, w.r.t. a request as follows.  evalP (P, Rq) if P is trusted   p if P is untrusted, evalP (P, Rq) = p and P is PP-authorized         d if P is untrusted, evalP (P, Rq) = d and P is DP-authorized  i p if P is untrusted, evalP (P, Rq) = p and P is PI-authorized reduce(P, Rq) = id   if P is untrusted, evalP (P, Rq) = d and P is DI-authorized    ie if P is untrusted, evalP (P, Rq) = ie and P is PP-authorized or  DP-authorized or PI-authorized or DI-authorized (e ∈ {p, d, dp})      null otherwise.  (3) Note that there is a mutual recursion between reduce(P, Rq) and evalP (P, Rq) (See Figure 3 for an example run). 2.3.4 Evaluation of Policy Sets Policy set evaluation is similar to Policy evaluation. The only difference is that the decisions from a policy set’s children policies/policy sets need to go through the reduction process before being combined, possibly being disregarded if the reduction process determines that they are not trusted. Given a policy set P S = hT, hP1 , . . . , Pn i, alg, Issuer, maxDelDepi, and a request Rq, define combDec(P S, Rq) = alg(DECP S ), where DECP S is the sequence of decisions obtained by removing all null elements from hreduce(P1 , Rq), . . . , reduce(Pn , Rq)i. Other than this, evalP olicySet (P S, Rq) is defined in the same way as evalP olicy (P S, Rq). According to (OASIS 2013), the PDP is evaluated as a policy set with the policy-combining algorithm specified in the PDP and all the top level policies and/or policy sets as its children. Given the PDP defined as hcombAlg, hP1 , . . . , Pn ii where each Pi is a top level policy or pol- icy set, the final decision of the PDP on a request Rq is defined by evalP DP (pdp, Rq) = evalP olicySet (ps0 , Rq) where ps0 is the policy set h∅, hP1 , . . . , Pn i, combAlg, null, inf i 2.3.5 Example of Evaluation Consider the policy hierarchy in Example 1 and the access request rq by a doctor who wants to mod- PP, DP p1 ps2 ify a record during business hours. According to the PP, DP p5 p7 evaluation semantics, all the children policies of ps1 ps1 are trusted. So none of them are disregarded. As p6 all of them return notApplicable to rq, we have RGPS2,rq RGPDP,rq evalP olicySet (ps1 , rq) = na. Fig. 2: Reduction graph RGps2,rq and RGPDP,rq Although p5 returns permit, p5 is untrusted, so the decision of p5 needs to go through the reduction process. The reduction graph RGps2,rq has three nodes, p5 , p6 , and p7 . The administrative request arp5 ,rq,p is generated. Evaluating arp5 ,rq,p Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming 7 Evaluate rq against PDP Reduce decision from ps2 Combine Generate admin. req. arp1/ps1/ps2, rq, p/d Reduce decision Reduce decision Reduce decision from p1 from ps1 from ps2 Evaluate ar against ps1 Evaluate ar against p1 Evaluate ar against ps2 Evaluate rq Evaluate rq Evaluate rq against p1 against ps1 Combine against ps2 Combine Combine …... Reduce decision Reduce decision Reduce decision from p5 from p6 from p7 Reduce decision Reduce decision Reduce decision Reduce decision Reduce decision Reduce decision from p2 from p3 from p4 from p5 from p6 from p7 Evaluate ar Evaluate ar Evaluate ar Evaluate rq Evaluate rq Evaluate rq Evaluate rq Evaluate rq Evaluate rq against p5 against p6 against p7 against p2 against p3 against p4 against p5 against p6 against p7 Fig. 3: Top-down procedure illustration: The tree structure on the left shows how PDP evaluation boils down to policy evaluations, where arrows denote subroutine calls. against p6 and p7 yields evalP olicy (p7 , arp5 ,rq,p ) = p, evalP olicy (p6 , arp5 ,rq,p ) = na, so there is a PP edge from p5 to p7 in the reduction graph RGps2 ,rq (Figure 2). Since p7 is trusted and there is a PP path from p5 to p7 , the decision of p5 is authorized and is combined as permit. Since the permit returned by p5 is the first applicable decision from ps2 ’s children policies, we have evalP olicySet (ps2 , rq) = p. However, again ps2 is untrusted, so the decision of ps2 needs to go through the reduction pro- cess. The reduction graph RGpdp,rq (Figure 2) has three nodes, p1 , ps1 and ps2 . The new admin- istrative request arps2 ,rq,p has almost the same content as arp5 ,rq,p except that the delegate category is filled with “record admin” instead of “hospital manager”. Evaluating arps2 ,rq,p against p1 and ps1 , we have evalP olicy (p1 , arps2 ,rq,p ) = p. So there is a PP edge from ps2 to p1 . As p1 is trusted and there is a PP path from ps2 to p1 , reduce(ps2 , rq) results in p. Since in this example the PDP’s combining algorithm is deny-unless-permit, the final decision is permit: evalP DP (pdp, rq) = p. Figure 3 shows the overall evaluation procedure. 3 Implementing XACML 3.0 in ASP In this section, we show how to construct an ASP program such that, given the ASP representa- tion of policy description and a request, its answer set corresponds to the PDP’s response to this request. The basic idea is to represent the evaluation function that we constructed in the previous section by ASP rules. Due to lack of space, we refer the reader to http://reasoning.eas.asu.edu/xacml2asp for the complete formalization of XACML 3.0 elements in ASP. 3.1 Representing XACML policy and requests as ASP facts We first show how to represent each of XACML 3.0 elements as ASP facts. Given a policy document, we assign a unique identifier (mostly an integer), denoted by Id(E), to each element. • A policy set PS = hTarget, hP1 , . . . , Pn i, combAlg, Issuer, maxDelDepi is represented as policySet(Id(PS), Id(Target), combAlg, Id(Issuer), maxDelDep). hasChild(Id(PS), Id(Pi ), i). (1 ≤ i ≤ n) • A policy P = hTarget, hR1 , . . . , Rn i, combAlg, Issuer, maxDelDepi is represented in a similar way except that its children are rules. • A rule R = hTarget, effect, conditioni is represented as rule(Id(R), Id(Target), effect, Id(condition)). • A target T = {AnyOf 1 , . . . , AnyOf n } is represented as hasAnyOf(Id(T ), Id(AnyOf i )). (1 ≤ i ≤ n) 8 J. Lee, Y. Wang and Y. Zhang An anyOf A = {AllOf 1 , . . . , AllOf n } and an allOf A = {M1 , . . . , Mn } are represented in a similar way. • A match M = hmF unc, AR, hdataType, valueii where AR = hhattrID, category, issueri, mbpi, is represented as the set of facts attrRetriever(Id(AR),AttrID, category, issuer, mbp). match(Id(M ), mFunc, Id(AR), dataType, attrVal). • An issuer I = {Attr1 , . . . , Attrn }, where each Attri is hhattrIDi , cati , attrIssueri i, htypei , vali ii, is represented as hasAttr(Id(I), attrIDi , cati , atIssueri , typei , vali ). (1 ≤ i ≤ n) • The PDP is translated as a special policy set. PDP = hhP1 , . . . , Pn i, combAlgi is repre- sented as policySet(pdp, empty target, combAlg, null, inf). hasChild(pdp, Id(Pi ), i). (1 ≤ i ≤ n) A request Rq = {Attr1 , . . . , Attrn } is represented in the same way as an issuer. 3.2 Reasoning about PDP Decision by ASP In this section, we show how to represent the evaluation semantics discussed in Section 2.3 in ASP rules. The representation is modular and turns each of the formal definitions in that section into ASP rules (to be precise, in the input language of F 2 LP (Lee and Palla 2009)).2 We use atom evaluate(e, Rq, V) to represent the mapping from an element to a value, evalE (e, Rq) = V . 3.2.1 Representing Rule Evaluation We represent the evaluation of rule described in (1) as follows. evaluate(R, Rq, Effect) <- rule(R, T, Effect, Condition) & evaluate(T, Rq, m) & evaluate(Condition, Rq, t). evaluate(R, Rq, na) <- rule(R, T, Effect, Condition) & (evaluate(T, Rq, nm) | evaluate(Condition, Rq, f)). evaluate(R, Rq, i(Effect)) <- rule(R, _, Effect, _) & request(Rq, _, _, _, _, _) & not evaluate(R, Rq, Effect) & not evaluate(R, Rq, na). 3.2.2 Representing Combining Algorithms We use atom reduce(Id(P ), Id(Rq), Dec) to represent the reduction operator reduce(P, Rq) = Dec in Section 2.3.3. Given a policy or a policy set P , we use atom combined decision(Id(P ), Id(Rq), Dec) to represent combDec(P, Rq) = Dec. We also add the following rule to simplify the represen- tation. combining_algo(P, Alg) <- (policy(P, _, Alg, _, _) | policySet(P, _, Alg, _, _). The actual evaluation of combDec(P, Rq) depends on the specific combining algorithm alg that P has. 3.2.3 Evaluating policy and policy set The evaluation of policy described in (2) can be represented by the following ASP rules, each of which describes each case in (2). 2 The use of F 2 LP language is not essential, but it is often more concise than the CLINGO language. Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming 9 evaluate(P, Rq, Dec) <- policy(P, T, _, _, _) & evaluate(T, Rq, m) & combined_decision(P, Rq, Dec). evaluate(P, Rq, na) <- policy(P, T, _, _, _) & evaluate(T, Rq, nm). evaluate(P, Rq, na) <- policy(P, T, _, _, _) & evaluate(T, Rq, i) & combined_decision(P, Rq, na). evaluate(P, Rq, i(Dec)) <- policy(P, T, _, _, _) & evaluate(T, Rq, i) & combined_decision(P, Rq, Dec) & (Dec=p | Dec=d). evaluate(P, Rq, i(Dec)) <- policy(P, T, _, _, _) & evaluate(T, Rq, i) & combined_decision(P, Rq, i(Dec)) & (Dec=p | Dec=d | Dec=dp). The evaluation of policy set is very similar to the evaluation of policy. 3.2.4 Representing the Reduction Process The reduction process discussed in Section 2.3.3 can be represented in ASP as follows. Generating administrative requests: Given a policy or policy set P , a request Rq, and a deci- sion Dec, we use the atom ar(Id(P ), Id(Rq), Dec) to denote ARP,Rq,Dec . The following ASP rule maps an attribute in Rq with a delegated category to an identical attribute in ARP,Rq,Dec . request(ar(P, Rq, Dec), AttrID, Cat, AttrIssuer, Type, AttrVal) <- to_evaluate_against(Rq, PS) & policySet(PS, _, _, _, _) & hasChild(PS, P, _) & request(Rq, AttrID, Cat, AttrIssuer, Type, AttrVal) & @isDelegatedPrefixed(Cat) == 1 & (Dec = d | Dec = p). to evaluate against(Rq,PS) is defined to be true if the evaluation of Rq against policy set PS needs to invoke the reduction process. The term @isDelegatedPrefixed(Cat) is an external LUA function call that returns 1 if Cat is prefixed by “delegated:”, 0 otherwise. The following ASP rule maps an attribute in Rq whose category is not prefixed by “delegated” and is different from “delegationInfo” and “delegate” to an identical attribute prefixed by “delegated:”. request(ar(P, Rq, Dec), AttrID, @addDelegatedPrefix(Cat), AttrIssuer,Type, AttrVal) <- to_evaluate_against(Rq, PS) & policySet(PS, _, _, _, _) & hasChild(PS, P, _) & request(Rq, AttrID, Cat, AttrIssuer, Type, AttrVal) & @equalsDelegationInfo(Cat) == 0 & @equalsDelegate(Cat) == 0 & @isDelegatedPrefixed(Cat) == 0 & (Dec = d | Dec = p). (The term @addDelegatedPrefix(Cat) is an external LUA function call that returns Cat prefixed by “delegated:”. @equalsDelegationInfo(Cat) is a LUA function call that returns 1 if Cat is the string delegation-info and 0 otherwise; @equalsDelegate(Cat) is the LUA function call that returns 1 if Cat is the string delegate, and 0 otherwise.) Similarly, we copy every attribute of P ’s issuer to an identical attribute with the category delegate to the administrative request, as well as decision-info. Constructing the reduction graph: Given a request Rq and a policy set P S, we use the atom path(Id(Rq), Id(PL), Id(PH), Type, Length) for the reduction graph RGP S,Rq , which is true if and only if there is a path of type Type and length Length from PL to PH in RGP S,Rq , where P S is the parent policy set of PL and PH. The following ASP rules define PP and PI edges in the reduction graph. path(Rq, PL, PH, pp, 1) <- evaluate(PH, ar(PL, Rq, p), p) & policySet(PS, _, _, _, _) & PH != PL & hasChild(PS, PH, _) & hasChild(PS, PL, _). indeterminate(i(Dec)) <- Dec = p | Dec = d | Dec = dp. path(Rq, PL, PH, pi, 1) <- evaluate(PH, ar(PL, Rq, p), Dec) & policySet(PS, _, _, _, _) & PH != PL & hasChild(PS, PH, _) & hasChild(PS, PL, _) & indeterminate(Dec). DP and DI edges are defined similarly. Based on the definition of edges (paths of length 1), we recursively define paths of arbitrary lengths in the reduction graph. 10 J. Lee, Y. Wang and Y. Zhang path(Rq, PL, PH, Type, L) <- path(Rq, PL, PM, Type, L1) & path(Rq, PM, PH, Type, L2) & L = L1 + L2. path(Rq, PL, PH, pi, L) <- path(Rq, PL, PM, T1, L1) & path(Rq, PM, PH, T2, L2) & ((T1 == pp & T2 == pi) | (T1 == pi & T2 == pp)) & L = L1 + L2. path(Rq, PL, PH, di, L) <- path(Rq, PL, PM, T1, L1) & path(Rq, PM, PH, T2, L2) & ((T1 == dp & T2 == di) | (T1 == di & T2 == dp)) & L = L1 + L2. Reduction of policies: First we define the notion of trusted and untrusted policies/policy sets as follows. trusted(P) <- (policy(P, _, _, Issuer, _) | policySet(P, _, _, Issuer, _)) & Issuer == null. untrusted(P) <- (policy(P, _, _, Issuer, _) | policySet(P, _, _, Issuer, _)) & not trusted(P). Then we define the authorization property of a policy/policy set w.r.t. a request. pp_authorized(Rq, P) <- path(Rq, P, TP, pp, L) & trusted(TP) & (policy(TP, _, _, _, Dep) | policySet(TP, _, _, _, Dep)) & L <= Dep. pi authorized, dp authorized, di authorized are defined in a similar way. Based on the above definitions, (3) can be represented as reduce(P, Rq, Dec) <- evaluate(P, Rq, Dec) & trusted(P). reduce(P, Rq, p) <- untrusted(P) & evaluate(P, Rq, p) & pp_authorized(Rq, P). reduce(P, Rq, d) <- untrusted(P) & evaluate(P, Rq, d) & dp_authorized(Rq, P). reduce(P, Rq, i(p)) <- untrusted(P) & evaluate(P, Rq, p) & pi_authorized(Rq, P). reduce(P, Rq, i(d)) <- untrusted(P) & evaluate(P, Rq, d) & di_authorized(Rq, P). reduce(P, Rq, i(Dec)) <- untrusted(P) & evaluate(P, Rq, i(Dec)) & (pp_authorized(Rq, P) | pi_authorized(Rq, P) | dp_authorized(Rq, P) | di_authorized(Rq, P)). The final decision is determined by evaluating the access request rq against the policy set PDP. final_decision(Dec) <- evaluate(pdp, rq, Dec). 3.3 XACML Delegation Analysis using ASP Once we turn XACML into ASP that has formal executable semantics, we can apply formal reasoning techniques in ASP to analyze XACML policies. 3.3.1 Delegation-Based Decision on Access Requests Given a set of ASP facts describing a policy hierarchy, we can simulate the PDP to make the decision on a certain request, by finding the answer sets of Π ∪ Πpolicy ∪ Πrequest , where Π is the PDP simulating program constructed in Section 3.2, Πpolicy is the given policy description constructed in Section 3.1, and Πrequest is the ASP facts representing the request. For example, in Example 1, we can check if the given policy permits the request by a doctor who wants to modify a record during the business hours. The program Πrequest is request(rq, "group", "subject", null, "string", "doctor"). request(rq, "group", "resource", null, "string", "record"). request(rq, "action-id", "action", null, "string", "modify"). request(rq, "is-business-hour", "environment", null, "string", "true"). The answer set of Π ∪ Πpolicy ∪ Πrequest contains path(rq,p5,p7,dp,1) path(rq,p5,p7,pp,1) path(rq,ps2,p1,dp,1) path(rq,ps2,p1,pp,1) final_decision(p) which is in accordance with the evaluation discussed in the example in Section 2.3.5. 3.3.2 Analysis of Possible Delegation In (Ahn et al. 2010) the authors showed how to verify a security property against a given policy description. As XACML 3.0 has introduced the delegation feature, where everyone can write Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming 11 policies, security leakages can be caused not only by a malicious request context, but also by an unforeseen delegation chain. Here we assume that new (untrusted) policies can be added, and check whether this may lead to a breach. We define several additional programs. Program Πquery represents the negation of the security property to check, and program Πdomain defines the domain of attributes. We use Πreq conf ig to denote the program that generates arbitrary access request given the domain defined in Πdomain . Finally, we use Πnpolicy conf ig to denote the program that generates 0 ∼ n arbitrary untrusted policies (which are to be set as the children of PDP). The generated policies have empty targets, so they are applicable to any access request. The contents of these programs are specific to particular domains and queries. The problem of checking whether a security property holds, assuming that new (untrusted) policies can be added, can be considered as the problem of checking whether the program Π ∪ Πpolicy ∪ Πdomain ∪ Πrequest conf ig ∪ Πnpolicy conf ig ∪ Πquery has no answer sets. If the program being checked is unsatisfiable, we can conclude that the security property specified by Πquery holds w.r.t. the attribute domain and the maximum number n of policies that can be added. Otherwise the answer sets returned provide counterexamples showing why the security property does not hold. In other words, the checking ensures that Π ∪ Πpolicy ∪ Πdomain ∪ Πrequest conf ig ∪ Πnpolicy conf ig entails the property being checked. Consider the policy in Example 1. For this example, Πdomain is the following set of facts. subject_group("record_admin"). subject_group("doctor"). subject_group("patient"). subject_group("hospital_manager"). resource_group("record"). action_id("read"). action_id("modify"). boolean_string("true"). boolean_string("false"). Πrequest conf ig is the following program % generate arbitrary access request 1 {request(rq, "group", "subject", null, "string", Val): subject_group(Val)}. 1 {request(rq, "group", "resource", null, "string", Val): resource_group(Val)}. 1 {request(rq, "action-id", "action", null, "string", Val): action_id(Val)}. 1 {request(rq, "is-business-hour", "environment", null,"string", Val): boolean_string(Val)} 1. and Πnpolicy conf ig where n = 6 (since any delegation chain has length less than 6) is the follow- ing program % for each policy set, generate 0 ˜ max_num_policy arbitrary policies valid_policy_number(1..6). {policy(policy_gen(NUM), empty_target, fa, issuer(NUM), #supremum) : valid_policy_number(NUM)} max_num_policy. hasChild(pdp, policy_gen(NUM), NUM + 3) <- valid_policy_number(NUM). hasChild(policy_gen(NUM), r(DEC), 1) <- valid_policy_number(NUM) & dec_queried(DEC). rule(r(permit), empty_target, p, null). rule(r(deny), empty_target, d, null). % generate arbitrary subject attributes for issuer of each policy 1 {hasAttr(issuer(NUM), "group", "subject", null,"string", Val): subject_group(Val)} <- policy(policy_gen(NUM), _, _, issuer(NUM), _). Suppose we are checking whether patients can modify the records in any case. The query is written as dec_queried(permit). request(rq, "group", "subject", null, "string", "patient"). request(rq, "group", "resource", null, "string", "record"). request(rq, "action-id", "action", null, "string", "modify"). <- not final_decision(p). For the program Π ∪ Πpolicy ∪ Πdomain ∪ Πrequest conf ig ∪ Π6policy conf ig ∪ Πquery , the ASP 12 J. Lee, Y. Wang and Y. Zhang solver returns an answer set that suggests that even when no new policy is added, if the patient is at the same time a doctor, then he would be allowed to modify a record. For the policy designer, this means he must decide whether it should be allowed for a patient to be a doctor at the same time. This is an instance of the problem known as “separation of duty.” Suppose he decides not to allow such a case. Even with prohibiting such instances, RGpdp, rq RG pdp, rq the answer set found suggests that if a p1 PP, DP ps2 p1 PP, DP ps2 record admin writes a policy to allow a pa- PP, DP PP, DP tient to modify a record, the patient would ps1 ps1 gen(1) PP, DP have access to the record. This is because the Deny Deny Permit PDP is set to have the combining algorithm Patient wants to modify the record Patient wants to modify the record deny-unless-permit. So even if p2 denies this Before policy_gen(1) is added After policy_gen(1) is added Fig. 4: The reduction graph before and after the generated policy is access, causing ps1 to deny this access, the added permit decision of the newly generated pol- icy (policy gen(1)) (which can be authorized by p1) overrides the deny decision. Figure 4 shows how the generated policy policy gen(1) affects the original reduction graph. So the system designer must consider, whether a record admin’s permission can defeat the constraint that a patient cannot modify the record. Suppose he decides not to allow this situation. To make sure a patient cannot modify the record even when he has permission from a record admin, we change the combining algorithm of the PDP to first-applicable, making the decision of ps1 to override the decision of any newly-written policy. After making this change, the solver returns no answer set, suggesting that there is no way for a patient to modify the record. To evaluate the effectiveness of our analysis ap- proach, we implemented in Java the translation of XACML into ASP (http://reasoning.eas. asu.edu/xacml2asp). The software XACML 2 ASP turns a policy description in XACML in the language of F 2 LP and then calls F 2 LP (v1.3) to turn it into the in- put language of ASP solver CLINGO (v3.0.5). Figure 5 Fig. 5: Experiments shows experiments with a few examples.3 The exper- iment was performed on an Intel Core2 Duo CPU E7600 3.06GH with 4GB RAM running Ubuntu 13.10. For each example, we arbitrarily constructed a partially defined access request and check whether the request can be granted in some case. 4 Conclusion The previous version of XACML was represented in several formal languages, such as answer set programs (Ahn et al. 2010), first-order logic (Hughes and Bultan 2004), a process alge- bra (Bryans 2005), MTBDDs (Fisler et al. 2005), Description Logics (Kolovski et al. 2007), and automated reasoning was performed by leveraging the reasoners available for these formal languages. In comparison with (Ahn et al. 2010), due to the coverage of delegation, our work is unavoid- ably more sophisticated. The formal semantics of ASP, being able to represent reachability and nonmonotonicity unlike other formal languages, provides a natural basis for formalizing delega- tion in XACML 3.0. 3 Since XACML 3.0 delegation model has not been widely applied yet, not many examples are available. Automated Reasoning about XACML 3.0 Delegation Using Answer Set Programming 13 Acknowledgements We are grateful to Michael Bartholomew, Amelia Harrison, and the anony- mous referees for their useful comments. This work was partially supported by the National Sci- ence Foundation under Grant IIS-1319794, South Korea IT R&D program MKE/KIAT 2010- TD-300404-001, and ICT R&D program of MSIP/IITP 10044494 (WiseKB). References A HN , G.-J., H U , H., L EE , J., AND M ENG , Y. 2010. Representing and reasoning about web access control policies. In Proc. 34th Annual IEEE Computer Software and Applications Conference (COMPSAC 2010). 137–146. B RYANS , J. 2005. Reasoning about XACML policies using CSP. In Proceedings of the 2005 workshop on Secure web services. ACM, 35. F ISLER , K., K RISHNAMURTHI , S., M EYEROVICH , L., AND T SCHANTZ , M. 2005. Verification and change-impact analysis of access-control policies. In Proceedings of the 27th international conference on Software engineering. ACM New York, NY, USA, 196–205. H UGHES , G. AND B ULTAN , T. 2004. Automated verification of access control policies. Computer Science Department, University of California, Santa Barbara, CA. KOLOVSKI , V., H ENDLER , J., AND PARSIA , B. 2007. Analyzing web access control policies. In WWW ’07: Proceedings of the 16th international conference on World Wide Web. ACM, New York, NY, USA, 677–686. L EE , J. AND PALLA , R. 2009. System F 2 LP – computing answer sets of first-order formulas. In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 515–521. OASIS. 2013. OASIS eXtensible Access Control Markup Language (XACML) V3.0. http://www.oasis- open.org/committees/xacml/.