Adventures in the Analysis of Access Control Policies

Abstract

Access Control is becoming increasingly important for today’s ubiquitous systems which provide mechanism to prevent sensitive resources 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. In this paper, we consider the analysis problem in the context of the Administrative Role-Based Access Control (ARBAC), one of the most widespread administrative models. We describe how we design heuristics to enable an analysis tool, called asaspXL, to scale up to handle large and complex ARBAC policies and a sequence of analysis problems. An extensive experimentation shows that the proposed heuristics play a key role in the success of the analysis tool over the state-of-the-art analysis tools.

1 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 [4] which is thus becoming increasingly important for today’s ubiquitous systems. In general, access control systems protect the resources of the systems by controlling who has permission to access what objects/resources.

Today, one of the most widely adopted access control models in the real world is Role-Based Access Control (RBAC) model [12]. In general, 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. 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 (ARBAC) [3] is the corresponding widely used administrative model for RBAC policies. In ARBAC, certain specific users, called administrators, are provided 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., [1, 5, 10, 15, 16]) have been developed for solving the user-role reachability problem, an instance of the safety issues, in the ARBAC model. Recently, a tool called asaspXL [11] has been shown to perform better than the state-of-the-art tools on sets of benchmark problems in [9, 15]. The main advantage of the analysis technique inside asaspXL over the state-of-the-art techniques is that the tool can solve the user-role reachability problem with respect to a finite but unknown number of users in the policies manipulated by the administrative actions. However, asaspXL does not scale to solve problems in some recently proposed benchmarks in [16]. This is because the so-called state explosion problem has not been handled carefully and thus, prevent asaspXL to tackle such benchmarks. Additionally, asaspXL does not also scale to solve a sequence of reachability problems. The main reason is that the explored states during the previous analysis processes are not optimized.

In this paper, we study how to design heuristics to enable asaspXL to analyze large and complex instances of user-role reachability problems and also to analyse the sequence of reachability problems more efficiently. The main idea is to try to alleviate the state explosion problem, which is well-known problem in model checking techniques, and reuse as many as possible the explored states, in the analysis of ARBAC policies. We also perform an exhaustive experiment to conduct the effectiveness of proposed heuristics and compare asaspXL’s performance with the state-of-the-art analysis tools.

The paper is organized as follows. Section 2 introduces the RBAC, ARBAC models, and the related analysis problem. Section 3 briefly introduces the framework to automatically analyse the infinite state transition systems, namely mcmt. The proposed heuristics to enable asaspXL to scale to solve user-role reachability problem are described in Sect. 4. Section 5 summarizes our experiments and Sect. 6 concludes the paper.

2 Administrative Role-Based Access Control

In the Role-Based Access Control (RBAC) model [12], access decisions are based on the roles that individual users have as part of an organization. Permissions are grouped by role name and correspond to various uses of a resource. Roles can have overlapping responsibilities and privileges, i.e. users belonging to different roles may have common permissions. Thus, it would be inefficient to repeatedly specify common permissions for a certain set of roles. To overcome this problem, (so-called) role hierarchies reflect the natural structure of an enterprise and make the specification of policies more compact by requiring that one role may implicitly include the permissions that are associated with another role.

Once RBAC policies are determined they need to be maintained according to the evolving needs of the organization. For flexibility and scalability, large systems usually require several administrators, and thus there is a need not only to have a consistent RBAC policy but also to ensure that the policy is only modified by the administrators who are allowed to do so. One of the most popular administrative frameworks is the Administrative RBAC (ARBAC) model [3] whose main insight is to use RBAC to control how RBAC policies may evolve through administrative actions that assign or revoke user memberships into roles. Since administrators can be only partially trusted, administration privileges must be limited to selected parts of the RBAC policies, called administrative domains. The ARBAC model defines administrative domains by using roles and RBAC itself to control how security officers can delegate (part of) their administrative permissions to trusted users. In this way, several administrators are able to modify the RBAC policy of a large system by following certain rules.

