Anh Truong
email: anhtt@hcmut.edu.vn

Hai Ton Dai

That

Solving the User-role Reachability Problem in ARBAC with Role Hierarchy

Access Control is becoming increasingly important for today's ubiquitous systems since it provides mechanism to prevent sensitive resources in the systems against unauthorized users. In access control models, the administration of access control policies is an important task that raises a crucial analysis problem: if a set of administrators can give a user an unauthorized access permission. We consider the analysis problem in the context of the Administrative Role-Based Access Control (ARBAC), the most widespread administrative model. One of the main assumptions of current analysis techniques is that the role hierarchy is constant and thus can be abstracted away that results in the bad scalability of analysis techniques. In this paper, we introduce three reductions to enable an available analysis technique, namely ASASPXL, to handle the user-role reachability problem with the presence of role hierarchy. An extensive experimentation reports the superiority of our reductions in comparison with the approach used in the literature.

II. USER-ROLE REACHABILITY PROBLEM A. Role-Based Access Control

In Role-Based Access Control (RBAC), access decisions are based on the roles that individual users have as part of an organization. The process of defining roles is based on a

I. INTRODUCTION

Modern information systems contain sensitive information and resources that need to be protected against unauthorized users who want to steal it. The most important mechanism to prevent this is Access Control [START_REF] Capitani Di Vimercati | Access control policies and languages[END_REF] which is thus becoming increasingly important for today's ubiquitous systems. In general, access control policies protect the resources of the systems by controlling who has permission to access what objects/resources.

Role-Based Access Control (RBAC) [START_REF] Sandhu | Role-Based Access Control Models[END_REF] is one of the most widely adopted access control models in the real world. In RBAC, access control policies specify which users can be assigned to roles which, in turn, are granted permissions to perform certain operations in the system. Usually, RBAC policies need to be evolved according to the rapidly changing environments and thus, it is demanded to have some mechanisms to control the modification of the policies. Administrative RBAC [START_REF] Crampton | Understanding and developing role-based administrative models[END_REF] (ARBAC) is the corresponding widely used administrative model for RBAC policies. The main idea of ARBAC is to provide certain specific users, called administrators, some permissions to execute operations, called administrative actions, to modify the RBAC policies. In fact, permissions to perform administrative actions must be restricted since administrators can only be partially trusted. For instances, some of them may collude to, inadvertently or maliciously, modify the policies (by sequences of administrative actions) so that untrusted users can get sensitive permissions. Thus, automated analysis techniques taking into consideration the effect of all possible sequences of administrative actions to identify the safety issues, i.e. administrative actions generating policies by which a user can acquire permissions that may compromise some security goals, are needed.

Several automated analysis techniques (see, e.g., [START_REF] Li | Security analysis in role-based access control[END_REF], [START_REF] Jha | Towards formal verification of role-based access control policies[END_REF], [START_REF] Stoller | Efficient policy analysis for administrative role based access control[END_REF], [START_REF] Alberti | ASASP: Automated Symbolic Analysis of Security Policies[END_REF], [START_REF] Ferrara | VAC -Verifier of Administrative Role-based Access Control Policies[END_REF], [START_REF] Yang | Policy Analysis for Administrative Role Based Access Control without Separate Administration[END_REF]) have been developed for solving the userrole reachability problem, an instance of the safety issues, in the ARBAC model. One of the the main assumptions of such techniques is that the role hierarchy is constant and can be preprocessed by the approach proposed in [START_REF] Sasturkar | Policy analysis for administrative role based access control[END_REF]. However, this approach results in an exponential number of administrative actions considered in the analysis that negatively affects the performance of analysis tools.

In this paper, we introduce three reductions to enable an available analysis technique, namely ASASPXL, to handle the user-role reachability problem with the presence of role hierarchy. The main idea is to transform an ARBAC system with role hierarchy to an equivalent one without role hierarchy and then use available analysis techniques to analyze the system. The experimental results show that the performance of one of the proposed reductions is superior to the other two and much better than the approach proposed in [START_REF] Sasturkar | Policy analysis for administrative role based access control[END_REF]. The reason for this is that the number of administrative actions considered in the analysis is reduced significantly by using our reductions that allows for the generation of reachability problems with smaller state spaces.

