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.
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, standardized by the Organization for the Advancement of Structured Information Standards (OASIS). The latest version, XACML 3.0, was standardized in 2013, and is significantly more enhanced and expressive than the previous version by introducing several new features, such as multiple decision profile, delegation, obligation/advice expressions, and more enhanced combining 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 previous 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 reducing 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.
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
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 humanfriendly, 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 semantics 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
2 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.
XACML is mainly an Attribute Based Access Control system (ABAC), in which attributes associated 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.
PDP PolicySet Policy Rule Target AnyOf AllOf
Match AttrIdentifier
AttrVal AttrRetriever hh(PolicyjPolicySet)*i; combAlgi hTarget; h(PolicyjPolicySet)+i;
combAlg; Issuer; maxDelDepi hTarget; hRule+i; combAlg; Issuer;
maxDelDepi fAnyOf g fAllOf +g fMatch+g hTarget; effect; conditioni hmFunc; AttrRetriever; AttrVali hattrID; category; attrIssueri hdataType; valuei hAttrIdentifier; mustBePresenti
Issuer
Request maxDelDep combAlg attrID attrIssuer dataType value effect condition mFunc category mustBePresent a string a string fhAttrIdentifier; AttrVali*g fhAttrIdentifier; AttrVali+g a nonnegative integer or inf (1) po j do j pud j dup j fa j ooa j ... string j integer j date j... a value of the corresponding data-type permit j deny a boolean function call a boolean function true j false subject j resource j action j ... 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.
ps1 Issuer: trusted CombAlg: first-applicable Target: any p2 Issuer: trusted Target: Subject: patient Resource: record Action: modify RuleEffect: deny Example 1
Access request pdp deny-unless-permit p1 Issuer: trusted Target: Delegate: record_admin DelegatedResource: record RuleEffect: permit MaxDep: 2 ps2 Issuer: record_admin CombAlg: first-applicable Target: any MaxDep: 5 p3 Issuer: trusted Target: Subject: patient Resource: record Action: read IsBusinessHour: false RuleEffect: deny p4 Issuer: trusted Target: Subject: doctor Resource: record Action: modify IsBusinessHour: false RuleEffect: deny
p6 p5 Issuer: trusted Issuer: hospital_manager Target: Target: Delegate: doctor Subject: doctor DelegatedSubject: patient Resource: record DelegatedResource: record Action: modify/read DelegatedAction: read IsBusinessHour: true DelegatedIsBusinessHour:true RuleEffect: permit RuleEffect: permit
MaxDep: 5 Fig. 1: Policy Hierarchy of Example 1 p7 Issuer: trusted Target: Delegate: hospital_manager DelegatedSubject: doctor DelegatedResource: record DlegatedAction: modify/read RuleEffect: permit MaxDep:3
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. 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 algorithm. 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,
8>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 >:ieff otherwise: (1) 2.3.2 Evaluation of Policies Given a policy P = hT; hR1; : : : ; Rni; 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 children 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. The evaluation of a policy P against a request Rq is defined as: 8>combDec(P; Rq) if evalT arget(T; Rq) = m > >>>>na if evalT arget(T; Rq) = nm evalP olicy(P; Rq) = <na if evalT arget(T; Rq) = i and combDec(P; Rq) = na >>>>ie if evalT arget(T; Rq) = i and combDec(P; Rq) = e (e 2 fp; dg) >:>ie if evalT arget(T; Rq) = i and combDec(P; Rq) = ie (e 2 fp; d; dpg) (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 policy/policy set. In these policy/policy set, attributes of the accesses that are allowed to be delegated 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. 1) Generating administrative requests: Given a policy/policy set P , a request Rq, and a decision e 2 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 becomes 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 children 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 ordered 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 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.
8>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 reduce(P; Rq) = ><>ip if P is untrusted, evalP (P; Rq) = p and P is PI-authorized >>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 2 fp; d; dpg) >>: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; : : : ; Pni; 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
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 Reduce decision from p1 Evaluate rq against p1
Evaluate rq against PDP
Combine Reduce decision from ps1 Evaluate rq against ps1
Combine
Reduce decision from ps2 Evaluate rq against ps2
Combine
Evaluate ar against ps1 …. .
Reduce decision from ps2
Generate admin. req. arp1/ps1/ps2, rq, p/d Evaluate ar against p1 Evaluate ar against ps2
Combine Reduce decision from p5
Redufrcoemdepc6ision Redufrcoemdepc7ision Evaluate ar against p5
Evaluate ar against p6
Evaluate ar against p7 Redufrcoemdepc2ision Redufrcoemdepc3ision Redufrcoemdepc4ision Redufrcoemdepc5ision Redufrcoemdepc6ision Redufrcoemdepc7ision
Eavgaaliunasttepr2q Eavgaaliunasttepr3q Eagvaailnusattepr4q Eavgaaliunasttepr5q Eavgaaliunasttepr6q Eavgaaliunasttepr7q 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 process. The reduction graph RGpdp;rq (Figure 2) has three nodes, p1, ps1 and ps2. The new administrative 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.
In this section, we show how to construct an ASP program such that, given the ASP representation 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.
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; : : : ; Pni; 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; : : : ; Rni; 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 = fAnyOf 1; : : : ; AnyOf ng is represented as
hasAnyOf(Id(T ); Id(AnyOf i)). (1 i n) An anyOf A = fAllOf 1; : : : ; AllOf ng and an allOf A = fM1; : : : ; Mng 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 = fAttr1; : : : ; Attrng, where each Attri is hhattrIDi; cati; attrIssuerii; htypei; valiii, 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; : : : ; Pni; combAlgi is represented as policySet(pdp, empty target, combAlg, null, inf).
hasChild(pdp, Id(Pi), i). (1 i n) A request Rq = fAttr1; : : : ; Attrng is represented in the same way as an issuer.
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 F2LP
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 representation. 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 F2LP language is not essential, but it is often more concise than the CLINGO language.
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 decision 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. 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.
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. 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
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 the PDP simulating program constructed in Section 3.2, [ policy [ policy is the given policy description request, where is 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 [ which is in accordance with the evaluation discussed in the example in Section 2.3.5.
3.3.2 Analysis of Possible Delegation
In
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 config to denote the program that generates arbitrary access request given the domain defined in domain.
Finally, we use n policy config 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 [ 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 config [ Consider the policy in Example 1. For this example, domain is the following set of facts. n policy config entails the property being checked. 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 config 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 n policy config where n = 6 (since any delegation chain has length less than 6) is the following 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 6 [ policy [ domain [ request config [ policy config [ query, the ASP 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.
PP, DP ps2
RGpdp,rq p1 ps1
PP, DP PP, DP
PP, DP ps2
PP, DP gen(1)
Even with prohibiting such instances, the answer set found suggests that if a record admin writes a policy to allow a patient to modify a record, the patient would have access to the record. This is because the PDP is set to have the combining algorithm deny-unless-permit. So even if p2 denies this
Deny Deny Permit Patient wants to modify the record Patient wants to modify the record
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 policy (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 approach, we implemented in Java the translation of XACML into ASP (http://reasoning.eas. asu.edu/xacml2asp). The software XACML2ASP turns a policy description in XACML in the language of F2LP and then calls F2LP (v1.3) to turn it into the input language of ASP solver CLINGO (v3.0.5). Figure 5 shows experiments with a few examples.3 The exper- Fig. 5: Experiments 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.
The previous version of XACML was represented in several formal languages, such as answer
set programs
In comparison with