Formalization. Let U be a set of users, R a set of roles, and P a set of permissions. Users are associated to roles by a binary relation $UA\subseteq U\times R$ and roles are associated to permissions by another binary relation $PA\subseteq R\times P$. A role hierarchy is a partial order $\succeq$ on R, where $r_1\succeq r_2$ means that $r_1$ is more senior than $r_2$ for $r_1,r_2\in R$. A user u is a member of role r when $(u,r)\in UA$. A user u has permission p if there exists a role $r\in R$ such that $(p,r)\in PA$ and u is a member of r. A RBAC policy is a tuple $(U,R,P,UA,PA,\succeq )$.

Usually (see, e.g., [15]), administrators may only update the relation UA while PA and $\succeq$ are assumed constant. An administrative domain is specified by a pre-condition, i.e. a finite set of expressions of the forms r or $\overline{r}$ (for $r\in R$), called role literals. A user $u\in U$ satisfies a pre-condition C if, for each $\ell \in C$, u is a member of r when $\ell$ is r or u is not a member of r when $\ell$ is $\overline{r}$ for $r\in R$. 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. In both cases, we say that $C_a$ is the administrative pre-condition, C is a (simple) pre-condition, 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. The relation $can\_revoke$ is only binary because simple pre-conditions are useless when revoking roles (see, e.g., [15]).

The semantics of the administrative actions in $\psi :=( can\_assign , can\_revoke )$ is given by the binary relation $\rightarrow _{\psi }$ defined as follows: $UA\rightarrow _{\psi } UA'$ iff there exist users $u_a$ and u in U such that either (i) there exists $(C_a,C,r)\in can\_assign$, $u_a$ satisfies $C_a$, u satisfies C (i.e. $(C_a,C,r)$ is enabled), and $UA'=UA\cup \{ (u,r)\}$ or (ii) there exists $(C_a,r)\in can\_revoke$, $u_a$ satisfies $C_a$ (i.e. $(C_a,r)$ is enabled), and $UA'=UA\setminus \{ (u,r)\}$. A run of the administrative actions in $\psi :=( can\_assign , can\_revoke )$ is a possibly infinite sequence $UA_0,UA_1, ..., UA_n, ...$ such that $UA_i\rightarrow _{\psi } UA_{i+1}$ for every $i\ge 0$.

A pair $(u_g,R_g)$ is called a (RBAC) goal for $u_g\in U$ and $R_g$ a finite set of roles. The cardinality $|R_g|$ of $R_g$ is the size of the goal. Given an initial RBAC policy $UA_0$, a goal $(u_g,R_g)$, and administrative actions $\psi =( can\_assign , can\_revoke )$; (an instance of) the user-role reachability problem consists of establishing if there exists a finite sequence $UA_0, UA_1, ..., UA_n$ (for $n\ge 0$) where (i) $UA_i\rightarrow _{\psi } UA_{i+1}$ for each $i=0, ..., n-1$ and (ii) in the policy $UA_n$ we have that $u_g$ is a member (explicit or implicit) of each role in $R_g$.

The definition of the user-role reachability problem considered here is the same of that in [15]. In the rest of the paper, we focus on user-role reachability problems where U and R are finite, P plays no role, and $\succeq$ is ignored because it can be eliminated by a pre-processing [13]. Thus, a RBAC policy is a tuple (U, R, UA) or simply UA when U and R are clear from the context.

3 Framework to Analyse Infinite State Transition Systems

mcmt [7] attempts to solve reachability problems for a certain class of infinite state systems whose state variables are arrays, that can be seen as functions mapping indexes to elements. Such transition systems can be used as suitable abstractions of parametrised protocols, sequential programs manipulating arrays, etc. The main idea underlying mcmt is to use a backward reachability procedure that repeatedly computes pre-images of the set of goal states, that is usually obtained by complementing a certain safety property that the system should satisfy. The set of backward reachable states of the system is obtained by taking the union of such pre-images. At each iteration of the procedure, it is checked whether the intersection with the initial set of states is non-empty (safety test), reporting the unsafety of the system, i.e. 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, it is checked if the set of backward reachable states is contained in the set computed at the previous iteration (fix-point test), reporting the safety of the system, i.e. no (finite) sequence of transitions leads the system from an initial state to one satisfying the goal. The peculiarity of mcmt is that sets of states and transitions are represented by first-order formulae so that the computation of pre-images boils down to logical manipulations and the safety and fix-point tests are reduced to satisfiability checks of first-order formulae. The resulting satisfiability problems are efficiently solved by state-of-the-art tools, called Satisfiability Modulo Theories (SMT) solvers.

