|
|
|
The HRU and SPM models present different aspects of the answer to the safety question. The obvious issue is the relationship between these models. For example, if SPM and HRU are equivalent, then SPM provides a more specific answer to the safety question than the HRU analysis does (that is, safety in acyclic attenuating schemes is decidable). If HRU can describe some systems that SPM cannot, then SPM's answer applies only to a limited set of systems. This bears some examination.
Ammann and Sandhu [19] have used SPM to represent multilevel security models, integrity models, and the Take-Grant Protection Model, so SPM subsumes those models. But the HRU model is central to safety analysis problems, and we explore its relationship to SPM in more detail.
How does SPM compare with the HRU model? If the two models are equivalent, then any safety analysis of SPM also applies to HRU and SPM offers some significant advantages over HRU for such analyses.
First, SPM is a higher-level model than HRU. This allows policies to be expressed very succinctly and at a more abstract level than in the access control matrix model. Hence, safety analyses can focus on the limits of the model and not on the details of representation. By way of contrast, safety analyses using the HRU model usually require a detailed mapping of the policy to the model, followed by an analysis.
However, the HRU model allows rights to be revoked and entities to be deleted (the delete, destroy subject, and destroy object rules). The SPM model has no revocation rule. The justification is exactly the same as for the Take-Grant Protection Model analyses that ignore that model's creation rule: what is removed can be replaced. So, in some sense, comparing HRU and SPM directly is unfair. A better comparison is one between SPM and a monotonic HRU scheme, in which there are no revocation rules, and we will use that model for further comparison.
In terms of comprehensiveness, HRU allows multiconditional commands. For example, suppose a system has a parent right, similar to the create right but requiring two subjects to have those rights over one another. Then either subject can execute a multicreate command that creates a new object and gives both subjects r rights over the new object. The multicreate command would be
command multicreate(s0, s1, o)
if p in a[s0, s1 ] and r in a[s1, s0 ]
then
create object o
enter r into a[s1, o ];
enter r into a[s2, o ];
end
However, SPM cannot express this command easily because the can-create function allows creators to have at most one type. If s0 and s1 have different types, SPM has no mechanism for creating o. This suggests that SPM is less expressive than HRU.
Ammann and Sandhu [19, 20, 872] revisited the notion of creation in SPM. Implicit in all models discussed so far is the assumption of a single parent. This assumption is not common in nature. (Consider humans, who have two parents.) It is more common in computer science, but (as we shall see) changing paradigms often simplifies solutions.
Consider two users, Anna and Bill, who must cooperate to perform a task but who do not trust each other. This problem of mutual suspicion is one of the oldest problems in security [413] and arises in multiuser computing systems. The usual solution is for Anna to define a proxy and give it only those rights she wishes Bill to have and for Bill to define a proxy similarly. Then Anna gives Bill's proxy the privileges to invoke Anna's proxy, and Bill gives Anna's proxy similar privileges. Working indirectly, the two proxies can work together and perform the task. Multiple indirection is disallowed (or else Anna's proxy could give her rights to Bill's proxy to a third party). Hence, the way the proxies use rights must be restricted, leading to a complex set of rights and manipulations.
Multiple parenting simplifies this model. Anna and Bill jointly create a proxy. Each then gives the proxy only those rights needed to perform the task. Neither parent is allowed to copy rights from the proxy. At this point, the copy operation must embody all restrictions on the manipulation of proxy rights and abilities, which is simpler than restricting the particular application of rights (as must be done in the preceding solution).
The Extended Schematic Protection Model (or ESPM) adds multiple parenting to SPM. The joint creation operation includes the SPM creation operation as a special case. The can-create function becomes
cc
TS x … x TS x T;
The create rules for the parents in a joint creation operation can allow the parents to get one anothers' rights to the child as well as their own, but this is equivalent to a creation rule in which parent rights are not copied, followed by applications of the copy rule. For simplicity, we require that each parent be given tickets only for its own rights over the new child, and not for rights of other parents.
Let X1, …, Xn be the n subject parents, let Y be the created entity, and let R1,i, R2,i, R4,i R for i = 1, …, n. Each creation rule has i components, each of which provides the tickets to the ith parent and the child; for example, the ith rule is
crP(t(X1), …, t(Xn), t(Y)) = Y/R1,i
Xi/R2,i
The child also has a rule of the form
crC(t(X1), …, t(Xn), t(Y)) = Y/R3
These rules are analogous to the single-parent creation rules, but with one for each parent.
|
EXAMPLE: To expand on this concept, let's revisit Anna and Bill's situation. Anna and Bill are equals, so for modeling purposes they have the same type a. The proxy is of type p; because the proxy has delegated authority, a and p may be different. We model the rights that Anna and Bill have over the proxy by the right x in R. Thus:
Then the proxy can use the right x to transfer whatever set of privileges the proxy requires. |
Considering two-parent joint creation operations is sufficient for modeling purposes. To demonstrate this, we show how the two-parent joint creation operation can implement a three-parent joint creation operation.
Let P1, P2, and P3 be three subjects; they will create a (child) entity C. With a three-parent joint creation operation, can-create will be
cc(t(P1), t(P2), t(P3)) = Z
and the type of the child is t(C) 
T. The creation rules are
crP1(t(P1), t(P2), t(P3)) = C/R1,1
crP2(t(P1), t(P2), t(P3)) = C/R1,2
crP3(t(P1), t(P2), t(P3)) = C/R1,3
crC(t(P1), t(P2), t(P3)) = C/R3
Our demonstration requires that we use the two-parent joint creation rule, not the three-parent rule. At the end of the demonstration, the parents and the child should have exactly the same tickets for one another. We will create additional entities and types, but they cannot interact with any other entities (in effect, they do not exist for the rest of the entities). Finally, if the creation fails, the parents get no new tickets.
For convenience, and to simplify the notation, we assume that the parents and child are all of different types.
Define four new entities A1, A2, A3, and S; each Ai, of type ai = t(Ai), will act as an agent for the corresponding parent Pi, and S, of type s = t(S), will act as an agent for the child. Let the type t represent parentagethat is, an entity with the ticket X/t has X as a parent. Again, without loss of generality, we assume that a1, a2, a3, s, and t are all new types.
During the construction, each agent will act as a surrogate for its parent; this agent obtains tickets on behalf of the parent, and only after the child is created does the agent give the parent the ticket. That way, if the construction fails, the parent has no new tickets.
Augment the can-create rules as follows:
cc(pi) = a1
cc(p2, a1) = a2
cc(p3, a2) = a3
cc(a3) = s
cc(s) = c
These rules enable the parents to create the agents. The final agent can create the agent for the child, which subsequently creates the child. Note that the second agent has two parents (P2 and A1), as does the third agent (P3 and A2); these rules are the two-parent joint creation operation.
On creation, the creation rules dictate the new tickets given to the parent and the child. The following rules augment the existing rules.
crP(p1, a1) = Ø | crC(p1, a1) = p1/Rtc |
crPfirst(p2, a1, a2) = Ø | |
crPsecond(p3, a2, a3) = Ø | crC(p2, a1, a2) = p2/Rtc |
crPfirst(p3, a3, a3) = Ø | |
crPsecond(p3, a3, a3) = Ø | crC(p3, a2, a3) = p3/Rtc |
crP(a3, s) = Ø | crC(a3, s) = a3/tc |
crP(s, c) = C/Rtc | crC(s, c) = c/R3t |
Here, crPfirst and crPsecond indicate the tickets given to the first and second parents, respectively.
The link predicates indicate over which links rights can flow; essentially, no tickets can flow to the parents until the child is created. The following links restrain flow to the parents by requiring each agent to have its own "parent" right.
link1(A1, A2) = A1/t
A2/t
link1(A2, A3) = A2/t
link2(S, A2) = A3/t
link3(A1, C) = C/t
link3(A2, C) = C/t
link3(A3, C) = C/t
link4(A1, P1) = P1/t
link4(A2, P2) = P2/t
link4(A3, P3) = P3/t
The filter functions dictate which tickets are copied from one entity to another:
f1(a2, a1) = a1/t
f1(a3, a2) = a2/t
f2(s, a3) = a3/t
f3(a1, c) = p1/R4,1
f3(a2, c) = p2/R4,2
f3(a3, c) = p3/R4,3
f4(a1, p1) = c/R1,1
f4(a2, p2) = c/R1,2
f4(a3, p3) = c/R1,3
Now we begin the construction. The creations proceed in the obvious order; after all are completed, we have
P1 has no relevant tickets.
P2 has no relevant tickets.
P3 has no relevant tickets.
A1 has P1/Rtc.
A2 has P2/Rtc A1/tc.
A3 has P3/Rtc A2/tc.
S has A3/tc C/Rtc.
C has C/R3.
We now apply the links and filter functions to copy rights. The only link predicate that is true is link2(S, A3), so we apply f2; then A3's set of tickets changes, as follows:
A3 has P3/Rtc A2/tc A3/t C/Rtc.
Now link1(A3, A2) is true, so applying f1 yields
A2 has P2/Rtc A1/tc A2/t C/Rtc.
Now link1(A2, A1) is true, so applying f1 again yields
A1 has P1/Rtc A1/t C/Rtc.
At this point, all link3s in this construction hold, so
C has C/R3 P1/R4,1 P2/R4,2 P3/R4,3.
Then the filter functions associated with link4, all of which are also true, finish the construction:
P1 has C/R1,1 P1/R2,1.
P2 has C/R1,2 P2/R2,2.
P3 has C/R1,3 P3/R2,3.
This completes the construction. As required, it adds no tickets to P1, P2, P3, and C except those that would be added by the three-parent joint creation operation. The intermediate entities, being of unique types, can have no effect on other entities. Finally, if the creation of C fails, no tickets can be added to P1, P2, and P3 because none of the link predicates in this construction is true; hence, no filter functions apply.
Generalizing this construction to n parents leads to the following theorem.
Theorem 317. [19] The two-parent joint creation operation can implement an n-parent joint creation operation with a fixed number of additional types and rights, and augmentations to the link predicates and filter functions.
A logical question is the relationship between ESPM and HRU; Ammann and Sandhu show that the following theorem holds.
Theorem 318. [19] Monotonic ESPM and the monotonic HRU model are equivalent.
Furthermore, the safety analysis is similar to that of SPM; the only difference is in the definition of the state function s. The corresponding function s' takes the joint creation operation into account; given this, the nature of the unfolding algorithm is roughly analogous to that of SPM. This leads to the equivalent of Theorem 316:
Theorem 319. [19] For an ESPM system with an acyclic attenuating scheme, for every history H that derives h from the initial state there exists a history G without create operations that derives g from the fully unfolded state u such that
(
X, Y
Because the proof is analogous to that of Theorem 316, we omit it.
What is the benefit of this alternative representation? If SPM and ESPM model the same systems, the addition of n-parent joint creation operations is not at all interesting. But if ESPM can represent systems that SPM cannot, the addition is very interesting. More generally, how can we compare different models?
Ammann, Sandhu, and Lipton [21] use a graph-based representation to compare different models. An abstract machine represents an access control model; as usual, that machine has a set of states and a set of transformations for moving from one state to another. A directed graph represents a state of this machine. A vertex is an entity; it has an associated type that is static. Each edge corresponds to a right and, like a vertex, has a static type determined on creation. The source of the edge has some right(s) over the target. The allowed operations are as follows.
Initial state operations, which simply create the graph in a particular state
Node creation operations, which add new vertices and edges with those vertices as targets
Edge adding operations, which add new edges between existing vertices
As an example, we simulate the three-parent joint creation operation with two-parent joint creation operations. As before, nodes P1, P2, and P3 are the parents; they create a new node C of type c with edges of type e. First, P1 creates A1, which is of type a, and an edge from P1 to A1 of type e'. Both a and e' are used only in this construction.
Then A1 and P2 create a new node A2, which is of type a, and A2 and P3 create a new node A3, with type a, and edges of type e' as indicated:
Next, A3 creates a new node S, which is of type a, which in turn creates a new node C, of type c:
Finally, an edge adding operation depending on the presence of edges P1
A1, A1A2, A2A3, A3S, and SC adds an edge of type e from P1 to C. An edge adding operation depending on the presence of edges P2A2, A2A3, A3S, and SC adds an edge of type e from P2 to C. A last edge adding operation depending on the presence of edges P3A3, A3S, and SC adds an edge of type e from P3 to C:
This completes the simulation. Exercise 10 suggests a simpler simulation.
The formal definition of simulation relies on two other notions: a scheme and a correspondence between schemes.
Definition 322. A scheme is an abstract finite-state machine that defines finite sets of node types, edge types, initial state operations, node creation operations, and edge adding operations. A model is a set of schemes.
Definition 323. Let NT(X) and ET(X) be the sets of node types and edge types, respectively, in scheme X. Then scheme A and scheme B correspond if and only if the graph defining the state in scheme A is identical to the subgraph obtained by taking the state in scheme B and deleting all nodes not in NT(A) and all edges not in ET(A).
Consider the simulation of a scheme C3 with a three-parent joint creation operation by a scheme C2 with a two-parent joint creation operation, as was done earlier. After the three-parent joint creation operation, the C3 state would be as follows:
Contrasting this with the result of the C2 construction, and the fact that the types a and e' do not exist in C3, this state in C3 clearly corresponds to the state resulting from the construction in C2.
Intuitively, scheme A simulates scheme B if every state reachable by A corresponds to a state reachable by B. Because A may have more edge types and node types than B, simulation implies that if A can enter a state a, either there is a corresponding state reachable by B or, if not, A can transition to another state a' from a and there is a state reachable by B that corresponds to a'. The last condition means that if scheme A has a halting state, then scheme B must have a corresponding halting state; otherwise, the simulation is incorrect.
Definition 324. Scheme A simulates scheme B if and only if both of the following are true.
For every state b reachable by scheme B, there exists some corresponding state a reachable by scheme A; and
For every state a reachable by scheme A, either the corresponding state b is reachable by scheme B or there exists a successor state a' reachable by scheme A that corresponds to a state reachable by scheme B.
Now we can contrast the expressive power of models.
Definition 325. If there is a scheme in model MA that no scheme in model MB can simulate, then model MB is less expressive than model MA. If every scheme in model MA can be simulated by a scheme in model MB, then model MB is as expressive as model MA. If MA is as expressive as MB and MB is as expressive as MA, the models are equivalent.
|
EXAMPLE: Consider a model M with one scheme A that defines three nodes called X1, X2, and X3 and a two-parent joint creation operation. A has one node type and one edge type. The two-parent joint creation operation creates a new node and adds edges from both parents to the child. A has no edge adding operations. A's initial state is simply X1, X2, and X3, with no edges. Now, consider a model N with one scheme B that is the same as scheme A except that scheme B has a one-parent creation operation instead of a two-parent joint creation operation. Both A and B begin at the identical initial state. Which, if either, is more expressive? Clearly, scheme A can simulate scheme B by having the two parents be the same node. Hence model M is as expressive as model N. How might scheme B simulate the creation operation of scheme A? Suppose X1 and X2 jointly create a new node Y in scheme A; then there are edges from X1 and X2 to Y, but no edge from X3 to Y. Scheme B can use its single-parent creation operation to create a node Y with parent X1. However, an edge adding operation must allow the edge from X2 to Y to be added. Consider what this edge adding operation must allow. Because there is only one type of node, and one type of edge, the edge adding operation must allow an edge to be added between any two nodes. Because edges can be added only by using the two-parent joint creation operation in scheme A, all nodes in scheme A have even numbers of incoming edges. But given the edge adding rule in scheme B, because we can add an edge from X2 to Y, we can also add an edge from X3 to Y. Thus, there is a state in scheme B containing a node with three incoming edges. Scheme A cannot enter this state. Furthermore, because there is no remove rule and only one edge type, scheme B cannot transition from this state to a state in which Y has an even number of incoming edges. Hence, scheme B has reached a state not corresponding to any state in scheme A, and from which no state corresponding to a state in scheme A can be reached. Thus, scheme B cannot simulate scheme A, and so model N is less expressive than model M. |
Given these definitions, Ammann, Lipton, and Sandhu prove the following theorem.
Theorem 320. [21] Monotonic single-parent models are less expressive than monotonic multiparent models.
Proof Begin with scheme A in the preceding example. We show by contradiction that this scheme cannot be simulated by any monotonic scheme B with only a single-parent creation operation. (The example does not show this because we are removing the requirement that scheme B begin in the same initial state as scheme A.)
Consider a scheme B that simulates scheme A. Let nodes X1 and X2 in A create node Y1 with edges from X1 and X2 to Y1. Then in scheme B there is a node W that creates Y1 with a single incoming edge from W. The simulation must also use edge adding operations to add edges from X1 to Y1 and from X2 to Y1 (assuming that W
X1 and W
Let W invoke the single-parent creation operation twice more to create nodes Y2 and Y3 and use the edge adding rules to add edges from X1 to Y1, Y2, and Y3 and from X2 to Y1, Y2, and Y3. The resulting state clearly corresponds to a state in scheme A.
Because scheme A has exactly one node type, Y1, Y2, and Y3 are indistinguishable as far as the application of the node creation and edge adding rules is concerned. So proceed as in the example above: in scheme A, let Y1 and Y2 create Z. In the simulation, without loss of generality, let Y1 create Z using a single-parent creation operation. Then scheme B uses an edge adding operation to add an edge from Y2 to Zbut that same edge adding rule can be used to add one more edge into Z, from Y3. Thus, there are three edges coming into Z, which (as we saw earlier) is a state that scheme A cannot reach, and from which no future state in scheme B that corresponds to a state in scheme A can be reached. Hence, scheme B does not simulate scheme A, which contradicts the hypothesis.
Thus, no such scheme B can exist.
This theorem answers the question posed earlier: because ESPM has a multiparent joint creation operation and SPM has a single-parent creation operation, ESPM is indeed more expressive than SPM.
The strengths of SPM and ESPM appear to derive from the notion of "types." In particular, ESPM and HRU are equivalent, but the safety properties of ESPM are considerably stronger than those of HRU. Sandhu expanded the access control matrix model by adding a notion of "type" and revisiting the HRU results. This model, called the Typed Access Matrix (TAM) Model [875], has safety properties similar to those of ESPM and supports the notion that types are critical to the safety problem's analysis.
TAM augments the definitions used in the access control matrix model by adding types.
Definition 326. There is a finite set of types T, containing a subset of types TS for subjects.
The type of an entity is fixed when the entity is created (or in the initial state) and remains fixed throughout the lifetime of the model. The notion of protection state is similarly augmented.
Definition 327. The protection state of a system is (S, O, t, A), where S is the set of subjects, O is the set of objects, A is the access control matrix, and t:O
The TAM primitive operations are the same as for the access control matrix model, except that the create operations are augmented with types.
Precondition: s 
S
Primitive command: create subject s of type ts
Postconditions: S' = S { s }, O' = O { s },
(y O)[t'(y) = t(y)], t'(s') = ts,
(y O')[a'[s, y] = Ø], (x S')[a'[x, s] = Ø],
(x S)(y O)[a'[x, y] = a[x, y]]
In other words, this primitive command creates a new subject s. Note that s must not exist as a subject or object before this command is executed.
Precondition: o O
Primitive command: create object o of type to
Postconditions: S' = S, O' = O { o },
(y O)[t'(y) = t(y)], t'(o') = to,
(x S')[a'[x, o] =,Ø], (x S')(y O)[a'[x, y] = a[x, y]]
In other words, this primitive command creates a new object o. Note that o must not exist before this command is executed.
These primitive operations are combined into commands defined as in the access control matrix model. Commands with conditions are called conditional commands; commands without conditions are called unconditional commands.
Finally, we define the models explicitly.
Definition 328. A TAM authorization scheme consists of a finite set of rights R, a finite set of types T, and a finite collection of commands. A TAM system is specified by a TAM scheme and an initial state.
Definition 329. The MTAM (Monotonic Typed Access Matrix) Model is the TAM Model without the delete, destroy subject, and destroy object primitive operations.
Definition 330. Let a(x1 : t1, …, xk : tk) be a creating command, where x1, …, xk
From this, we can define the notion of acyclic creations.
Definition 331. The creation graph of an MTAM scheme is a directed graph with vertex set V and an edge from u
As an example, consider the following command, where s and p are subjects and f is an object.
command create•havoc(s : u, p : u, f : v, q : w)
create subject p of type u;
create object f of type v;
enter own into a[s,p];
enter r into a[q,p];
enter own into a[p,f];
enter r into a[p,f];
enter w into a[p,f];
end
Here, u and v are child types and u and w are parent types. Note that u is both a parent type and a child type. The creation graph corresponding to the MTAM scheme with the single command create•havoc has the edges (u, u), (u, w), (v, u), and (v, w). Thus, this MTAM scheme is cyclic. Were the create subject p of type u deleted from the command, however, u would no longer be a child type, and the resulting MTAM scheme would be acyclic.
Sandhu has shown that the following theorem is true.
Theorem 321. [875] Safety is decidable for systems with acyclic MTAM schemes.
The proof is similar in spirit to the proof of Theorem 316.
Furthermore, because MTAM subsumes monotonic mono-operational HRU systems, a complexity result follows automatically:
Theorem 322. [875] Safety is NP-hard for systems with acyclic MTAM schemes.
However, Sandhu [875] has also developed a surprising result. If all MTAM commands are limited to three parameters, the resulting model (called "ternary MTAM") is equivalent in expressive power to MTAM. However:
Theorem 323. [875] Safety for the acyclic ternary MTAM model is decidable in time polynomial in the size of the initial access control matrix.
|
|
|
| Top |