The paper is organized as follows. Section II introduces the RBAC, ARBAC models, and the related analysis problem. Section III briefly introduces the automated analysis tool ASASPXL and the model checking technique underlying it. The three reductions to enable ASASPXL to handle the userrole reachability problem with the presence of role hierarchy are described in Section IV. Section V discusses the dynamic role hierarchy and how to extend our reductions to solve the user-role reachability problem in the context of dynamic role hierarchy. Section VI summarizes our experiments and Section VII concludes the paper. Fig. 1. User and Permission Assignments; and Role Hierarchies careful analysis of how an organization operates. Permissions are grouped by role name and correspond to various uses of a resource. A permission is restricted to individuals authorized to assume the associated role and represents a unit of control, subject to regulatory constraints within the RBAC model. For example, within a hospital, the role of doctor can include operations to perform diagnosis, prescribe medication, and order laboratory tests; the role of nurse can be limited to a strict subset of the permissions assigned to a doctor such as order laboratory tests.

We formalize a RBAC policy as a tuple (U, R, P, U A, P A, ) where U is a set of users, R a set of roles, and P a set of permissions. A binary relation UA ⊆ U × R represents a user-role assignment and a binary relation P A ⊆ R × P represents a role-permission assignment. A user-role assignment specifies the roles to which the user has been assigned while a role-permission assignment specifies the permissions that have been granted to a role. A partial order on R is a role hierarchy of the policy, where r 1 r 2 means that r 1 is more senior than r 2 for r 1 , r 2 ∈ R, i.e., every permission assigned to r 2 is also available to r 1 .

A user u is an explicit member of role r when (u, r) ∈ UA while the user u is an implicit member of role r if there exists r ∈ R such that r r and (u, r ) ∈ UA. A user u has permission p if there exists a role r ∈ R such that (r, p) ∈ P A and u is a (explicit or implicit) member of r.

Example 1 Consider an RBAC policy describing a department in a university as depicted in Figure 1. The top-left table is the user-role assignment, the top-right is the role-permission assignment, and the bottom is an example of role hierarchies (The role at the tail of an arrow is more senior than the one at the head).

Let us consider the user Charlie: he is an explicit member of role Faculty because the tuple (Charlie, Faculty) is in the user-role assignment UA. Additionally, role Faculty has been assigned to permissions AssignGrades, ReceiveHBenefits, and UseGym. Thus, Charlie can assign grades, receive benefits and use the gym through the role Faculty.

Let us consider the role hierarchy: role Faculty is more senior than role UEmployee (i.e., Faculty UEmployee). Therefore, Charlie is an implicit member of role UEmployee, and thus he can also use all permissions assigned to role UEmployee.

B. Administrative RBAC (ARBAC)

Access control policies need to be maintained according to the evolving needs of the organization. For flexibility and scalability in large distributed systems, several administrators are usually required and there is a need not only to have a consistent policy but also to ensure that the policy is modified by administrators who are allowed to do so.

Several administrative frameworks have been proposed on top of the RBAC model to address these issues. One of the most popular administrative frameworks is Administrative RBAC (ARBAC) [START_REF] Crampton | Understanding and developing role-based administrative models[END_REF] that controls how RBAC policies may evolve through administrative actions that update the UA and PA relations (e.g., actions that update UA include assigning or revoking user memberships into roles).

Formalization. Usually, administrators may only update the relation UA while PA and are assumed constant. This is because a change in PA and/or implies a change in the organization (see [START_REF] Stoller | Efficient policy analysis for administrative role based access control[END_REF] for more detail). From now on, we focus on situations where U and R are finite, P plays no role, and thus, a RBAC policy is a tuple (U, R, UA, ).

Since administrators can be only partially trusted, administration privileges must be limited to selected parts of the RBAC policies, called administrative domains. An administrative domain is specified by a condition defined as follows:

Definition 1 A pre-condition C is a finite set of expressions of the forms r or r where r ∈ R.

A user u ∈ U satisfies a pre-condition C with respect to a role hierarchy if, for each ∈ C, u is a member of r with respect to when is r or u is not a member of r with respect to when is r for r ∈ R. We say that r is a positive role and r is a negative role in C. Notice that the role membership must consider both explicit and implicit users (i.e., a user u is a member of role r if u is an explicit or implicit member of r) because of role hierarchy .