mcmt was successfully used for the verification of several infinite state systems [6] and features some interesting heuristics to automatically synthesize invariants that can be used to prune the search space of the system that become also available to the user for a deeper understanding of the structure of the system. For more details on mcmt, the interested reader is pointed to [7]. Since model checking techniques have been found quite useful for the analysis of authorization policies, it would be interesting to apply mcmt in this context. Unfortunately, as observed in [1], there some practical problems to do this. Two of the most important ones are the following:

• P1 mcmt permits only mono-dimensional arrays while RBAC policies seem to require at least bi-dimensional arrays to encode the characteristic function of the binary relation UA.

• P2 mcmt restricts the number of existentially quantified variables in formulae representing transitions to (at most) two while can_assign and can_revoke actions usually require more of such variables.

These and other problems have lead us to build a new tool, called asasp [1], based on the same ideas of mcmt but specifically tuned for the symbolic analysis of authorization policies. We were successfull in doing this as asasp shows a better scalability than rbac-pat [8] on a set of synthetic user-role reachability problems introduced in [15]. However, our aim in building asasp was to reach a good trade-off between efficiency and expressivity. In fact, we were able to extend the classical ARBAC policies with attributes and to efficiently solve the associated user-role reachability problems in [2]. Key to the expressivity of asasp input language is the capability of handling arbitrary (possibly infinite) set of roles—such as those depending on parameters, see, e.g., [14]—and several existentially quantified variables in formulae representing transitions that are fundamental to express conditions involving role hierarchies and attribute values [2].

Almost at the same time of [1], a new tool, called mohawk [9], has been proposed for the analysis of ARBAC policies especially tailored to error-finding rather than verification as it is the case of both rbac-pat and asasp. In [9], it is shown that mohawk outperforms rbac-pat on the problems in [15] and on a new set of synthetic, much larger problems. Indeed, we tried asasp on new problems of mohawk and, rather disappointingly, it was not able to scale up and handle large problem instances. After a careful analysis of the behavior of asasp, we made the following crucial observations.

• O1 Since the set R of roles is finite, it is not necessary to use the binary relation UA to record user-role assignments. It is sufficient to replace it with a finite collection of sets, one per role. Formally, let $R=\{ r_1, ..., r_n\}$ for $n\ge 1$, define $U_{r_i}= \{ u | (u,r_i)\in UA\}$ for $i=1, ..., n$. Straightforward modifications to the definition of $\rightarrow _{\psi }$ (for $\psi$ a pair of relations can_assign and can_revoke), given in Sect. 2, allows one to replace UA with the $U_{r_i}$’s.

• O2 Since the role-hierarchy can be pre-processed before attempting to solve a user-role reachability problem (see, e.g., [13]), the definition of $\rightarrow _{\psi }$, for a given tuple in can_assign or can_revoke, existentially quantifies over two users, the administrator and the user to which the administrative action is going to be applied.

On the one hand, the two observations suggest that asasp expressivity is too much for modelling large synthetic problems (as those in [9]) that are characterized by simple pre-conditions in which even role hierarchies are not used. Since it is well-known that expressivity and efficiency are opposing forces when developing automated analysis techniques, we believe this to be one of the main reasons for the poor results obtained by asasp on the problems in [9]. On the other hand, O1 and O2 pave the way to the use of mcmt on this kind of synthetic problems as they remove the two problems discussed above. In particular, we can represent the characteristic function of a $U_{r_i}$ by using a mono-dimensional array $a_{r_i}$ mapping users to Booleans; thus overcoming P1. Also P2 is no more a problem as mcmt supports the definition of transitions by formulae containing (at most) two existentially quantified variables.

We illustrate the encoding in mcmt of user-role reachability problem by means of an excerpt of an example from [15].

Example 1

Let $U=\{ u_1, u_2\}$, $R=\{r_a, r_{1}, ..., r_{8}\}$, and $UA := \{ (u_1,r_{1}), (u_1,r_{4})$, $(u_1,r_{7}), (u_2, r_a) \}$ and the tuple $(\{r_a\}, \{r_{1}\}, r_{2})$ is in can_assign whereas the tuple $(\{r_a\}, r_{1})$ is in can_revoke. The goal of the user-role reachability problem is $\{(u_1, r_{6})\}$.

