=Paper=
{{Paper
|id=Vol-1433/tc_78
|storemode=property
|title=Automated Reasoning about XACML 3.0 Delegation
Using Answer Set Programming
|pdfUrl=https://ceur-ws.org/Vol-1433/tc_78.pdf
|volume=Vol-1433
|dblpUrl=https://dblp.org/rec/conf/iclp/LeeWZ15
}}
==Automated Reasoning about XACML 3.0 Delegation
Using Answer Set Programming==
https://ceur-ws.org/Vol-1433/tc_78.pdf
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/.