Permission to assign users to roles is specified by a ternary relation can assign containing tuples of the form (C a , C, r) where C a and C are pre-conditions, and r a role. Permission to revoke users from roles is specified by a binary relation can revoke containing tuples of the form (C a , r) where C a is a pre-condition and r a role. The relation can revoke is only binary because simple pre-conditions are useless when revoking roles (see, e.g., [START_REF] Stoller | Efficient policy analysis for administrative role based access control[END_REF]). In both cases, we say that C a is the administrative pre-condition, C is a (simple) precondition, r is the target role, and a user u a satisfying C a is the administrator. When there exist users satisfying the administrative and the simple (if the case) pre-conditions of an administrative action, the action is enabled. ARBAC transition system. We define an ARBAC transition system as a tuple (α 0 , ψ) where α 0 is the initial RBAC policy (U, R, UA 0 , ) and ψ is the (disjoint) union of the sets of administrative actions can assign and can revoke (i.e., ψ := (can assign, can revoke) ). A state of an ARBAC transition system is a tuple α where α is a RBAC policy. Since the administrative actions depend on and affect only the relations UA and , in the following, we abbreviate a RBAC policy (U, R, UA, ) as (UA, ). We define the effect of executing an administrative action in ψ by defining a binary relation → ψ on the states of the ARBAC system as follows:

Definition 2 (UA, ) → ψ (UA , ) iff there exist users u a and u in U such that either:

• there exists (C a , C, r) ∈ can assign, u a satisfies C a , u satisfies C (i.e. (C a , C, r) is enabled), and UA = UA ∪ {(u, r)} or • there exists (C a , r) ∈ can revoke, u a satisfies C a (i.e. (C a , r) is enabled), and UA = UA \ {(u, r)}.
A run of the ARBAC transition system

(α 0 , ψ) is a (pos- sibly infinite) sequence (UA 0 , ), (UA 1 , ), ..., (UA n , ), ... of states such that (UA i , ) → ψ (UA i+1 , ) for i ≥ 0.
Example 2 Consider the RBAC policy with the UA relation and role hierarchy depicted in Figure 1 and an administrative action ({PCMember }, {UMember }, Student) ∈ can assign, i.e., the administrative pre-condition is C a = {PCMember }, the simple pre-condition is C = {UMember }, and the target role is Student.