To formalize this problem in mcmt, we introduce one array per role $u_r$ for $r\in R$ mapping a user in U to a Boolean that encodes the characteristic function of the set $U_r$, as defined above. The initial relation UA can be expressed as follows:

$$\begin{aligned} \forall x.\left[ \begin{array}{l} u_{r_{1}}(x) \leftrightarrow x=u_1 \wedge u_{r_{4}}(x) \leftrightarrow x=u_1 \wedge u_{r_{7}}(x) \leftrightarrow x=u_1 \wedge u_{r_{a}}(x) \leftrightarrow u=u_2 \wedge \\ \lnot u_{r_{2}}(x) \wedge \lnot u_{r_{3}}(x) \wedge \lnot u_{r_{5}}(x) \wedge \lnot u_{r_{6}}(x) \end{array} \right] \end{aligned}$$

The tuple $(\{r_a\}, \{r_{1}\}, r_{2})$ in can_assign is formalized as

$$\begin{aligned} \exists x_a,x.\left[ \begin{array}{l} u_{r_{a}}(x_a) \wedge u_{r_{1}}(x) \wedge \forall y.(u_{r_{2}}'(y) \leftrightarrow (y=x\vee u_{r_{2}}(x))) \end{array} \right] \end{aligned}$$

and $(\{r_a\}, r_{1})$ in can_revoke as

$$\begin{aligned} \exists x_a,x.\left[ \begin{array}{l} u_{r_{a}}(x_a) \wedge u_{r_{1}}(x) \wedge \forall y.(u_{r_{1}}'(y) \leftrightarrow (y\ne x\wedge u_{r_{2}}(x))) \end{array} \right] \end{aligned}$$

where $u_r$ and $u_r'$ indicates the value of $U_r$ immediately before and after, respectively, of the execution of the administrative action and we have omitted identical updates, i.e. a conjunct $\forall y.(u_{r}'(y) \leftrightarrow u_{r}'(y))$ for each r not mentioned in the formula. Finally, the goal can be represented as $\exists x.u_{r_{6}}(x)\wedge x=u_1$.   $\square$

We built a translator to create mcmt reachability problems out of user-role reachability problems and mcmt on the problems resulting from the translations of those in [9]: the results were still disappointing in terms of scalability. After analysing the behavior of mcmt, we identified another important source of complexity: the number of transitions or, equivalently, the number of tuples in can_assign and can_revoke is so large that the heuristics implemented in mcmt to control the state space explosion problem are not enough. This is due to the fact that the problems that mcmt is successful in solving comprise tens of transitions, each one involving complex conditions and updates of data structures and updates. Instead, the transitions obtained from the translation of user-role reachability problems in [9] are hundreds or thousands (up to 80,000) involving, as discussed above and shown in the example, simple conditions and updates. In the following section, we describe how this difficulty can be tamed by designing a suitable wrapper around mcmt in order to generate a sequence of user-role reachability problems with an increasing number of transitions. We will also explain how the solution of the problem $P_i$ (for $i>0$) in the sequence can be speeded up by caching the invariants synthesized by mcmt in the runs to solve $P_0, ..., P_{i-1}$. The synthesized invariants encode “structural” properties of the user-assignment relation UA; e.g., ‘a given role can be assigned to no user’ or ‘if a user is not assigned to a certain set of roles then he/she will not be assigned to the roles in another set.’ Clearly, this kind of properties is using when solving problem $P_i$. For example, if we know from a previous run of mcmt that no user can be assigned to role $r_7$ and the goal of the user-role reachability problem is $(u,\{r_1, r_7, r_9\})$, we can immediately conclude that the goal is unreachable.

4 asasp 2.1: New Clothes for Analyzing ARBAC Policies

In this section, we describe the architecture of our technique. asasp 2.1 receives an ARBAC policy and a safety query as its input. In case it finds a sequence of transitions (including can_assign, can_revoke rules) that leads the RBAC system to the query state, the result UNSAFE is reported. Otherwise, asasp 2.1 reports that the system is SAFE. Figure 1 illustrates the architecture of asasp 2.1.

Fig. 1.

asasp 2.1 architecture

In general, the policy and the query are verified through the following steps:

• Pre-processing: The query is analyzed to find the answer in the database. If an answer is found, the result is reported without running the remains of the technique.

• Administrative Action Filter: The policy and the query are analyzed to filter the related transitions and roles for current verification step.

• Model checking: The technique verifies the filtered policy. The model checker mcmt [7] is used in the verification.

• Learning: The learning component analyzes the verification result before outputting them.

We discuss the details of these steps here in the remains of this section. Because of the separate administration restriction [..], we do not care the administrative roles in asasp 2.1.

4.1 Pre-processing

In general, the time spent in running the model checker holds the most important part in the amount of time taken for the verification process of automatic analysis techniques. Therefore, if we reduce the time spent in running the model checker, the total time will also be reduced significantly. With our technique, if the answer is found in this pre-processing step, asasp 2.1 returns the result without calling other components, including mcmt, and hence the time for verification process is reduced.

In order to speed up the verification processes, the states which have been visited in the previous verifications are saved to a database. When a new query is issued, asasp 2.1 first checks the database to find the answer for the query. If it finds the answer, the result is reported. Otherwise, the remains of the technique are called. For example: in the database, we have a state in which “User x is assigned both role A and role B.” This state is marked as an unsafe state. It means that the state is reachable from the initial state of the policy. When a new query such as “User x can be assigned role A or not” is issued, asasp 2.1 finds in the database and returns UNSAFE. This means that there exists a sequence of transitions which lead the system from the initial state to the query state. Another example is that a state in which “User y is assigned both role B and role C” is marked as a safe state in the database. A safe state means that it is unreachable from the initial state. If asasp 2.1 receives a query such as “User y can be assigned role A, role B and role C at the same time or not”, it returns the result SAFE quickly.

4.2 Administrative Action Filter

For a complex ARBAC policy with many users, roles and transitions, it is not efficient to analyze the entire policy. Many previous techniques fail to verify these policies. The reason is that the model checkers used in these techniques require large resources, including memory and processor, to verify the entire policies, meanwhile, hardware technologies currently can not satisfy these requirements. Therefore, there is a need to filter these policies before sending to the model checkers for verifying. The model checkers then can verify these filtered policies in a reasonable time.

In this analysis step, our technique removes all the redundant transitions, users and roles which do not relate to the current verification process. Moreover, the technique also reuses the states which have been verified in the previous verification processes to speed up the current verification.

The idea to filter the complex policies comes from the one in [9]. In this technique, the authors refine the complex policies according to the related-by-assignment relationship between roles. At each refinement step, the technique selects the users, roles and transitions which relate to the roles in the current priority degree. The refined policy is then verified by a model checker. In our technique, we do not define the priority of each role, we just care which roles is related to the current analysis step. The roles related to the first analysis step are the roles in the safety query. We call the set of the roles related to the current analysis step as a current related role set. In the current analysis step, asasp 2.1 analysis the policy to extract the transitions related to current analysis step. A transition is related to the current analysis step if its goal contains at least one role in the current related role set. For example, in the first analysis step of the policy in Fig. 2, the current related role set contains role Manager. The set of the transitions related to the first analysis step contains $( Admin , QC \wedge IT , Manager )$, $( Admin , Tester , Manager )$, and $( Admin , Manager )$.

Fig. 2.

An example of ARBAC policy

Moreover, asasp 2.1 also considers removing the transitions which are not able to be executed in the current verification step. The idea comes from the observation that a transition may be executed if the preconditions of the transition are satisfied (e.g., the transition $( Admin , QC \wedge IT , Manager )$ may be executed if there is at least one user who has both roles $QC$ and $IT$). In our technique, we use the idea with less constraint as follows: a transition may be executed (and therefore this transition will be added to the current filtered policy) if each role in its precondition is:

• In the initial state or

• In the current related role set and there is at least a transition in the original policy whose goal contains the role.

For example in Fig. 2: we assume that the current related role set includes Manager and Tester. The transition $( Admin , Developer \wedge QA , Tester \wedge QC )$ is a transition related to the current analysis step because its goal $Tester \wedge QC$ contains the role Tester. Furthermore, all roles in its precondition $Developer \wedge QA$ are in the initial state. This transition therefore is added to the current filtered policy. The transition $( Admin , QC \wedge IT ,$ $Manager )$ is also a transition related to the current analysis step. However, it is not added to the current filtered policy because the roles in its precondition are not in the current related role set and there is no transition whose goal contains the role $IT$.

After running the current analysis step, asasp 2.1 will calculate the set of the roles related to next analysis step. The next related role set will contain all roles in the current related role set. Moreover, for each assignment transition (can_assign rule) in the set of the transitions related to the current analysis step, the roles in its precondition will also be added to the next related role set if: for each role in the precondition, there is at least a transition in the original policy whose goal contains the role. For example in Fig. 2, we assume that the current related role set includes Manager. The set of transitions related to the current analysis step is $\langle ( Admin , QC \wedge IT , Manager ), ( Admin , Tester , Manager ), ( Admin ,$ $Manager )\rangle$. After running the analysis step, the next related role set will be $\langle Manager , Tester \rangle$. The roles $QC$ and $IT$ of the transition $( Admin , QC \wedge IT , Manager )$ are not added to the next related role set because there is no transition in the original policy whose goal contains the role $IT$.

One of the key points in our technique is to reuse the states which have been visited in the previous verifications. Normally, the users tend to query the policy many times with different safety queries, hence the reuse of visited states will reduce the time taken by the model checker significantly. In our technique, the results of the previous verifications were analyzed by the learning component after the model checker found the answer for the previous queries. All states extracted from the results and their statuses (safe or unsafe) were saved to the database. This information is then added to each analysis step of the current verification. Intuitively, each unsafe state can be considered as an initial state of the filtered policy of the current analysis step. If the state in the query can be reachable from one of these initial states, it is also unsafe. However, this implementation requires that the model checker supports the system with multiple initial states. In the current version of asasp 2.1, we use another way to add the visited states to the current filtered policy. The idea is that:

• For each unsafe state, a new transition which “connects” the initial state to the unsafe state will be added to the filtered policy.

• For each safe state, we remove from the filtered policy the transitions whose preconditions contain the roles in the safe state.

Fig. 3.

Reusing visited states

For example in Fig. 3(a), from the previous verifications, state B, C and D are un-safe states while state G is a safe state. At the current verification, two new transitions are added and one transition is removed. The current policy is shown in Fig. 3(b). If we want to check state E, we just go backward to state C and then can reach the initial state. If we want to check state F, we do not care the states G, H and I.

After executing the current analysis step, the filtered policy is transfer to the verification step in order to determine whether the query state is safe or not. If the state is unsafe, asasp 2.1 will call the learning step to analyze the results and then terminate the verification process. Otherwise, asasp 2.1 will call the next analysis step to refilter the policy. After the next analysis step, if some transitions can be added to the current filtered policy, the verification step then will be called to verify the new filtered policy. If the current filtered policy is not changed, the results of the verification step will be transfer to the learning step and the verification process is terminated after finishing the learning step.

4.3 Model Checking

In this step, asasp 2.1 translates the filtered policy and the query to an infinite state based system in the MCMT code. It then invokes MCMT to verify the system. If MCMT determines that the query is satisfied in the filtered policy, it returns the result UNSAFE as well as a log file. The log file contains a sequence of transitions that leads the system from the initial state to the query state. Similarly, the result SAFE and a log file are also returned if the model checker determines that the query is not satisfied in the filtered policy. In this case, the log file provides a list of invariants which are tracked during the verification. In case MCMT returns the result UNSAFE, the log file and the result are transferred to the learning component. In this component, the log file is analyzed in order to extract the unsafe states. No additional verification step is executed and the result is outputted after being analyzed. Conversely, asasp 2.1 calls again the analysis step to refilter the policy with the next related role set and an additional verification step may then be executed. After the analysis step, if some additional transitions are added to the previous filtered policy, asasp 2.1 will call the verification step again. Otherwise, it transfers the result and the log file of the previous verification step to the learning component. In this case, the learning component analyzes the log file to get the safe states and then outputs the result SAFE.

4.4 Learning

After verifying the policy, our technique will analyze the output of the verification step and save the states which have been visited during the verification. According to the result of the verification step, the learning component will process as follows:

• If the result UNSAFE is returned, the learning component analyzes the sequence of transitions which leads the RBAC system from the initial state to the query state. The states which are extracted from the analysis of these transitions then will be saved as unsafe states.

• If the result is SAFE, the learning component will extract invariants which have been tracked during the verification step. These invariants then will be saved as safe states.

In the next section, we provide an example to describe asasp 2.1’s operations in detail.

Table 1. The status of the analysis component during verification

4.5 Worked Out Example

We illustrate asasp 2.1’s operations using the example in Fig. 2. The safety query in this example asks whether Bob can be assigned to the role Manager or not. Table 1 describes the status of the analysis component during the verification: (RS: Current related role set; RT: Current set of related transitions; NRS: Next related role set; FT: the set of transitions in the current filtered policy). After the analysis step 1, mcmt returns the result SAFE. Therefore, a new analysis step is executed. When mcmt verifies the filtered policy in the analysis step 2, the result UNSAFE is returned. asasp 2.1 then calls the learning component to analyze the output of the verification step 2. The query state can be reached by executing the following sequence of transitions:

• $Bob$ is assigned to $Tester$ and $QC$ by the transition $( Admin , Developer \wedge QA , Tester \wedge QC )$.

• $Bob$ is then assigned to $Manager$ by the transition $( Admin , Tester , Manager )$.

The learning component finds and saves the unsafe state $( Bob , Developer \wedge QA \wedge Tester \wedge QC \wedge Manager )$ to the database. The state means that the user $Bob$ has roles $Developer$, $QA$, $Tester$, $QC$ and $Manager$ at the same time. At the next verification, if the query asks whether $Bob$ can be assigned to the role $QC$ or not, asasp 2.1 returns the result UNSAFE without running the model checker.

5 Experimental Evaluation

In this section, we show the evaluation we conducted in order to evaluate the effectiveness of our technique. In [9], the authors compared mohawk to other state-of-the-art verification tools for ARBAC policies such as symbolic model checking, bounded model checking and RBAC-PAT [8]. They also demonstrated that mohawk is more efficient than other tools. In this paper, instead of comparing our tool to the symbolic model checking, the bounded model checking or RBAC-PAT, we just compare asasp to mohawk and show that our tool analyzes ARBAC policies better than mohawk.

We use the dataset which was used to compare mohawk to other verification tools as shown in [9]. The dataset includes three test suites. The first one (called as Test suite 1) contains policies with positive conjunctive can_assign rules and non-empty can_revoke rules. The second one (called as Test suite 2) includes policies with mixed conjunctive can_assign rules and empty can_revoke rules while the last one (Test suite 3) contains policies with mixed conjunctive can_assign rules and non-empty can_revoke rules. For each policy in the test suites, we call asasp and mohawk 5 times with different safety queries and measure the average time taken for the verification process. All experiments were performed on an Intel Core 2 Duo T6600 (2.2 GHz) CPU, 2 GB Ram and Ubuntu 11.10.

Table 2. Experimental results for single queries

Table 2 describes the experimental results.

mohawk takes two stages to verify an ARBAC policy. In the first stage, it slices the original policy and then, in the second stage, the sliced policy is verified by the refinement steps. We consider that the time taken for the verification process is the sum of time consumed by these stages. The table shows that our tool answers the safety queries faster than mohawk in most cases. In other word, these experimental results demonstrate the effectiveness of our technique.

We also test our technique in verifying a sequence of safety queries. It means that asasp receives a set of safety queries, it verifies the first query and then the second query, and so on until the last query. We perform the verification of an ARBAC policy with a set of 8 different safety queries. Figure 4 shows that the time which asasp takes for verifying n-th query is smaller than the one of the previous verifications. The reason is that asasp reuses the states which have been visited in the previous verifications and hence, the time taken for the current verification may be reduced.

Fig. 4.

Experimental results for a sequence of queries

6 Conclusions, Related and Future Work

We have presented techniques to enable the MCMT framework to solve instances of user-role reachability problem. We have also designed a set of heuristics that help our analysis techniques to be more scalable. The main idea is to reduce as much as possible the number of administrative actions in the original problem and reuse the visited states of previous analysis processes. We have shown that the proposed techniques do not miss errors in buggy policies and performs significantly better than mohawk on the larger problem instances in [9]. As future work, we plan to consider the combination of backward and forward reachability procedure to speed up the analysis of the model checker.