Role based access control (RBAC) is a widely used approach to access control with well-known advantages in managing authorization policies. This paper considers user-role reachability analysis of administrative role based access control (ARBAC), which defines administrative roles and specifies how members of each administrative role can change the RBAC policy. Most existing works on user-role reachability analysis assume the separate administration restriction in ARBAC policies. While this restriction greatly simplifies the user-role reachability analysis, it also limits the expressiveness and applicability of ARBAC. In this paper, we consider analysis of ARBAC without the separate administration restriction and present new techniques to reduce the number of ARBAC rules and users considered during analysis. We also present parallel algorithms that speed up the analysis on multi-core systems. The experimental results show that our techniques significantly reduce the analysis time, making it practical to analyze ARBAC without separate administration.
Role based access control (RBAC) [1] is a widely used approach to access control with well-known advantages in performing authorization management. An RBAC policy is a tuple where U, R and P are finite sets of users, roles, and permissions, respectively, is the user-role assignment relation, and is the permission-role assignment relation. RBAC also supports role hierarchy: specifies that is senior to (or is junior to ), which implies that every member of is also a member of , and every permission assigned to is also available to members of .
Administrative role-based access control’97 (ARBAC’97) [17] defines administrative roles and specifies how members of each administrative role can change the RBAC policy. One part of ARBAC specifies user-role administration which controls changes to user-role assignments. The policy is expressed by two types of rules: (1) grants an administrative role permission to assign a target role to any user who satisfies the precondition c, and (2) grants an administrative role permission to revoke a target role from a user. The precondition c is a conjunction of literals, where each literal is either r (positive precondition) or (negative precondition) for some role r. A user satisfies a positive (negative) precondition if the user is (is not) a member of the role. A role is called an administrative role if it has an administrative permission, i.e., if it appears in the first component of a or a rule. ARBAC’97 requires separate administration [22], i.e., administrative roles cannot be target roles in can_assign and can_revoke rules or appear in preconditions. In the rest of this paper, we represent the precondition c as , where P contains all positive preconditions in c and N contains all negative preconditions in c.
The correctness of ARBAC policies is critical to system security, because any errors in ARBAC may result in violations of confidentiality or integrity. In large organizations with complex ARBAC policies, manual inspection of ARBAC policies for correctness can be impractical, because actions performed by different administrators may interfere with each other in subtle ways. Thus, automated analysis algorithms are essential to ensure that an ARBAC policy conforms to desired correctness properties.
This paper considers user-role reachability analysis of ARBAC [22], which asks queries of the form “given an RBAC policy ϕ, an ARBAC policy ψ, a set of users U, a target user , and a set of roles (called the “goal”), is it possible for users in to assign to all roles in the goal?”. Several other security analysis problems, such as user-role availability [16], role containment [16] and weakest precondition [22], can be reduced to this problem.
User-role reachability analysis is intractable even under various restrictions on the ARBAC policy [16,18]. Most existing research on user-role reachability analysis [8,9,14] follows the definition of ARBAC’97, which assumes separate administration. This prohibits an administrative role to serve as the target role in ARBAC rules, so it is sufficient to consider the user-role assignments of only the target user. However, in practice, the separate administration restriction does not always hold. For example, a university ARBAC policy may specify that the role can assign a member of role to role , which can in turn assign any user to role . Formally, this policy is expressed by rules and , which do not satisfy the separate administration restriction.
Analysis of ARBAC without separate administration is significantly more challenging, because it must consider administrative actions that change the role memberships of all users, not only the target user. For example, a non-target user u may assign another non-target user to an administrative role, which can in turn change the role assignments of the target user. Stoller et al. [22] tackled this problem by developing an algorithm that is fixed parameter tractable with respect to the numbers of users and mixed roles (i.e. roles that appear both negatively and positively in the policy). This means that the algorithm is exponential in the numbers of users and mixed roles, but is polynomial in the size of the policy when the numbers of users and mixed roles are fixed. Since the number of users is large in large organizations, and the algorithm is exponential in the number of users, the algorithm does not scale well. For example, we used the implementation in [22] to analyze a university ARBAC policy containing 150 users, and the program failed to terminate within 6 h for 4 out of the 8 randomly generated queries.
Contributions. This paper presents a number of reduction techniques that improve the scalability of the algorithm in [22]. Our main contributions are summarized below.
We propose two static reduction techniques – enhanced slicing (Section 3.1) and hierarchical rule reduction (Section 3.6) – to reduce the number of ARBAC rules considered during analysis.
We develop a user equivalent set reduction technique (Sections 3.3) and several involved-user reduction techniques (Section 3.4) to reduce the number of users considered during the analysis.
We propose two lazy reduction techniques – the subsumed-user reduction and the delayed revocation reduction – to delay performing unnecessary transitions (Section 3.5).
We present several parallel algorithms, which speed up the analysis on multi-core or multi-processor platforms (Section 4).
We evaluated the effectiveness of our reduction techniques and our parallel algorithms on an ARBAC policy for university administration. The experimental results show that our techniques significantly reduce the analysis time.
Organization. The rest of the paper is organized as follows. Section 2 describes the user-role reachability analysis algorithm for ARBAC without separate administration developed in [22]. Sections 3 and 4 present our reduction techniques and parallel algorithms, respectively. The experimental results are given in Section 5, followed by a discussion of related research in Section 6. Section 7 concludes the paper.
Preliminaries: User-role reachability analysis of ARBAC
User-role reachability queries are introduced in Section 1. Let be a set of all user-role assignments in the RBAC policy ϕ. The user-role reachability query is represented as a tuple .
Stoller et al. [22] presented an algorithm for analyzing ARBAC without separate administration, which is formalized in Algorithm 1. A role is negative if it appears negatively in some precondition in the policy; otherwise, it is non-negative. A role is positive if it appears in the goal, appears positively in some precondition in the policy, or is an administrative role; otherwise, it is non-positive. A role that is both negative and positive is a mixed role. Note that their algorithm applies to ARBAC without role hierarchy; role hierarchy can be eliminated using the algorithm in [18]. The algorithm works as follows.
The algorithm first performs a slicing transformation (function in Line 3), which back-chains along ARBAC rules to identify roles that are possibly useful for assigning to users. Such roles are preconditions and administrative roles, directly or indirectly (i.e., transitively), for assigning the target user to any goal roles. Lines 27–30 identify rules that are possibly useful for assigning those roles to users, add their positive preconditions to , and add their negative preconditions to .
Lines 31–34 identify possibly useful rules, i.e. rules that revoke roles in , and rules for assigning users to administrative roles in these rules. The algorithm then computes a set of all rules that are possibly useful for assigning the target user to any role in the goal; such rules are called “relevant rules”. includes all rules whose targets are in and all rules whose targets are in .
The user-role reachability analysis algorithm in [22]
Next, the algorithm constructs a reduced state graph G using rules in . Each state in G is a set of user-role assignments, and each transition describes an allowed change to the state defined by the ARBAC policy ψ. A transition is either which specifies that an administrative role adds user u to role r, or which specifies that an administrative role revokes user u from role r. The following reductions are applied: (1) Transitions that revoke non-negative roles (i.e., roles in ) or add non-positive roles (i.e., ) are prohibited because they do not enable any other transitions; (2) Transitions that add non-negative roles or revoke non-positive roles are invisible; such transitions will not disable any other transitions. Transitions that add or revoke mixed roles are visible. Invisible transitions together with a visible transition form a single composite transition.
The graph G is constructed as follows. First, the algorithm computes , which is the largest state that is reachable from by performing all invisible transitions enabled from (function in Line 3). The algorithm then computes a set of all states reachable from (Lines 5–21), and returns true iff there exists a state s in G such that (Lines 4, 11 and 18). The worst-case time complexity for constructing the graph is for some constant c, where is the number of mixed roles, is the number of users, and is the size of the policy [22].
A condition called the hierarchical role assignment (HRA) is defined in [22], under which analysis of ARBAC without separate administration can be reduced to analysis of ARBAC with separate administration. An ARBAC policy satisfies HRA if, for all where r is an administrative role, .
Consider the following ARBAC policy ψ, and the reachability query for this policy with the initial RBAC policy , the target user , the set of non-target users , and the goal .
1.
2.
3.
4.
5.
6.
7.
8.
This policy does not satisfy the separate administration restriction, because role is an administrative role in rule 2 and a target role in rule 4.
The graph illustrating the slicing process in Example 1.
First, the algorithm performs slicing to compute and . Initially, contains all roles in the goal, i.e. , and is empty. Figure 1 illustrates the slicing process. Each edge in the figure is labeled with the number of the rule applied during slicing. Roles in nodes without ¬ are positive preconditions or administrative roles of the rule applied; such roles are added to . Roles in nodes containing ¬ are negative preconditions of the rule applied; such roles are added to . The set of mixed roles is computed as . The algorithm then computes the set of rules that are useful for assigning the target user to any role in the goal. contains all rules whose target roles are in and rules whose target roles are in , i.e., rules 1, 2, 3, 4 and 7.
The state graph constructed in Example 1 using the algorithm in [22].
Next, the algorithm computes the initial state and all states reachable from using rules in . Because and , rule 3 is applied to assign to . Since is non-negative, is added to through an invisible transition. Because , , and is a mixed role, rule 1 is applied to assign to and through visible transitions and . Similarly, because and is a mixed role, rule 7 is applied to revoke from through a visible transition . The algorithm stops when no more transitions can be computed. The resulting graph appears in Fig. 2. Because the graph does not contain , the goal is not reachable.
Reduction techniques
The analysis algorithm described in Section 2 does not scale well for policies containing a large number of users. Let be a user-role reachability query. This section presents several techniques for reducing the numbers of users and ARBAC rules considered during analysis.
Enhanced slicing
This section presents an enhanced slicing algorithm to further reduce the number of roles and rules processed during slicing. Our enhanced slicing has the following features. First, because the target user needs to be assigned to all roles in the goal, while non-target users do not need to be assigned to any role in the goal, the enhanced slicing treats these two types of users differently. As a result, the size of the sliced policy for non-target users may be smaller than that for the target user. Second, our enhanced slicing for the target user eliminates rules whose negative preconditions contain an irrevocable role assigned to the target user in the initial policy, because such rules can never be enabled. Third, our enhanced slicing does not process non-negative and irrevocable administrative roles assigned to some user in the initial RBAC policy, because such roles can never be revoked and hence do not need to be reassigned to any user.
An enhanced slicing algorithm for the target user
Enhanced slicing for the target user. We say that a role r is irrevocable in an ARBAC policy if the policy does not contain a rule with target r. Algorithm 2 gives our enhanced slicing algorithm for the target user .
The algorithm first identifies roles that are possibly useful for assigning to . Such roles are preconditions and administrative roles, directly or indirectly, for assigning to any role in the goal. Lines 4–11 identify rules that are possibly useful for assigning those roles to , add their positive preconditions and administrative roles to , and add their negative preconditions to . The differences between our enhanced slicing algorithm and the slicing algorithm in [22] are: (1) if administrative roles or positive preconditions of the aforementioned rules are non-negative or irrevocable and have already been assigned to in the initial RBAC policy , then we do not add them to and do not process them during slicing. This is safe because such roles will not be revoked during analysis and hence there is no need to reassign them to (Lines 6 and 7); (2) for every aforementioned rule, we check if the negative precondition of the rule contains an irrevocable role assigned to in . If so, such a rule can never be enabled and hence will not be applied during slicing (Line 5).
Lines 12–17 identify rules that are possibly useful for assigning the target user to any role in the goal and rules that enable administrative roles of those rules. Such rules include rules that revoke roles in and rules that are possibly useful for assigning the target user to administrative roles of rules identified. Similar to rules, if administrative roles of rules identified above are non-negative or irrevocable and are already assigned to the target user, then we do not process such roles during slicing (Lines 14–15). In addition, since a negative role may become non-negative after slicing, to further reduce the number of relevant rules computed, we perform slicing multiple times until the set of all negative roles remains unchanged.
An enhanced slicing algorithm for non-target users
Enhanced slicing for non-target users. The algorithm tries to assign non-target users to administrative roles with permission to assign the target user to the goal, and to roles useful for that purpose. For example, consider the following ARBAC policy:
1.
2.
3.
When analyzing whether the target user can be assigned to all roles in the goal , it is not useful to assign non-target users to . As a result, it is not useful to assign non-target users to roles in the positive precondition of rule 1, i.e., and . Instead, it is sufficient to assign non-target users to the administrative role which has permission to assign to , and administrative role which has permission to assign to and (i.e., roles in the positive precondition of rule 1).
Algorithm 3 gives our enhanced slicing algorithm for non-target users. Lines 5–21 identify and rules that are possibly useful for assigning the target user to any role in the goal, add administrative roles of such rules to , and apply the slicing algorithm in [22] to process administrative roles. The differences between our enhanced slicing algorithm for non-target users and the slicing algorithm in [22] are: (1) our enhanced slicing algorithm does not add roles in the precondition of the aforementioned rules to since it is not necessary to assign such roles to non-target users; (2) if administrative roles of the aforementioned rules identified above are non-negative or irrevocable and have already been assigned to some user in the initial RBAC policy , then we do not add them to and do not process them during slicing (Lines 7 and 8); (3) for each of the aforementioned rules, if the negative precondition of the rule contains an irrevocable role assigned to the target user in , then such a rule can never be enabled and hence will not be applied during slicing (Line 6).
Two-stage slicing. While computing the initial state using the sliced policy, non-negative administrative roles that are not in the initial RBAC policy may be added to the initial state through invisible transitions. It is unnecessary to assign such roles to other non-target users during analysis if they do not appear in the positive precondition of the sliced policy. To further reduce the number of rules applied during the analysis, we apply the enhanced slicing algorithm twice: before and after computing the initial state. Our experiments on a university policy show that the two-stage slicing sometimes significantly reduces the number of relevant rules computed.
Consider Example 1. Figure 3 illustrates the enhanced slicing for the target user. The enhanced slicing is performed from role (i.e., the role in the goal). Since is the target role of rule 2, roles in the positive precondition of rule 2, i.e., and , are added to . Since the administrative role of rule 2 is a non-negative role and , is not processed during slicing. The algorithm then performs enhanced slicing for the target user from and , adds and to , and adds to . Therefore, for the target user, , , and . Next, the algorithm performs enhanced slicing for non-target users. It is sufficient to assign non-target users to administrative roles that have permissions to assign the target user to the goal, i.e., and . Since and are non-negative, , and , these roles are not processed during slicing. As a result, for non-target users, and . This means that there is no need to assign roles to non-target users. The reduced state graph constructed with the enhanced slicing algorithm contains only one state .
The graph illustrating the enhanced slicing for the target user in Example 2.
Dead-role reduction
We say that a role r is dead if r is not assigned to any user in the initial RBAC policy and cannot be assigned to any user during the analysis. Our dead-role reduction aims to eliminate rules that are not useful for reaching the goal because they involve dead roles. The reduction first computes a set of roles that are not target roles of any rule and are not assigned to any user in ; such roles are dead. Next, the reduction eliminates and rules whose administrative roles are in , and rules whose positive preconditions are in , because such rules are never enabled. This process is repeated until no rules can be eliminated. The dead-role reduction may turn negative roles to non-negative, and hence may reduce the size of the state graph.
User equivalent set reduction
In this section, we show that from each state it is sufficient to perform visible transitions for the target user and for non-target users assigned distinct sets of roles. Our technique is based on a notion of user equivalent set. The user equivalent set representation of a state s is basically an alternative representation of s, in which all users assigned the same set of roles are grouped together.
The user equivalent set representation of a state s is defined as where , , and for every , .
Let be the transition graph constructed using the user equivalent set representation. There is a transition in if and only if there is a transition in G. The goal is reachable in if and only if there exists a state and such that and .
Our user equivalent set reduction works as follows. For every state s and every , we compute only transitions for the target user and transitions for one randomly selected non-target user in , if contains such users. This is different from Algorithm 1, which computes transitions for all users in . Intuitively, the user equivalent set reduction is correct because transitions performed on all users in are the same, and transitions performed on one user in do not disable transitions performed on other users in . We use to denote the transition graph constructed with the user equivalent set reduction.
Given two states and , we say that if there exists a substitution , where and , such that . Theorem 2 formalizes the correctness of the reduction. We prove a lemma and then Theorem 2.
Letbe a user-role reachability query,, andandbe reduced state graphs constructed for Q with and without the user equivalent set reduction, respectively. (a) For every sequence of transitionsin, there exists a sequence of transitionsin, where,,,, and there existandsuch that,, and. (b) For every sequence of transitionsin, there exists a sequence of transitionsin.
We prove part (a) by induction on the length n.
Base case: When , both and contain only one state . The lemma holds.
Induction: Assume that the lemma holds when . We prove the lemma for .
Let be a sequence of transitions in . By the induction hypothesis, contains a sequence of transitions , where , , , , and there exist and such that , , and .
If , then there exists such that . Because , there exists such that and . Therefore, contains transition and . If where , then there exists such that . Because , there exists such that . Let be a user in . Because and are assigned the same set of roles, we can perform transition and . The case where can be similarly proved. Thus, part (a) holds.
Part (b) holds because is a subgraph of . □
Letbe a user-role reachability query, andandbe reduced state graphs constructed for Q with and without the user equivalent set reduction, respectively. The goal is reachable iniff the goal is reachable in.
Suppose the goal is reachable in . Then there exists a sequence of transitions in such that , , and . From Lemma 1(a), there exists a sequence of transitions in where , , , , and there exist and such that , , and . Because , there exists such that and . As a result, and hence the goal is reachable in .
Suppose contains a goal state . Then from Lemma 1(b), is also a state in and hence the goal is reachable. Therefore, the theorem holds. □
Consider the user-role reachability query in Example 1. Since non-target users and are assigned the same set of roles in the initial state, the algorithm with user equivalent set reduction performs only transitions for or , but not both, from the initial state. In contrast, Algorithm 1 performs transitions for both and from the initial state. The graph constructed with the user equivalent set reduction is given in Fig. 4.
The state graph constructed in Example 3 with the user equivalent set reduction.
User-counter optimization. In our implementation, we reduce the size of states by replacing in with a pair , where records the number of non-target users in , and is either 1 (indicating ) or 0 (indicating ). This optimization may significantly reduce the size of states if many users are assigned the same set of roles. For example, in a university, thousands of users may be assigned the Student role.
Consider the user-role reachability query in Example 1 with an extended RBAC policy that assigns and to , and to and , and to .
Without the user-counter optimization, the initial state is , and the following two transitions are enabled from the initial state: , and .
With the user-counter optimization, the initial state is , which specifies that 998 non-target users are assigned roles and , 2 non-target users are assigned roles and , and 1 target user is assigned role . The following two transitions are enabled from the initial state: , where in the transition specifies that the user is a non-target/target user.
Involved-user reduction
In Theorem 1 of [5], Ferrari et al. prove that, given a query, if the goal is reachable, then there exists a run (i.e. a finite sequence of transitions) in which the goal is reachable and at most users change their role-combinations, where is a set of administrative roles in the ARBAC policy and a role combination is the set of roles assigned to a user (we call it a role set). Based on this theorem, they propose to keep in the system at most users for each role set during analysis. In this section, we present three user-oriented reductions – static involved-user, spare-user, and dynamic involved-user reductions – that extend their work to further reduce the number of users considered during the analysis. The static involved-user reduction is performed prior to the construction of the state graph, the spare-user reduction is similar to the static involved-user reduction, except that it limits the number of non-target users in every state, not only the initial state, and the dynamic involved-user reduction is performed during the generation of the state graph.
Static involved-user reduction. Our static involved-user reduction improves the reduction in [5] by computing a separate and sometimes smaller bound on the number of users needed for each role set (equivalently, for each set of roles in the user equivalent set representation) in the initial state, instead of a single bound that applies to all role sets in the initial state.
Let be a role set and be an upper-bound on the set of roles that can be assigned to users whose initial role set is . Formally, is defined as , where returns the least fixed-point of f. Our reduction states that the number of non-target users for each role set in the initial state can be limited to , which is an upper-bound on the number of administrative roles that can be assigned to users with role set . We state a lemma and then prove the correctness of this reduction.
Letbe a role set. For every user u with the initial role set, the set of roles assigned to u is always a subset of.
(Static involved-user reduction).
Letbe a user-role reachability query,be a set of user-role assignments obtained fromby reducing the number of users associated with each role set RS to,, and. (a) If the goal is reachable in Q, then the goal is reachable in; (b) If the goal is reachable in, then the goal is reachable in Q.
Part (a) is proved based on the proof of Theorem 1 in [5] and Lemma 3.1. Let G and be the reduced state graph constructed for Q and , respectively. A user u is involved in a sequence of transitions T if u’s role set changes in T. A user u is essential in a sequence of transitions T if there exists in T such that u is the only user in assigned the administrative role in .
First, we show that, for every sequence of transitions T in G that contains a goal state, there exists a sequence of transitions in G that contains a goal state, and at most non-target users in each role set RS are involved in . is constructed as follows. If T contains at least one involved non-target user that is not essential, then we pick one such user u and remove from T all transitions that change u’s role set. If all non-target users in T are essential, then we pick one such user u and remove all transitions that both change u’s role set and are performed after the last state in which u is essential. The above process is repeated on the resulting sequence of transitions until no more transitions can be eliminated, which results in . Because the above construction keeps in each state one user among those assigned an administrative role, the eliminated transitions do not disable transitions in . Therefore, is a sequence of transitions in G. Because all users in are essential and for each user u with the initial role set , the set of roles assigned to u is always a subset of (Lemma 3.1), at most non-target users with initial role set change their role sets in . contains a goal state because the above construction does not eliminate transitions performed on the target user.
Next, we construct a sequence of transitions from such that is a sequence of transitions in , and contains a goal state. We first remove all users that are not involved in from all states in , which results in . Let where . is constructed as , where σ is a mapping between users in and users in defined below: if is in ; otherwise, where and for all . Since contains at most non-target users in each role set RS in , the above mapping is always possible. Therefore, if the goal is reachable in Q, then the goal is reachable in .
Part (b) follows directly from the fact that is obtained from by reducing the number of users associated with each role set to . □
The static involved-user reduction can be improved by not considering administrative roles in that are non-negative or irrevocable, i.e., limiting the number of non-target users with role set RS to . Such roles will not be revoked during the analysis and hence do not need to be reassigned to non-target users.
Consider the user-role reachability query in Example 1. Our static involved-user reduction works as follows. The set of administrative roles in the ARBAC policy is . The non-target user is initially assigned role set . The policy does not contain a rule such that , so and hence . This means that we need to keep in the initial state. Non-target users and are initially assigned role set . Because the precondition of the first rule is a subset of , the rule’s target is a descendant. As a result, and . This means that we need to keep either or , but not both, in the initial state. Assume that we keep in the initial state. The state graph constructed with the static involved-user reduction is given in Fig. 5.
The state graph constructed in Example 5 with the static involved-user reduction.
Spare-user reduction. The spare-user reduction is similar to the static involved-user reduction, except that it limits the number of non-target users in every state, not only the initial state. Intuitively, the spare-user reduction should perform the same or better than the static involved-user reduction, since fewer or the same number of users are considered during the analysis. Our experimental results on a university RBAC and a university ARBAC policy show that this is true for most cases. However, in some cases, the spare-user reduction increases the numbers of states and transitions. For example, if a state s has been processed before a transition , then removing spare users from may result in a different target state that, without the spare user reduction, might never be processed. In this case, the reduction could increase the size of the state graph.
Dynamic involved-user reduction. The dynamic involved-user reduction limits the number of users whose role sets change in each explored path in the state graph. The algorithm performs a depth-first search (DFS) to check whether the goal is reachable. During the DFS, it keeps track of the number of users that change role sets (we call such users “involved users”) in the run corresponding to the DFS stack. When the number of users involved in the run on the stack is greater than , the algorithm explores only transitions which change role sets of users that are already involved in the trace.
Note that the above algorithm counts users that change role sets only in visible transitions. Informally, it would be unsound to also count users that change role sets in invisible transitions, because our algorithm always executes invisible transitions as soon as possible, but the invisible transitions do not necessarily appear in the paths in the full state graph (i.e., the graph without the invisible transition reduction) that reach the goal with the minimal number of involved users.
The dynamic involved-user reduction is partly incompatible with the user-count optimization in Section 3.3. With the user-count optimization, the algorithm does not keep track of identities of the users, which makes it hard to keep track of how many users changed role sets. One solution is to introduce identities for users on demand; we call this the partial user-count reduction. It works as follows. A state s is a set of tuples of the form , where Anon is the number of anonymous users with role set , and is the set of named users with role set . The target user is never anonymous. Thus, has role set iff . In every state, the algorithm computes transitions only for the named users and one anonymous user; the anonymous user becomes named in the target state of the transition. The name is chosen to be , where i is the smallest i such that does not appear in .
On one hand, the dynamic involved-user reduction may generate smaller state graphs than the other two reductions presented in this section. On the other hand, tracking the involvement of users in the dynamic involved-user reduction imposes additional performance overhead and is partly incompatible with the user-count optimization. As a result, the performance of the dynamic involved-user reduction might or might not be better than other two reductions. In addition, the dynamic involved-user reduction is incompatible with the current implementation, which uses bread-first search. Consequently, we did not implement this reduction.
Consider a user-role reachability query which is the same as that in Example 1, except that all administrative roles in the ARBAC policy are replaced with . Without any reduction, the state graph is the same as that in Fig. 2. Because , . Therefore, with the dynamic involved-user reduction, the number of users that change role sets in each path of the state graph is limited to 2. Figure 6 gives the state graph constructed with the dynamic involved-user reduction.
As a small example of a query for which the dynamic involved-user reduction is more effective than the static involved-user reduction, consider a user-role reachability query which is the same as that in Example 1, except that all administrative roles in the ARBAC policy are replaced with , is assigned only (instead of both and ), and the ARBAC policy contains one more rule . With no reduction, there are 8 states. The static involved user reduction does not eliminate any states because the number of users associated with each role set in the initial RBAC policy is 1 and for each role set , . The dynamic involved user reduction reduces the number of states to 7.
The state graph constructed with the dynamic involved-user reduction.
Lazy reduction
This section describes two lazy reduction techniques that reduce the size of the state graph by delaying transitions.
Subsumed-user reduction. Let . The subsumed-user reduction works as follows. Given a state s, for every non-target user u, if there exists a user other than u such that (1) and (2) (i.e. all roles in are non-negative), then we do not perform transitions on u from s. Such transitions will be performed later when one of the above conditions does not hold.
Intuitively, this reduction is sound because every transition enabled on u in s is also enabled on in s (since non-negative roles do not disable any transitions), and transitions performed on do not disable transitions enabled on u.
Given states s and , we say that is a superstate of s, denoted as , if , and for every non-target user u in s, there exists a non-target user in such that and . For example, if is a non-negative role, then .
Below, we prove one lemma and then the correctness of the reduction.
Letbe a user-role reachability query,, andand G be reduced state graphs constructed for Q with and without the subsumed-user reduction, respectively. (a) For every sequence of transitionsin, there exists a sequence of transitionsin G. (b) For every sequence of transitionsin G, there exists a sequence of transitionsin, such that.
Part (a) follows from the fact that, in every state, the algorithm with the subsumed user reduction explores a subset of the enabled transitions.
The proof of part (b) is by induction on n.
Base case: When , both G and contain only state . Therefore, the lemma holds.
Induction hypothesis: Assume that the lemma holds for , i.e., for every sequence of transitions in G, there exists a sequence of transitions in such that . We now prove the lemma for . Assume that there is a transition in G. If , then because , and contains all administrative roles in . Therefore, contains a transition such that . Otherwise, since for every non-target user u in , there exists a non-target user in such that and , contains a transition such that . The case where the transition is a transition can be similarly proved. Therefore, part (b) holds. □
Letbe a user-role reachability query,, andand G be reduced state graphs constructed for Q with and without the subsumed-user reduction, respectively. The goal is reachable in G iff the goal is reachable in.
The “if” part follows immediately from part (a) of Lemma 3.
The state graph constructed in Example 8: (a) without the subsumed-user reduction, (b) with the subsumed-user reduction.
Next, we prove the “only if” part. Suppose G contains a sequence of transitions , such that . From part (b) of Lemma 3, contains a sequence of transitions , such that . The latter implies and hence . □
Consider Example 1, except with the initial RBAC policy . Figure 7(a) and (b) give the state graph computed without and with the subsumed-user reduction, respectively. In the initial state, the role sets of and are and , respectively, and , , and are non-negative roles. Therefore, with the subsumed-user reduction, the algorithm does not compute transitions for from the initial state. Similarly, is not performed from state and is not performed from state .
Delayed revocation. A transition can be delayed if the transition can neither enable new transitions in s nor be disabled by any transitions. Formally, a transition is not performed from s (i.e. is delayed) if
∪ , where and are sets of all visible transitions enabled from s and , respectively,
,
contains at least one transition, and
is non-negative or irrevocable.
Conditions 1 and 2 specify that does not enable new visible and invisible transitions, respectively. Conditions 3 and 4 specify that cannot be disabled by other transitions. Requiring to contain at least one transition ensures that not all transitions from s will be delayed, which in turn ensures that the delayed transitions can be executed later. This condition can be relaxed by not delaying one transition that is enabled in s, if no transitions are enabled in s.
The correctness of the delayed revocation reduction is formalized in Theorem 6. We prove one lemma and then Theorem 6. Let ⊑ denote the subsequence notation.
Letbe a user-role reachability query,, andand G be reduced state graphs constructed for Q with and without the delayed revocation reduction, respectively. (a) For every sequence of transitionsin G, there exists a sequence of transitionsinsuch that, and. (b) For every sequence of transitionsin, there exists a sequence of transitionsin G.
Part (a) is proved by induction on the length n.
Base case: If n = 0, then both G and comprise only one state . The lemma holds.
Induction: Assume the lemma holds for . Below, we prove the lemma for . Suppose there is a sequence of transitions in G. By the induction hypothesis, there is a sequence of transitions in such that , and .
First, we consider the case where is not a delayed transition in . Since at least one transition is enabled from s and is non-negative or irrevocable, delayed transitions do not disable . In addition, differs from only by containing user-role pairs removed from by delayed transitions. As a result, transition can be executed where . If is a delayed transition in , then .
Part (b) follows from the fact that is a subgraph of G. Thus, the lemma holds. □
Letbe a user-role reachability query,, andand G be reduced state graphs constructed for Q with and without the delayed revocation reduction, respectively. The goal is reachable in G iff the goal is reachable in.
If the goal is reachable in G, then there exists a sequence of transitions in G such that . From Lemma 5(a), there exists a sequence of transitions in such that , so . Thus, the goal is reachable in .
If contains state such that , then from Lemma 5(b), is also in G and hence the goal is reachable. Therefore, the theorem holds. □
Consider the user-role reachability query in Example 1. Since the transition does not enable new transitions from the initial state and is non-negative, with delayed revocation reduction, this transition is not performed from the initial state. Similarly, is also not performed from state and state . The graph constructed with the delayed revocation reduction is given in Fig. 8.
Hierarchical rule reduction
Hierarchical rule reduction avoids considering rules whose administrative roles are junior to non-negative or irrevocable administrative roles in . Formally, the hierarchical rule reduction eliminates rules such that there exists such that and is non-negative or irrevocable. This is safe because senior roles inherit all administrative permissions of their junior roles, and non-negative/irrevocable roles are never revoked during analysis. Note that, the hierarchical rule reduction does not reduce the size of the transition graph, but may reduce the analysis time, since fewer rules are applied during analysis.
The state graph constructed in Example 9 with the delayed revocation reduction.
Consider the user-role reachability analysis query in Example 1 with the role hierarchy . The following three rules are added when the policy is transformed into a non-hierarchical policy: , , and . Since is a non-negative role, will never be revoked during analysis. As a result, rules 4 and 5 in Example 1 are not necessary for reaching the goal (since administrative roles of these two rules are , which is junior to ), and hence will not be applied during analysis with this reduction.
Integrating all reductions
Integrating all reductions needs to be done carefully to achieve the best performance, since the order of the reductions may significantly affect the performance of the algorithm. Let be a user-role reachability query. Algorithm 4 describes the integration process.
Integrating all reductions
Perform the dead role analysis to eliminate ARBAC rules involving dead roles (line 2) and store the rest of rules in .
Perform the enhanced slicing (lines 3–4) on , and store the sliced policies for the target user and non-target users in and , respectively. The order of steps 1 and 2 is not significant.
Compute the initial state from the initial RBAC policy ; invisible transitions for the target user are computed using rules in and invisible transitions for non-target users are computed using rules in (line 5). Note: this step is performed after steps 1 and 2, because steps 1 and 2 reduce the number of rules applied to compute the initial state and hence may reduce the size of the initial state.
Perform the second-stage slicing on and , and store the sliced policies for the target user and non-target users in and , respectively (lines 6–7). Note: this step is performed after step 3 because it depends on computed in step 3.
Perform the hierarchical rule reduction on and , and store the resulting policies in and (line 8). Note: this step is performed after steps 1–4, because a negative administrative role in the original policy may become non-negative after dead role analysis and two-stage slicing, which may improve the effectiveness of the hierarchical rule reduction.
Perform the static involved user reduction (line 9) to keep in the system the target user and at most non-target users for each role set, where is the set of administrative roles that may possibly be assigned to non-target users during analysis, computed as the intersection of administrative roles in and target roles in . Note: step 6 is performed after steps 1–5, because steps 1–5 may reduce the number of rules considered and hence may reduce the number of roles in .
During the analysis, for every state s and every user equivalent set in s, apply the subsumed-user reduction to check whether s contains a user equivalent set such that and contains only non-negative roles (function ). If so, do not explore transitions for users in ; otherwise, explore transitions from s for users in using the user equivalent set reduction (lines 10–18).
Note that, even if the enhanced slicing alone reduces the number of states and transitions computed, integrating the enhanced slicing and the user-equivalent set reduction does not always reduce the number of states and transitions. This is because, sometimes, when fewer roles are assigned to users, the state may contain more user equivalent sets. In our experiments, the integration reduces the number of states and transitions for most policies, but increases the number of states and transitions for a few policies.
Parallel version of user-role reachability analysis algorithm in [22]
Multi-core processors are becoming pervasive. To benefit from this, it is important to parallelize algorithms. This section modifies the algorithm from [22] (Algorithm 1 in this paper) to perform analysis in parallel. The basic idea is to create multiple threads, each of which repeatedly removes and processes states from the workset. Since more than one thread may access the workset and the set of processed states concurrently, we explored techniques to efficiently synchronize and reduce contention on these two sets. Pseudocode for the parallel algorithm is given in Algorithm 5.
First, we perform slicing to eliminate irrelevant roles, as we do in Algorithm 1. We then compute the initial state of the transition graph and add to a workset W (Line 5). Next, we create n threads (Line 6; represents the concurrent execution of threads). Typically, n is greater than the number of cores in order to keep all cores busy. Finally, each thread removes one state from the workset W, computes transitions enabled from the state using Lines 7–10 and 14–17 of Algorithm 1, and adds the target states to W and the set of reachable states if the target states are not already in (Lines 11–21). Since multiple threads may access concurrently, synchronization is needed to prevent interference between concurrent accesses. To reduce contention on , we implemented as a hashtable with a separate lock for each bucket (i.e. each collision chain), shown in Fig. 9. As usual, stores a set of states whose hash values are h. After a thread computes a transition , it computes the hash value of , locks , adds to if is not already in , and unlocks . Our experimental results show that locking each bucket instead of the entire hashtable significantly improves the performance, because threads access very frequently and checking whether a state is in is relatively expensive. The algorithm terminates if the goal is reached, or if W is empty and all threads are not performing any computation.
To reduce contention on the workset W, we modify the algorithm so that each thread has its own workset. Below, we present three approaches to synchronization for the workset.
NoLock: In this approach, a thread never accesses other threads’ worksets. Every time a thread computes a transition, it stores the target state in its own workset, if the target state is not already in . This approach eliminates all locking for worksets, but may result in idle threads (due to empty worksets).
FullLock: In this approach, a thread t is allowed to access other threads’ worksets to remove a state to process, if t’s workset is empty. The thread t will access other threads’ worksets one by one until it finds a non-empty workset, when it removes one or more states from the workset. This approach provides better load balancing, but it requires locking the workset every time it is accessed. A challenge is to decide how many states a thread should remove from another thread’s workset at a time. If a thread takes one state at a time, then the thread is likely to run out of work again relatively soon. Another approach is to take a fixed fraction of the states in the workset. In our implementation, we pick states, where is the size of the workset and is a user-specified bound.
PartialLock: In this approach, after a thread computes a fixed number of transitions, it checks if thread is idle. If so, it locks the workset of thread , adds the target state to the workset, unlocks the workset, and starts thread . The advantage of this approach is that locking is needed only when thread adds a state to thread ’s workset. A challenge is to decide how many transitions a thread should compute before it checks if a thread is idle. If the number is small, then each thread has to frequently check if is idle. If the number is large, then a thread may be idle for long time.
Other designs. It may be possible to improve performance by replacing mutual exclusion locks on buckets in with reader–writer locks. However, our experiments show that this does not yield performance improvement. In fact, it often causes performance degradation, because multiple threads rarely access the same bucket simultaneously, and reader–writer locks, due to their complexity, incur greater overhead than mutual exclusion locks.
We also considered using a lock-free data structure to implement the workset. To evaluate the potential benefit of this approach, we measured the overhead of the mutual exclusion lock by comparing running times of one thread with and without locking. Our experimental results show that locking incurs negligible overhead. This implies that a lock-free data structure would not appreciably improve the performance.
Performance results
This section evaluates the effectiveness of our reduction techniques and parallel algorithms using the university ARBAC policy developed in [22] and the university RBAC policy developed in [7].
The university RBAC and ARBAC policies contain 845 users, 32 roles (including 13 administrative roles), 329 rules, and 78 rules, after being converted to the corresponding non-hierarchical policies. The policies include rules for assignment of users to various student and employee roles. Student roles include undergraduate student, graduate student, teaching assistant, research assistant, honors student, etc. Employee roles include president, provost, dean, department chair, faculty, honors program director, etc. A sample rule is: the honors program director can assign an undergraduate student to the honors student role. A sample user-role reachability query is: can a user who is a member of the department chair role and a user who is a member of the undergraduate student role assign the latter user to the honors student role? Details of the university ARBAC policy are available from [21].
The university ARBAC policy does not satisfy the separate administration restriction. In addition, the policy has hierarchical role assignment w.r.t. all administrative roles except those for assigning users to roles “honors student” and “graduate student”. This means that if the goal contains these two roles, then we cannot directly apply the algorithm for analyzing ARBAC with separate administration to carry out analysis. In our experiments, we randomly select one target user , one role r, and n non-target users . We then apply analysis algorithms to check whether users in together can assign to both honors student role and role r.
Each data point reported in this section is an average over 8 randomly generated queries. These 8 queries were generated as follows. First, we randomly generated 100 queries. Next, we ran the analysis program without reduction for the university policy containing 50 users and chose the first 8 policies in which the program generated at least 30 states. This eliminates very easy queries. The sets of non-target users were generated incrementally, so that each set of non-target users is a superset of the sets of non-target users generated for smaller n.
Experimental results of NoReduct and four least effective reductions; error bars indicate that the reported average is a lower bound on the actual average. (Colors are visible in the online version of the article; https://dx-doi-org.web.bisu.edu.cn/10.3233/JCS-140511.)
Experimental results of NoReduct and four most effective reductions; error bars indicate that the reported average is a lower bound on the actual average. (Colors are visible in the online version of the article; https://dx-doi-org.web.bisu.edu.cn/10.3233/JCS-140511.)
Effectiveness of reduction techniques. Figure 10(a)–(d) report the number of states, the number of transitions, the execution time, and the number of timeout policies (i.e., policies for which the analysis does not complete within 5 h) for the program without reduction (NoReduct) and with each of the four least effective reductions: the dead-role reduction (DeadRole), the delayed revocation reduction (DelayedRev), the subsumed-user reduction (Subsumed), and the static involved-user reduction (Involved). Figure 11 reports the same for NoReduct and the five most effective reductions: the enhanced slicing (EnhancedSlicing), the user equivalent set reduction (UserEquiv), the spare-user reduction (Spare), all reductions in [24] (AllReduct in [24]) and all reductions in this paper (AllReduct). The reported data were obtained on a 2.5 GHz Pentium machine with 4 GB RAM running Ubuntu 12.04.
In our experiments, a run terminates as soon as the goal is reached (when the analysis result is true) or no more transitions can be computed (when the analysis result is false). We do not include the hierarchical rule reduction in the figures as this reduction itself is not effective in our experiments, because all administrative roles in the university ARBAC policy that have junior roles are mixed roles. In addition, the static involved-user reduction and the spare-user reduction cannot be applied together. AllReduct in Fig. 11 uses the static involved-user reduction, which generates slightly fewer states and transitions than using the spare-user reduction for the reason given in Section 3.4.
The timeout threshold in our experiments is 5 h. If a run on a particular query does not terminate in 5 h, then we use the smallest number of states and transitions that had been explored when the timeout occurred in the computation of the average numbers of states and transitions explored for the current set of queries (corresponding to a given number of users and combination of reductions). Thus, in those cases, the reported averages are lower bounds on the actual averages that would have been obtained if we let the program always run to completion. In Figs 10 and 11, we use the error bar to indicate that the reported average is a lower bound on the actual average. For example, we see from Figs 10(d) and 11(d) that, when the number of users is 200 or more, all variants except AllReduct timeout for 1 to 5 out of 8 policies.
While all reductions improve the performance, their effectiveness varies for different queries. The user equivalent set reduction performs the best for most policies and the subsumed-user reduction is the least effective (effective for only 75 and 100 users). Our experimental results also show that, although the static involved-user reduction does not reduce the number of states and transitions for 50 users, the execution time is less, because no transitions are performed on users who are eliminated. In addition, applying the spare-user reduction alone is more effective than applying the static involved-user reduction alone.
Note that the execution time of most variants for 400 users is smaller than that for 300 users. This is because the newly added users enable new transitions, which turns the analysis result for one of the 8 policies from “false” to ”true” and the program terminates as soon as the goal is reached. For the same reason, the execution time of most variants for 500 users is smaller than that for 400 users, and the execution time for 700 users is smaller than that for 600 users.
Integrating all reductions leads to a very effective solution. When the problem becomes difficult for the baseline algorithm to solve, AllReduct achieves an improvement of four orders of magnitude in execution time and terminates in all experiments. Our experimental results also show that AllReduct performs slightly better than Allreduct in [24] for 50–150 users and performs significantly better than Allreduct in [24] for 200–800 users. Further, integrating the two-stage slicing with the spare-user reduction reduces the number of administrative roles that need to be assigned to non-target users during analysis from 13 to 2–4.
Execution time of parallel algorithms.
Performance results of parallel algorithms. Figure 12 gives the execution time of our parallel analysis algorithms without reductions – SharedWorkset (Algorithm 5), NoLock, PartialLock(1), PartialLock(50), FullLock(1), and FullLock(5) – with 15 and 30 threads. FullLock(n) represents FullLock with the user-specified bound n. PartialLock(n) represents PartialLock in which a thread checks whether its neighbor is idle after computing every n transitions. The number atop each bar is the speedup of the corresponding parallel algorithm over the sequential algorithm. For example, Fig. 12(a) shows that, with 50 users and 15 threads, SharedWorkset is 2.9 times faster than the sequential algorithm. Each the reported data were obtained on a computer with two 2.4 GHz Quad-Core AMD Opteron Processors and 16 GB RAM running Ubuntu 3.2.0. A 32-bit Ubuntu kernel was installed, so each process is limited to access only 4 GB memory.
On average, FullLock performs the best, followed by PartialLock, NoLock, and SharedWorkset. The running times of FullLock(1) and FullLock(5) are almost the same. PartialLock(50) performs slightly better than PartialLock(1) for 50 and 75 users, but slightly worse for 100 users. FullLock and SharedWorkset with 30 threads outperform those with 15 threads, because the threads often wait for locks to access worksets in FullLock and SharedWorkset, and hence more CPU cores are utilized with 30 threads than 15 threads. The running times of NoLock and PartialLock with 15 threads are close to those with 30 threads.
We have also measured the total number of times a thread accesses other threads’ workset in FullLock. Our experimental results show that with 15 threads, the number of accesses to other threads’ worksets is significantly less than that with 30 threads (by a factor of 64.65–83.59%). This is because, with fewer threads, there are more states in each workset and hence the chance that the workset becomes empty is smaller. Our experimental results also show that, with 30 threads, allowing a thread to take more than one state significantly reduces the average number of accesses to other threads’ worksets (reduced by 4.97–64.39%), but does not have a significant effect on the running time. This indicates that only a small fraction of the total execution time is spent in accessing other threads’ worksets.
Related work
A number of researchers have studied user-role reachability analysis of ARBAC. Schaad et al. [19] applied the Alloy analyzer [12] to check the separation of duty properties for ARBAC97; they did not consider preconditions for any operations. Li et al. [16] presented algorithms and complexity results for various analysis problems for two restricted versions of ARBAC97, called AATU and AAR; they did not consider negative preconditions. Jayaraman et al. [14] presented an abstraction refinement mechanism for detecting errors in ARBAC policies. Alberti et al. [2] developed a symbolic backward algorithm for analyzing Administrative Attribute-based RBAC policies, in which the policy and the query are encoded into a Bernays–Shonfinkel–Ramsey first order logic formulas. Becker [3] proposed a language DYNPAL for specifying dynamic authorization policies, which is more expressive than ARBAC, and presented techniques for analyzing DYNPAL. Sasturkar et al. [18] showed that user-role reachability analysis of ARBAC is PSPACE-complete, and presented algorithms and complexity results for ARBAC analysis subject to a variety of restrictions. Stoller et al. [20] presented algorithms for analyzing parameterized ARBAC. Gofman et al. [9] presented algorithms for analyzing evolving ARBAC. Uzun et al. [23] developed algorithms for analyzing temporal role-based access control models. However, none of the above works consider analysis of ARBAC without separate administration.
Several researchers have considered analysis of ARBAC without separate administration. Stoller et al. [22] provided fixed-parameter tractable algorithms for ARBAC with and without the separate administration restriction. Their algorithm for analyzing ARBAC without separate administration is exponential in the number of users in the policy, which is usually large in practice. Our work significantly improves the scalability of their algorithm by reducing the number of ARBAC rules and users considered during analysis. Ferrara et al. [4] converted ARBAC policies to imperative programs and applied abstract-interpretation techniques to analyze the converted programs. However, if the goal is reachable, their approach cannot produce a trace which shows how the goal is reachable. Later, the same authors showed that if the goal is reachable in an ARBAC policy, then there exists a run of S with at most users in which the goal is reachable [5]. In this paper, we present three reductions that extend their work to further reduce the number of users considered during the analysis; our other reductions are different from their. In addition, none of the above works present parallel analysis algorithms.
A number of researchers considered analysis of fixed security policy [10,11,13,15], analysis of a single change to a fixed policy, or analysis of differences between two fixed policies [6,15]. However, none of these works consider analysis of ARBAC.
Conclusion and future work
This paper considers user-role reachability analysis without the separate administration restriction, which was shown to be PSPACE-complete in general. We present new analysis techniques with the goal of finding an efficient solution to the problem. Our techniques focus on reducing the number of ARBAC rules and users considered during analysis and delaying unnecessary computations. We also present parallel algorithms that speed up the analysis on multi-core systems. Experiments with a university ARBAC policy show that our techniques significantly reduce the analysis time. In the future, we plan to develop symbolic analysis algorithms to implicitly search the state space with a potential to further improve the performance of the analysis.
Footnotes
Acknowledgments
This work was supported in part by NSF Grants CNS-0855204 and CNS-0831298. We thank Kyoung-Don Kang for providing feedback on parallel algorithms and Dulcinea Chau for her contribution to the implementation of parallel algorithms.
References
1.
A.N.S.I. (ANSI), Role-based access control, ANSI INCITS Standard 359-2004, February 2004.
2.
F.Alberti, A.Armando and S.Ranise, Efficient symbolic automated analysis of administrative attribute-based RBAC-policies, in: ACM Symposium on Information, Computer and Communications Security, 2011, pp. 165–175.
3.
M.Y.Becker, Specification and analysis of dynamic authorisation policies, in: 22nd IEEE Computer Security Foundations Symposium (CSF), 2009, pp. 203–217.
4.
A.L.Ferrara, P.Madhusudan and G.Parlato, Security analysis of role-based access control through program verification, in: IEEE Computer Security Foundations Symposium (CSF), 2012, pp. 113–125.
5.
A.L.Ferrara, P.Madhusudan and G.Parlato, Policy analysis for self-administrated role-based access control, in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2013, pp. 432–447.
6.
K.Fisler, S.Krishnamurthi, L.A.Meyerovich and M.C.Tschantz, Verification and change-impact analysis of access-control policies, in: International Conference on Software Engineering (ICSE), 2005, pp. 196–205.
7.
M.Gofman, R.Luo, J.He, Y.Zhang and P.Yang, Incremental information flow analysis of role based access control, in: International Conference on Security and Management (SAM), 2009, pp. 397–403.
8.
M.Gofman, R.Luo, A.Solomon, Y.Zhang, P.Yang and S.Stoller, RBAC-PAT: A policy analysis tool for role based access control, in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2009, pp. 46–49.
9.
M.Gofman, R.Luo and P.Yang, User-role reachability analysis of evolving administrative role based access control, in: European Symposium on Research in Computer Security (ESORICS), 2010, pp. 455–571.
10.
J.D.Guttman, A.L.Herzog, J.D.Ramsdell and C.W.Skorupka, Verifying information flow goals in security-enhanced Linux, Journal of Computer Security13(1) (2005), 115–134.
11.
K.Irwin, T.Yu and W.H.Winsborough, On the modeling and analysis of obligations, in: ACM Conference on Computer and Communications Security (CCS), 2006, pp. 134–143.
12.
D.Jackson, I.Schechter and I.Shlyakhter, Alcoa: the alloy constraint analyzer, in: International Conference on Software Engineering (ICSE), June 2000, 2000, pp. 730–733.
13.
S.Jajodia, P.Samarati and V.S.Subrahmanian, A logical language for expressing authorizations, in: IEEE Symposium on Security and Privacy, 1997, pp. 31–42.
14.
K.Jayaraman, M.Tripunitara, V.Ganesh, M.Rinard and S.Chapin, Mohawk: Abstraction-refinement and bound-estimation for verifying access control policies, ACM Transaction on Information and System Security (TISSEC)15(4) (2013), 18:1–18:28.
15.
S.Jha and T.Reps, Model-checking SPKI-SDSI, Journal of Computer Security12 (2004), 317–353.
16.
N.Li and M.V.Tripunitara, Security analysis in role-based access control, ACM Transactions on Information and System Security (TISSEC)9(4) (2006), 391–420.
17.
R.Sandhu, V.Bhamidipati and Q.Munawer, The ARBAC97 model for role-based administration of roles, ACM Transactions on Information and Systems Security (TISSEC)2(1) (1999), 105–135.
18.
A.Sasturkar, P.Yang, S.D.Stoller and C.Ramakrishnan, Policy analysis for administrative role based access control, Theoretical Computer Science (TCS)412(44) (2011), 6208–6234.
19.
A.Schaad and J.D.Moffett, A lightweight approach to specification and analysis of role-based access control extensions, in: ACM Symposium on Access Control Models and Technologies (SACMAT), 2002, pp. 13–22.
20.
S.D.Stoller, P.Yang, M.I.Gofman and C.Ramakrishnan, Symbolic reachability analysis for parameterized administrative role-based access control, Journal of Computers & Security30(2,3) (2011), 148–164.
21.
S.D.Stoller, P.Yang, C.R.Ramakrishnan and M.I.Gofman, An ARBAC policy for a university, 2007, available at: http://www.cs.sunysb.edu/~stoller/ccs2007/university-policy.txt.
22.
S.D.Stoller, P.Yang, C.R.Ramakrishnan and M.I.Gofman, Efficient policy analysis for administrative role based access control, in: 14th ACM Conference on Computer and Communications Security (CCS), 2007, pp. 445–455.
23.
E.Uzun, V.Atluri, S.Sural, J.Vaidya, G.Parlato, A.L.Ferrara and M.Parthasarathy, Analyzing temporal role based access control models, in: ACM Symposium on Access Control Models and Technologies (SACMAT), 2012, pp. 177–186.
24.
P.Yang, M.Gofman and Z.Yang, Policy analysis for administrative role based access control without separate administration, in: 27th IFIP WG 11.3 Conference on Data and Applications Security and Privacy (DBSEC), pp. 49–64.