User Alice satisfies the pre-condition C a because (Alice, PCMember ) ∈ UA. User Eve satisfies the precondition C because he is an explicit member of role UEmployee that is more senior than role UMember (e.g., (F red, UEmployee) ∈ UA and UEmployee UMember . As a sequence, the administrative action is enabled.

We can update the current UA to UA = UA ∪ {(Eve, Student)} by executing the following instance of the administrative action specified above: administrator Alice (who has role PCMember ) assigns role Student to user Eve.

C. The User-role Reachability Problem

Normally, policy designers and administrators want to foresee if the interactions among administrative actions, as seen in the Example 2, can lead the system to conflict states violating the security requirements of the organization (e.g., the security requirements forbid a user being assigned to some sensitive roles). Thus, they need to analyze access control policies in order to discover such violation. This problem is called as the user-role reachability problem and is defined as follows.

Definition 3 A pair (u g , R g ) is called a (RBAC) goal for u g ∈ U and R g a finite set of roles. The cardinality |R g | of R g is the size of the goal.
Definition 4 Given an initial RBAC policy (UA, ), a goal (u g , R g ), and administrative actions ψ = (can assign, can revoke); (an instance of) the user-role reachability problem, identified by the tuple (UA, ), ψ, (u g , R g ) , consists of checking if there exists a finite sequence (UA 0 , ), (UA 1 , ), ..., (UA n , ) (for n ≥ 0) where (i)

(UA i , ) → ψ (UA i+1 , ) for each i = 0, ..., n -1 and (ii) u g is a member of each role of R g in (UA n , ).
In real scenario, subtle interactions between administrative actions in real policies may arise that are difficult to be foreseen by policy designers and administrators. Thus, automated analysis techniques are thus of paramount importance to analyze such policies and answer the user-role reachability problem. The analysis techniques we will present in the following will be able to establish this automatically for the problem in ARBAC.

III. MODEL CHECKING MODULO THEORIES AND THE REACHABILITY PROBLEM

Model Checking Modulo Theories (MCMT). MCMT [START_REF] Ghilardi | Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis[END_REF] is a framework to solve reachability problems for infinite state systems that can be represented by transition systems whose set of states and transitions are encoded as constraints in firstorder logic. Several systems have been abstracted using such symbolic transition system such as parametrised protocols, sequential programs manipulating arrays, timed system, etc (see again [START_REF] Ghilardi | Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis[END_REF] for an overview).

MCMT framework uses a backward reachability procedure that repeatedly computes the so-called pre-images of the set of goal states, that is usually obtained by complementing a certain safety property that the system should satisfy. Then, the set of backward reachable states of the system is obtained by taking the union of the pre-images. At each iteration of the procedure, the procedure checks whether the intersection between the set of backward reachable states and the initial set of states is non-empty (i.e., safety test) or not (i.e., the unsafety of the system: there exists a (finite) sequence of transitions that leads the system from an initial state to one satisfying the goal). Otherwise, when the intersection is empty, the procedure checks if the set of backward reachable states is contained in the set computed at the previous iteration (fix-point test) and, if yes, the safety of the system (i.e. no (finite) sequence of transitions leads the system from an initial state to one satisfying the goal) is returned. Since sets of states and transitions are represented by first-order constraints, the computation of pre-images reduces to simple symbolic manipulations and testing safety and fix-point to solving a particular class of constraint satisfiability problems, called Satisfiability Modulo Theories (SMT) problems, for which scalable and efficient SMT solvers are currently available (e.g., Z3 [12]).

ASASPXL. In [START_REF] Ranise | Boosting Model Checking to Analyse Large ARBAC Policies[END_REF], it is studied how the MCMT approach can be used to solve (variants of) the user-role reachability problem in ARBAC transition system with out role hierarchy. On the theoretical side, it is shown that the backward reachability procedure described above decides (variants of) the user-role reachability problem. On the practical side, extensive experiments have shown that an automated tool, called ASASPXL [START_REF] Ranise | Boosting Model Checking to Analyse Large ARBAC Policies[END_REF], has a good trade-off between scalability and expressiveness. The analysis tool ASASPXL is build on top of MCMT, the first implementation of the MCMT approach [START_REF] Ghilardi | Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis[END_REF], that gives some advantage. First, we only need to write a translator from instances of the user-role reachability problem to reachability problems in MCMT input language, a routine programming task. Second, MCMT has been developed and extensively used for the past years. It is thus more robust and offers a higher degree of confidence. Third, we can reuse some features of a better engineered incarnation of the MCMT approach that can be exploited to significantly improve performances. An exhaustive experiment in [START_REF] Ranise | Boosting Model Checking to Analyse Large ARBAC Policies[END_REF] has shown that ASASPXL is superior to the state-of-the-art analysis tools such as MOHAWK [START_REF] Jayaraman | Automatic Error Finding for Access-Control Policies[END_REF], VAC [START_REF] Ferrara | VAC -Verifier of Administrative Role-based Access Control Policies[END_REF], and PMS [START_REF] Yang | Policy Analysis for Administrative Role Based Access Control without Separate Administration[END_REF].

The structure of ASASPXL is depicted in Figure 2. It takes as input an instance of the user-role reachability problem and returns reachable, when there exists a finite sequence of administrative operations that lead from the initial RBAC policy to one satisfying the goal, and unreachable otherwise. To give such results, ASASPXL firstly pre-processes the original user-role reachability problem by module Heuristics that helps to refine the original problem to speed up the analysis in the module MCMT (see [START_REF] Ranise | Boosting Model Checking to Analyse Large ARBAC Policies[END_REF] for more details). Then, it translates the refined user-role reachability problem to the reachability problem in MCMT input language (module Translator). Next, ASASPXL invokes the model checker MCMT to verify the reachability of the problem. Finally, according to the answer returned by the model checker (in the data storage Explored Policies), ASASPXL refines it and returns reachable or unreachable as its output (module Refinement).

IV. SOLVING THE USER-ROLE REACHABILITY PROBLEM

WITH ROLE HIERARCHY The analysis tool ASASPXL (and all state-of-the-art analysis tools mentioned in Section III) assumes that the role hierarchy relation is constant and thus can be ignored when solving the user-role reachability problem (As the result, the role membership considers only explicit users instead of both implicit and explicit users as in Section II-B). In the following, we describe three reductions that pre-process away role hierarchies so that (an adapted version of) the technique in ASASPXL can be used to solve user-role reachability problem.

The first reduction, namely R A , is an adaptation of the approach proposed in [START_REF] Sasturkar | Policy analysis for administrative role based access control[END_REF] and applied to ASASPXL. The second one, namely R L , proposes a solution that aims to avoid the exponential explosion in size of the user-role reachability problem resulting from the application of R A . The last one R M exploits a feature of the analysis technique inside ASASPXL to atomize chains of the additional administrative actions generated in R L , thereby reducing significantly the possible interleavings to solve the user-role reachability problems.

A. Abstract Reduction R A

In [START_REF] Sasturkar | Policy analysis for administrative role based access control[END_REF], the authors propose an approach to analyze ARBAC policies with role hierarchies that applies a preprocess module to abstract away role hierarchy in the original user-role reachability problem and then using an available analysis technique to solve the problem. The main idea of the preprocess module is to replace each action in the original set of administrative actions ψ by a set of additional actions with respect to the hierarchies of roles being present in the pre-conditions of the original action. We adapt this approach to ASASPXL as follows.

Let consider the user-role reachability problem with role hierarchy (UA, ), ψ, (u g , R g ) as defined in Section II-C and the following abbreviations:

• Senior(r) stands for a set of all senior roles of r with respect to hierarchy • Senior(r) stands for a set of all senior roles of r with respect to hierarchy but is written in negative form r i where r i is a senior role of r

• Senior(C) = Senior(r 1 ) × Senior(r 2 ) × ... × Senior(r k )
where

C = {r 1 , r 2 , ..., r k } ⊆ R
The abstract reduction R A works as follows.

Step -For each set R g ∈ Senior(R g ): create a new userrole reachability problem without role hierarchy (UA), ψ, (u g , R g ) -The answer for the original user-role reachability problem is reachable iff one of the new problems (UA), ψ, (u g , R g ) returns reachable The main idea underlying Step 1 is to guarantee that a user satisfying a negative role r must not be assigned to any senior role of r while Step 2 exploits all possible associations of positive roles with respect to role hierarchy. We emphasize that solving the original user-role reachability problem with role hierarchy is now equivalent to solving a set of new userrole reachability problems without role hierarchy (Step 3). The idea is to ensure that if a role senior to r g ∈ R g (in the goal (u g , R g ) of the original problem) is reachable, then also r g is reachable.

Example 3 Consider an ARBAC system (α 0 , ψ) where α 0 = (UA 0 , ).

Let U = {Alice, Bob, Charlie, David, Eve, F red, Greg}, R = {PC (PCMember ), FA(Faculty), TA, ST (Student), UE (UEmployee), UM (UMember ), PT (PTEmployee)}, and = {(TA ST ), (PC FA), (PC PT ), (UE UM )}. The goal is (Eve, {ST , UM }).

The set ψ of administrative actions contains:

({PC }, {UM , ST }, PT ) ∈ can assign (1) ({FA}, ST ) ∈ can revoke (2)

Consider action (1) (the other actions will be processed in a similar way):

Step 1 of R A transforms action (1) ∈ ψ to the following action:

({PC }, {UM , ST , TA}, PT ) (3)
by replacing the negative role ST with the set Senior(ST ) = {ST , TA}.

Step 2 of R A adds the following administrative actions to ψ:

({PC }, {UM , ST , TA}, PT ) ∈ can assign (4) ({PC }, {UE , ST , TA}, PT ) ∈ can assign (5)
Notice how the original role UM is replaced with its senior UE (e.g., (UE UM )) in action [START_REF] Jha | Towards formal verification of role-based access control policies[END_REF].

The user-role reachability problem (UA 0 , ), ψ, (Eve, {ST , UM }) will be transformed to 4 userrole reachability problems without role hierarchy:

(UA 0 ), ψ, (Eve, {ST , UM }) (6) (UA 0 ), ψ, (Eve, {TA, UM }) (7) (UA 0 ), ψ, (Eve, {ST , UE }) (8) (UA 0 ), ψ, (Eve, {TA, UE }) ( 9
)
because of tuples (TA ST ) and (UE UM ) in role hierarchy 2

B. Linear Reduction R L

It is easy to see that the reduction R A , in the worst case, results in an exponential number of additional administrative actions in ψ (cf. Step 2 of R A ). As shown in [START_REF] Ranise | Boosting Model Checking to Analyse Large ARBAC Policies[END_REF], the number of administrative actions is the main source of complexity in solving the user-role reachability problem. Moreover, solving a single original user-role reachability problem (with hierarchy) now becomes to solving a set of new user-role reachability problems (user-role reachability analysis for ARBAC policy is PSPACE-complete [START_REF] Stoller | Efficient policy analysis for administrative role based access control[END_REF]). The crucial observation to avoid this is the following: if a user is assigned to a role r 1 and (r 1 r 2 ) ∈ , we can assume that the user is also assigned to role r 2 . In this case, we say that the user is implicitly assigned to role r 2 . This suggests to transform each tuple in the role hierarchy to a new administrative action of type can assign hier (similar to those of type can assign) such that when a user is assigned to a role r, he can be "implicitly" assigned to any junior role of r by executing the new actions. As we need only one additional action per tuple in role hierarchy , it is easy to see that the number of such actions is linear in the cardinality of .

The effect of explicit and implicit role memberships must be handled carefully. In fact, if a user u is assigned to a role r by a can assign action (explicit role membership), u then can be implicitly assigned to any junior role of r by executing the can assign hier actions mentioned above (implicit role membership). Now, if u is revoked from r by executing a can revoke action, then the role membership must be handled such that also all the junior roles of r that have been implicitly assigned to u must be revoked. Intuitively, to do this, we need to keep track of all the junior roles implicitly assigned to every user that is a computationally heavy task. To avoid this problem, we modify the structure of RBAC policies defined in Section II by adding a new relation UAH ⊆ U × R. Now, the relation UA is required to record only explicit role memberships (i.e., those resulting by executing can assign actions) while the new relation UAH record both the explicit and implicit ones.

Before describing the reduction R L , we introduce the new administrative action of type can assign hier as follows.

Definition 5 An administrative action of type can assign hier is of the form (r s r j ) where r s and r j are roles in R Moreover, to handle the effect of explicit and implicit role memberships, we need to modify the relation → ψ defined in Definition 2 in Section II-B as in the following. We note that a state of ARBAC transition system is modified by adding the new relation UAH and removing relation (since all tuples in are transformed to can assign hier actions): Definition 6 (UA, UAH ) → ψ (UA , UAH ) iff there exist users u a and u in U such that either:

• there exists (C a , C, r) ∈ can assign, u a satisfies C a , u satisfies C (i.e. (C a , C, r) is enabled), UA = UA ∪ {(u, r)}, and UAH = UAH ∪ {(u, r)} or • there exists (C a , r) ∈ can revoke, u a satisfies C a (i.e. (C a , r) is enabled), UA = UA \ {(u, r
)}, and UAH = UA or • there exists (r s , r j ) ∈ can assign hier , u satisfies {r s }, and UAH = UAH ∪ {(u, r j )}.

We note that the satisfiability of a user to a pre-condition is now with respect to relation UAH instead of UA as in Section II-B. We also emphasize that can assign actions update both UA and UAH while can assign hier ones update only UAH . Additionally, can assign hier actions do not require an administrator to be executed, it only requires to check that there exists a user u who is member of senior role r s to add the tuple (u, r j ) to UAH . An action of type can revoke removes a tuple from UA and then sets UAH to the updated value (i.e., after the removal of the tuple) of UA. The need of resetting UAH to UA after removing a tuple arises from the observation that removing an explicit role membership invalidates all the implicit ones in UAH related to it.

We are ready to define the linear reduction R L as follows:

Step 1 Processing negative roles in pre-conditions:

-For each tuple (C a , C, r) ∈ can assign: * for each negative role r occurring in C a : replace r with Senior(r) with respect to role hierarchy . * for each negative role r occurring in C: replace r with Senior(r) with respect to role hierarchy . -For each tuple (C a , r) ∈ can revoke: * for each negative role r occurring in C a : replace r with Senior(r) with respect to role hierarchy Step 2 Processing tuples in role hierarchy :

-For each tuple (r s r j ) ∈ : * add a can assign hier action (r s r j ) to the set of administrative actions ψ As argued above, the number of additional actions resulting by applying R L is linear to the number of tuples in role hierarchy . Moreover, R L does not need to refine the goal in the original user-role reachability problem as in the reduction R A (cf. Step 3 in R A ) and thus, avoid solving a set of (refined) reachability problems.

Example 4 Consider the ATRBAC system in Example 3 and

= {(TA ST ), (PC FA), (PC PT ), (UE UM )}.

After using

Step 1 to process negative roles in administrative actions as in Example 3, the reduction R L adds to the set ψ the following can assign hier actions:

(TA ST ), (10)
(PC FA), ( 11
) (PC PT ), (12)
(UE UM ), (13) 2
C. Composite Reduction R C
The reduction R L reduces significantly the number of actions added to the set ψ to simulate the role hierarchy . However, the sequences of can assign hier actions used to obtain junior roles may negatively affect the performances of analysis tools. In fact, if the depth of role hierarchy , i.e., the longest chain of the form (r 1 r 2 ), (r 2 r 3 ), ..., (r n r n+1 ) for (r i r i+1 ) ∈ with i = 1; ...; n, is large, we need to execute a long sequence of can assign hier actions (r 1 r 2 ), (r 2 r 3 ), ..., (r n r n+1 ) to implicitly assign the user to the most junior role. To avoid this problem, we exploit a feature of the analysis technique underlying the tool ASASPXL to "combine" the affect of the long sequence of can assign hier actions into an atomic administrative action. The main idea is to design a new version of action type can assign hier, namely m can assign hier, such that a user can be assigned to all the junior roles of a given role in one shot. We are now ready to define the composite reduction R C . In the following, we use Junior(r) = {r | r is more senior than r } to denote the set of all junior roles of a given role r:

Step 1 Processing negative roles in pre-conditions:

- The reduction R C adds to the set ψ the following m can assign hier actions:

(TA {ST }), ( 14
) (PC {FA, PT }), ( 15
) (UE {UM }), ( 16
)
Now, a user assigned to role PC can be implicitly assigned to all junior roles of PC by executing m can assign hier action (15) 2

V. DISCUSSION

In Section IV, we introduce three reductions to enable available analysis technique to handle the user-role reachability problem with the presence of role hierarchy. The main idea is to transform an ARBAC system with role hierarchy to an equivalent one without role hierarchy and then use available analysis techniques to analyze the system. While proposed reductions is only capable of transforming static role hierarchy, i.e., role hierarchy is assumed to be constant during the analysis, that is usually happening in real scenario 1 , some specific applications may require some modification to the role hierarchy that is also supported by ARBAC framework in [START_REF] Crampton | Understanding and developing role-based administrative models[END_REF]. In such applications, role hierarchy can be modified by administrative actions that add or delete some tuples to/from (now we also call as a dynamic role hierarchy). As a result, the analysis techniques need to consider not only the administrative actions modifying the relation UA but also actions modifying the role hierarchy .

In fact, we can use the idea of simulating the effect of role hierarchy in the reductions R C and R L , e.g., using can assign hier and m can assign hier actions, to design an approach to solve the user-role reachability problem in the context of dynamic hierarchy as follows: First, we represent all possible role relationships (r 1 r 2 ) by using a set of can assign hier actions as in R L . Then, the effect of administrative actions that modify the role hierarchy can be simulated by enabling or disabling the execution of corresponding can assign hier actions. For instance, adding a tuple (r 1 r 2 ) to role hierarchy will make the can assign hier action (r 1 r 2 ) enabled and vice versa. Because the role hierarchy now is represented by a set of can assign hier actions, it can be abstracted away and thus, it is possible to reuse available analysis techniques such as ASASPXL to solve the user-role reachability problem in the context of dynamic hierarchy. The details of this approach and its implementation is left as our future work.

VI. IMPLEMENTATION AND EXPERIMENTS

We implement three reductions R A , R L , and R C on top of the analysis tool ASASPXL using Python. Basically, we build a module named Pre-processing module containing three submodules R A , R L , and R C and then put it in front of the module Heuristics in the structure of ASASPXL depicted in Figure 2. Now, ASASPXL takes as input an instance of the user-role reachability problem with role hierarchy and, depending on the reduction used, it forwards the problem to R A , R L , or R C accordingly to process the role hierarchy. Then, ASASPXL solves the problem by using modules Heuristics, Translator, MCMT, and Refinement as described in Section III.

To evaluate the scalability of the three reductions, we generate synthetic benchmark as follows: we use the ARBAC user-role reachability problems from [START_REF] Ferrara | VAC -Verifier of Administrative Role-based Access Control Policies[END_REF] and add randomly generated role hierarchies organized-as suggested in [START_REF] Li | Administration in Role Based Access Control[END_REF]as lattices with a senior-most and a junior-most role. The We emphasize that it is not possible to compare ASASPXL (with the three reductions) with the other state-of-the-art analysis tool since they do not support specific features that we need to build the reductions R L and R C as discussed in the beginning of Section IV-B and IV-C.

VII. CONCLUSIONS

We have introduced three reductions R A , R L , and R C that pre-process away role hierarchies so that (an adapted version of) the technique in ASASPXL can be used to solve userrole reachability problem in ARBAC. The experimental results show that the performance of R C is better than that of R L and much better than R A . This is because the number of additional administrative actions is reduced significantly by using R C and R L that allows for the generation of problems with smaller state spaces.

As future work, we plan to study how to extend our approach to cope with the dynamic role hierarchies. In fact, we can use the idea of simulating role hierarchy in the reductions R C and R L , i.e., using can assign hier and m can assign hier actions to simulate the affect of role hierarchy, to design an approach in the context of dynamic hierarchy as discussed in Section V.

1

 1 Processing negative roles in pre-conditions: -For each tuple (C a , C, r) ∈ can assign: * for each negative role r occurring in C a : replace r with Senior(r) with respect to role hierarchy . * for each negative role r occurring in C: replace r with Senior(r) with respect to role hierarchy . -For each tuple (C a , r) ∈ can revoke: * for each negative role r occurring in C a : replace r with Senior(r) with respect to role hierarchy Step 2 Processing positive roles in-preconditions: -For each (C a , C, r) ∈ can assign: * Let C + a = {r 1a , r 2a , ..., r ka } denote the set of all positive roles in C a and C + = {r 1 , r 2 , ..., r l } denote the set of all positive roles in C. Let C - a and C -denote the set of all negative roles in C a and C, respectively * for each tuple (r 1a , r 2a , ..., r ka ) ∈ Senior(C + a ) and tuple (r 1 , r 2 , ..., r l ) ∈ Senior(C + ): add to ψ the administrative action ({r 1a , r 2a , ..., r ka } ∪ C - a , {r 1 , r 2 , ..., r l } ∪ C -, r) -For each (C a , r) ∈ can revoke: * Let C + a = {r 1a , r 2a , ..., r ka } denote the set of all positive roles in C a and C - a denote the set of all negative roles in C a

Fig. 2 .

 2 Fig. 2. ASASPXL architecture

  hier is of the form (r s C) where r s is a role in R and C ⊆ RThe relation → ψ is similar to one defined in Definition 6 except the semantic of can assign hier actions is replaced by that of m can assign hier as follows.

  benchmark contains policies inspired by a university whose number of roles is 40, the number of administrative actions from 217 to 492, and the cardinality | | of role hierarchy from 10 to 300. All the experiments were performed on an Intel Core I5 (2.6 GHz) CPU with 4 GB Ram running Ubuntu 11.10. Table I reports the experimental results of running three reductions R A , R L , and R C on the benchmark. Column 1 shows the name of the test case, column 2 contains the number of roles, administrative operations, and | | in the policies. Columns 3, 4, and 5 show the average execution times (in seconds) taken by ASASPXL with using the three reductions R A , R L , and R C , respectively.The results show the superiority of the last reduction R C over the other two. It is also clear that R A is the less scalable of the three. The reason comes from the fact that number of additional administrative actions generated by R L and R C

Fig. 3 .Figure 3

 33 Fig. 3. Performance when varying | |

  For each tuple (C a , C, r) ∈ can assign:

	* for each negative role r occurring in C a : re-
	place r with Senior(r) with respect to role
	hierarchy .
	* for each negative role r occurring in C: replace
	r with Senior(r) with respect to role hierarchy
	.
	-For each tuple (C a , r) ∈ can revoke:
	* for each negative role r occurring in C a : re-
	place r with Senior(r) with respect to role
	hierarchy
	Step 2 Processing tuples in role hierarchy :
	-For each role r ∈ R:
	* If Junior(r)	=	∅ then add a
	i can assign hier action (r Junior(r)) to
	the set of administrative actions ψ
	Example 5 Consider again the ATRBAC system in Example 3
	and = {(TA	ST ), (PC	FA), (PC	PT ), (UE
	UM )}.

TABLE I EXPERIMENTAL

 I RESULTS ON THE BENCHMARK IN[START_REF] Yang | Policy Analysis for Administrative Role Based Access Control without Separate Administration[END_REF] is reduced significantly in comparison with that of R A as discussed in Section IV-B.

	Test	# Roles # Rules	RA	RL	RC
	case	# | |
	Test 1	40 287 10	1.25	0.93	0.28
	Test 2	40 217 20	2.91	1.17	0.82
	Test 3	40 262 50	3.73	1.14	1.03
	Test 4	40 296 50	2.51	1.12	0.97
	Test 5	40 480 100	8.31	4.27	1.97
	Test 6	40 479 150	22.56 11.32	5.09
	Test 7	40 467 150	47.22 10.92	6.12
	Test 8	40 484 200	51.27 13.65	5.27
	Test 9	40 463 250	45.15 19.92	6.91
	Test 10	40 492 300	39.92 17.21	10.62

Authorized licensed use limited to: CEA. Downloaded on June 28,2022 at 08:31:10 UTC from IEEE Xplore. Restrictions apply.

• there exists (r s , C) ∈ m can assign hier , u satisfies {r s }, and UAH = UAH ∪ {(u, r j )|r j ∈ C}.

This is because role hierarchy closely reflects the structure of the organizations in which the policies are used, thus, the modifications to role hierarchy should be rare as they imply substantial changes to the organizations themselves.