3.4 Closing the Gap

Given that in specific systems we can answer the safety question, why can't we answer it about generic systems? What is it about the Harrison-Ruzzo-Ullman (HRU) model that makes the safety question undecidable? What characteristics distinguish a model in which the safety question is decidable from a model in which the safety question is not decidable? A series of elegant papers have explored this issue.

The first paper introduced a model called the Schematic Send-Receive (SSR) Protection Model [869]. The Schematic Protection Model (SPM) [870] generalizes these results.

3.4.1 Schematic Protection Model

The key notion of the Schematic Protection Model, also called the SPM, is the protection type. This is a label for an entity that determines how control rights affect that entity. For example, if the Take-Grant Protection Model is viewed as an instance of a scheme under the SPM, the protection types are subject and object because the control rights take, grant, create, and remove affect subject entities differently than they do object entities. Moreover, under SPM, the protection type of an entity is set when the entity is created, and cannot change thereafter.

In SPM, a ticket is a description of a single right. An entity has a set of tickets (called a domain) that describe what rights it has over another entity. A ticket consists of an entity name and a right symbol; for example, the ticket X/r allows the possessor of the ticket to apply the right r to the entity X. Although a ticket may contain only one right, if an entity has multiple tickets X/r, X/s, and X/t, we abbreviate them by writing X/rst.

Rights are partitioned into a set of inert rights (RI) or control rights (RC). Applying an inert right does not alter the protection state of the system. For example, reading a file does not modify which entities have access to the document, so read is an inert right. But in the Take-Grant Protection Model, applying the take rule does change the protection state of the system (it gives a subject a new right over an object). Hence, the take right is a control right. SPM ignores the effect of applying inert rights, but not the effect of applying control rights.

The attribute c is a copy flag; every right r has an associated copyable right rc. A ticket with the copy flag can be copied to another domain. The notation r:c means r or rc, with the understanding that all occurrences of r:c are read as r or all are read as rc.

We partition the set of types T into a subject set TS and an object set TO. The type of an entity X is written t(X). The type of a ticket X/r:c is t(X/r:c), which is the same as t(X)/r:c. More formally, let E be the set of entities; then t:ET and t:E x RT x R.

The manipulation of rights is controlled by two relationships: a link predicate and a filter function. Intuitively, the link predicate determines whether the source and target of the transfer are "connected" (in a mathematical sense), and the filter function determines whether the transfer is authorized.

3.4.1.1 Link Predicate

A link predicate is a relation between two subjects. It is local in the sense that its evaluation depends only on the tickets that the two subjects possess. Formally:

Definition 3–13. Let dom(X) be the set of tickets that X possesses. A link predicate link_i(X, Y) is a conjunction or disjunction (but not a negation) of the following terms, for any right z RC.

1. X/z dom(X)

2. X/z dom(Y)

3. Y/z dom(X)

4. Y/z dom(Y)

5. true

A finite set of link predicates { link_i | i = 1, …, n } is called a scheme. If only one link predicate is defined, we omit the subscript i.

EXAMPLE: The link predicate corresponding to the Take-Grant Protection Model rules take and grant is link(X, Y) = Y/g dom(X) X/t dom(Y) Here, X and Y are connected if X has g rights over Y or Y has t rights over X, which corresponds to the model in the preceding section.

EXAMPLE: The link predicate link(X, Y) = X/b dom(X) connects X to every other entity Y provided that X has b rights over itself. With respect to networks, b would correspond to a broadcast right. However, X does not yet have the right to broadcast to all Y because predicates do not endow the ability to exercise that right. Similarly, the predicate link(X, Y) = Y/p dom(Y) corresponds to a pull connection between all entities X and Y. Again, this is not sufficient for Y to exercise the pull right, but it is necessary.

EXAMPLE: The universal link depends on no entity's rights: link(X, Y) = true This link holds even when X and Y have no tickets that refer to each other.

3.4.1.2 Filter Function

The filter functions impose conditions on when transfer of tickets can occur. Specifically, a filter function is a function f_i: TS x TS2^TxR that has as its range the set of copyable tickets. For a copy to occur, the ticket to be copied must be in the range of the appropriate filter function.

Combining this requirement with the others, a ticket X/r:c can be copied from dom(Y) to dom(Z) if and only if, for some i, the following are true:

One filter function is defined for each link predicate. As with the link predicates, if there is only one filter function, we omit the subscripts.

EXAMPLE: Let f(t(Y), t(Z)) = T x R. Then any tickets are transferable, assuming that the other two conditions are met. However, if f(t(Y), t(Z)) = T x RI, then only inert rights are transferable; and if f(t(Y), t(Z)) = Ø, no rights can be copied.

3.4.1.3 Putting It All Together

Let us take stock of these terms by considering two examples: an owner-based policy and the Take-Grant Protection Model.

In an owner-based policy, a subject U can authorize another subject V to access an object F if and only if U owns F. Here, the set of subjects is the set of users and the set of objects is the set of files. View these as types. Then:

TS = { user }, TO = { file }

In this model, ownership is best viewed as copy attributes—that is, if U owns F, all its tickets for F are copyable. Under this interpretation, the set of control rights is empty because no rights are required to alter the state of the protection graph. All rights are inert. For our example, assume that the r (read), w (write), a (append), and x (execute) rights are defined. Then:

RC = Ø, RI = { r:c, w:c, a:c, x:c }

Because the owner can give the right to any other subject, there is a connection between each pair of subjects and the link predicate is always true:

link(U, V) = true

Finally, tickets can be copied across these connections:

f(user, user) = { file/r, file/w, file/a, file/x }

EXAMPLE: Suppose a user Peter wishes to give another user Paul execute permissions over a file called doom. Then t(Peter) = user, t(doom) = file, and doom/xc dom(Peter). Because any user can give rights away to any other user, all users are "connected" in that sense, so link(Peter, Paul) = true. Finally, because t(doom) = file, and t(Paul) = user, we have t(doom)/x f(t(Peter), t(Paul)). Thus, Peter can copy the ticket doom/x to Paul.

The Take-Grant Protection Model can be formulated as an instance of SPM. The set of subjects and objects in the Take-Grant model corresponds to the set of subjects and objects in SPM:

TS = { subject }, TO = { object }

The control rights are t (take) and g (grant), because applying them changes the protection state of the graph. All other rights are inert; for our example, we will take them to be r (read) and w (write). All rights can be copied (in fact, the Take-Grant Protection Model implicitly assumes this), so:

RC = { tc, gc }, RI = { rc, wc }

Rights can be transferred along edges labeled t or g, meaning that one vertex on the edge has take or grant rights over the other. Let p and q be subjects. Then the link predicate is

link(p, q) = p/t dom(q) q/g dom(p)

Finally, any right can be transferred, so the filter function is simply

f(subject, subject) = { subject, object } x { tc, gc, rc, wc }

We now explore how the transfer of tickets occurs in SPM.

3.4.1.4 Demand and Create Operations

The demand function d:TS2^TxR authorizes a subject to demand a right from another entity. Let a and b be types. Then a/r:c d(b) means that every subject of type b can demand a ticket X/r:c for all X such that t(X) = a. This is a generalization of the take rule in the Take-Grant model. The take rule refers to an individual subject. The demand rule refers to all subjects of a particular type (here, of type b).

EXAMPLE: In the owner-based policy, no user can force another to give rights; hence, the range of the demand function is empty: d(user) = Ø. In the Take-Grant Protection Model, there is also no demand function. Although the take right is similar, to treat it as the demand right would require the creation of additional types to distinguish between those vertices directly connected by take edges to subjects and all other vertices. This complicates the system unnecessarily. Hence, d(subject) = Ø.

Sandhu [871] has demonstrated that a sophisticated construction eliminates the need for the demand operation. Thus, although the demand rule is present in SPM, that rule is omitted from the models that followed SPM.

Creating a new entity requires handling of not only the type of the new entity but also the tickets added by the creation. The type of the new entity is specified by the relation can-create (cc): cc TS x T; a subject of type a can create entities of type b if and only if cc(a, b) holds.

In practice, the rule of acyclic creates limits the membership in this relation. Represent the types as vertices, and let a directed edge go from a to b if cc(a, b). The relation cc is acyclic if this graph has no loops except possibly edges from one vertex to itself. Figure 3-5 gives an example of both cyclic and acyclic can-create relations. The rationale for this rule is to eliminate recursion in cc; if a subject of type a can create a subject of type b, none of the descendents of the subject can create a subject of type a. This simplifies the analysis without unduly limiting the applicability of the model.

Let A be a subject of type a = t(A) and let B be an entity of type b = t(B). The create-rule cr(a, b) specifies the tickets introduced when a subject of type a creates an entity of type b.

If B is an object, the rule specifies the tickets for B to be placed in dom(A) as a result of the creation. Only inert tickets can be created, so cr(a, b) { b/r:c RI }, and A gets B/r:c if and only if b/r:c cr(a, b).

If B is a subject, the rule also specifies that the tickets for A be placed in dom(B) as a result of the creation. Assume that types a and b are distinct. Let cr_p (a, b) be the set of tickets the creation adds to dom(A), and let cr_c(a, b) be the set of tickets the creation adds to dom(B). Then A gets the ticket A/r:c if a/r:c cr_p(a, b) and B gets the ticket A/r:c if a/r:c cr_c(a, b). We write cr(a, b) = { a/r:c, b/r:c | r:c R }. If the types a and b are not distinct, then do the types refer to the creator or the created? To avoid this ambiguity, if a = b, we define self/r:c to be tickets for the creator and a/r:c to be tickets for the created, and we say that cr(a, a) = { a/r:c, self/r:c | r:c R }. cr_p(a, b) and cr_c(a, b) are subsets of cr(a, a), as before.

Recall that the principle of attenuation of privilege (see Section 2.4.3) states that no entity may have more rights than its creator. The attenuating create-rule captures this notion:

Definition 3–14. A create-rule cr(a, a) = cr_p(a, b)|cr_c(a, b) is attenuating if:

1. cr_c(a, b) cr_p(a, b) and

2. a/r:c cr_p(a, b) self/r:c cr_p(a, b).

A scheme is attenuating if, for all types a such that cc(a, a), then cr(a, a) is attenuating.

If the graph for cc is constructed as above and has no loops, the scheme is attenuating.

EXAMPLE: The can-create relation for the owner-based policy says that users can create files; hence, cc(user) = { file }. The creator of the file can give itself any inert rights over the file; hence, cr(user, file) = { file/r:c | r RI }. Figure 3-6 shows the graph that this can-create relation induces; it is clearly acyclic and loop-free, so the scheme is attenuating. Figure 3-6. The graph at left corresponds to the cc for the owner-based policy. The graph at right corresponds to the Take-Grant Protection Model. Both are acyclic; the left graph is loop-free, but the right graph contains a loop. In the Take-Grant Protection Model, a subject can create either a subject or an object; hence, cc = { (subject, subject), (subject, object) }. A subject can give itself any rights over the vertices it creates, but it does not give the created subject any rights (although the creator may subsequently apply the grant rule to do so). Hence, crc(a, b) = Ø and crp(a, b) = { subject/tc, subject/gc, subject/rc, subject/wc }, so: cr(subject, subject) = { subject/tc, subject/gc, subject/rc, subject/wc } | Ø cr(subject, object) = { object/tc, object/gc, object/rc, object/wc } Figure 3-6 also shows the graph that this cc induces. It, too, is acyclic, but not loop-free. Because no self tickets are provided (the Take-Grant Protection Model rules are not reflexive), condition 2 of Definition 3–14 fails and the scheme is not attenuating.

Only dom(A) and dom(B) are affected by this operation; no other entity has its domain changed. Thus, the create-rule is local; this means that creation has only a local impact on the state of the system and again mimics real systems.

3.4.1.5 Safety Analysis

The goal of this model is to identify types of policies that have tractable safety analyses. Our approach will be to derive a maximal state in which any additional entities or rights do not affect the safety analysis. We then analyze this state.

First, we introduce a flow function that captures the flow of tickets around a particular state of the system being modeled.

Definition 3–15. A legal transition is a change in state caused by an operation that is authorized. A history is a sequence of legal transitions. A derivable state is a state obtainable by beginning at some initial state and applying a history.

In simpler terms, a system begins at an initial state. An authorized operation (such as the copying of a ticket) causes a legal transition. Suppose a sequence of legal transitions moves the system into a (final) state. Then that set of legal transitions forms a history, and the final state is derivable from the history and the initial state.

We represent states by a superscript h. The set of subjects in state h is SUB^h, the set of entities is ENT^h, and the link and dom relations in the context of state h are and dom^h.

Definition 3–16. If there are two entities X and Y, and either:

1. for some i, or

2. there is a sequence of subjects X₀, …, X_n such that , , and for k = 1, …, n,

then there is a path^h from X to Y.

In other words, a path^h from X to Y means that either a single link or a sequence of links connects X and Y. We write this as path^h(X, Y). Multiple path^hs may connect X and Y; in that case, we enumerate them as , j = 1, …, m.

The following algorithm defines the set (called the capacity, or cap(path^h(X,Y))) of the tickets that can flow over a path^h from X to Y.

In this set, the tickets for all but the final link must be copyable. If they are, any tickets in the last link will be in the capacity, whether or not they are copyable.

Now we can define the flow function as the union (sum) of all the capacities between two entities.

Definition 3–17. Let there be m path^hs between subjects X and Y in state h. The flow function flow^h:SUB^h x SUB^h2^TxR is defined as .

Sandhu [870] has shown that the flow function requires O(|T x R| |SUB^h|³), and hence the computation's time complexity is polynomial in the number of subjects in the system.

This definition allows us to sharpen our intuition of what a "maximal state" is (and will ultimately enable us to define that state formally). Intuitively, a maximal state maximizes flow between all pairs of subjects. Call the maximal state * and the flow function corresponding to this state flow^*; then if a ticket is in flow^*(X, Y), there exists a sequence of operations that can copy the ticket from X to Y. This brings up two questions. First, is a maximal state unique? Second, does every system have a maximal state?

We first formally define the notion of maximal state using a relation named ₀.

Definition 3–18. The relation g ₀ h is true if and only if, for all pairs of subjects X and Y in SUB⁰, flow^g(X, Y) flow^h(X, Y). If g ₀ h and h ₀ g, g and h are equivalent.

In other words, the relation ₀ induces a set of equivalence classes on the set of derivable states.

Definition 3–19. For a given system, a state m is maximal if and only if h ₀ m for every derivable state h.

In a maximal state, the flow function contains all the tickets that can be transferred from one subject to another. Hence, all maximal states are in the same equivalence class and thus are equivalent. This answers our first question.

To show that every system has a maximal state, we first show that for any state in a finite collection of derivable states, there is a maximal state.

Lemma 3–3. Given an arbitrary finite collection H of derivable states, there exists a derivable state m such that, for all h H, h ₀ m.

Proof By induction on |H|.

Basis. Take H = Ø and m to be the initial state. The claim is trivially true.

Induction hypothesis. The claim holds when |H| = n.

Induction step. Let |H'| = n + 1, where H' = G { h }; thus, |G| = n. Choose g G such that, for every state x G, x ₀ g; such a state's existence is guaranteed by the induction hypothesis.

Consider the states g and h, defined above. Each of these states is established by a history. Let M be an interleaving of these histories that preserves the relative order of transitions with respect to g and h, and with only the first create operation of duplicate create operations in the two histories. Let M attain state m. If either path^g(X, Y) for X, Y SUB^g or path^h(X, Y) for X, Y SUB^h, then path^m(X, Y), as g and h are ancestor states of m and SPM is monotonic. Thus, g ₀ m and h ₀ m, so m is a maximal state in H'. This concludes the induction step and the proof.

Take one state from each equivalence class of derivable states. To see that this is finite, consider each pair of subjects in SUB⁰. The flow function's range is 2^TxR, so that function can take on at most 2^|TxR| values. Given that there are |SUB⁰|² pairs of subjects in the initial state, there can be at most 2^|TxR||SUB⁰|² distinct equivalence classes.

Theorem 3–15. There exists a maximal state * for every system.

Proof Take K to be the collection of derivable states that contains exactly one state from each equivalence class of derivable states. From above, this set is finite. The theorem follows from Lemma 3–3.

In this model, the safety question now becomes: Is it possible to have a derivable state with X/r:c in dom(A), or does there exist a subject B with ticket X/rc in the initial state or which can demand X/rc and t(X)/r:c in flow^*(B, A)?

To answer this question, we need to construct a maximal state and test. Generally, this will require the creation of new subjects. In the general case, this is undecidable. But in special cases, this question is decidable. We now consider an important case—that of acyclic attenuating schemes—and determine how to construct the maximal state.

Consider a state h. Intuitively, generating a maximal state m from h will require all three types of operations. Define u to be a state corresponding to h but with a minimal number of new entities created such that m can be derived from u without any create operations. (That is, begin in state h. Use create operations to create as few new entities as possible such that state m can be derived from the new state after the entities are created. The state after the entities are created, but before any other operations occur, is u.) For example, if in the history from h to m, subject X creates two entities of type y, in u there would be only one entity of type y. That entity would act as a surrogate for the two entities that X created. Because m can be derived from u in polynomial time, if u can be created by adding to h a finite number of subjects, the safety question is decidable in polynomial time for such a system.

We now make this formal.

Definition 3–20. ([870], p.425) Given any initial state 0 of an acyclic attenuating scheme, the fully unfolded state u is the state derived by the following algorithm.

(* delete any loops so it's loop-free *)
cc' = cc – { (a, a) | a  TS }
(* mark all subjects as unfolded *)
for X  SUB0 do
        folded = folded  { X }
(* if anything is folded, it has to be unfolded *)
while folded  Ø do begin
        (* subject X is going to be unfolded *)
        folded = folded – { x }
        (* for each type X can create, create one entity of *)
        (* that type and mark it as folded; this will force *)
        (* the new entity to be unfolded *)
        for y  TS do begin
            if cc'(t(X), y) then
               X creates Y of type y
               (* system is in state g here *)
               if y  SUBg then
                   folded = folded  { X }
        end
end
(* now account for the loops; the system is in state h here *)
for X  SUBh do
        if cc(t(X), t(X)) then
           X creates Y of type t(X)
(* currently in desired state u *)

The while loop will terminate because the system is acyclic and attenuating, hence the types of the created entities must all be different—and TS is a finite set.

Definition 3–21. Given any initial state of an acyclic attenuating scheme, for every derivable state h define the surrogate function s:ENT^hENT^h by

1. s(X) = X if X in ENT⁰

2. s(X) = s(Y) if Y creates X and t(Y) = t(X)

3. s(X) = t(Y)-surrogate of s(Y) if Y creates X and t(Y) | t(X)

It is easy to show that t(s(A)) = t(A).

If t(X) = t(Y), then s(X) = s(Y). If t(X) t(Y), then in the construction of u, s(X) creates s(Y) (see the while loop of Definition 3–20). Also, in this construction, s(X) creates entities X' of type t(X) = t(s(X)) (see the last for loop of Definition 3–20). So, by Definition 3–14, we have the following lemma.

Lemma 3–4. For a system with an acyclic attenuating scheme, if X creates Y, then tickets that would be introduced by pretending that s(X) creates s(Y) are in dom^u(s(X)) and dom^u(s(Y)).

Now, let H be a legal history that derives a state h from the initial state of an acyclic attenuating system. Without loss of generality, we may assume that H's operations are ordered such that all create operations come first, followed by all demand operations, followed by all copy operations. Replace the transitions in H as follows, while preserving their relative order.

Call the new history G. Then:

Lemma 3–5. Every transition in G is legal, and if X/r:c dom^h(Y), then s(X)/r:c dom^g(s(Y)).

Proof By induction on the number of copy operations in H.

Basis. Assume that H consists only of create and demand operations. Then G consists only of demand operations. By construction, and because s preserves type, every demand operation in G is legal. Furthermore, X/r:c can appear in dom^h(Y) in one of three ways. If X/r:c dom⁰(Y), then X, Y ENT⁰ and s(X)/r:c dom^g(s(Y)) trivially holds. If a create operation in H put X/r:c dom^h(Y), s(X)/r:c dom^g(s(Y)) by Lemma 3–4. And if a demand operation put X/r:c dom^h(Y), then s(X)/r:c dom^g(s(Y)) follows from the corresponding demand operation in G. This establishes both parts of the claim.

Induction hypothesis. Assume that the claim holds for all histories with k copy operations, and consider a history H with k + 1 copy operations. Let H' be the initial sequence of H composed of k copy operations, and let h' be the state derived from H'.

Induction step. Let G' be the sequence of modified operations corresponding to H'. By the induction hypothesis, G' is a legal history. Let g' be the state derived from G'. Suppose the final operation of H is "Z copies X/r:c from Y." By construction of G, the final operation of G is "s(Z) copies s(X)/r:c from s(Y)." Now, h differs from h' by at most X/r:c dom^h(Z). However, the construction causes the final operation of G to be s(X)/r:c dom^h(s(Z)), proving the second part of the claim.

Because H' is legal, for H to be legal the following conditions must hold.

1. X/rc dom^h'(Y)

2. 

3. t(X/r:c) f_i(t(Y), t(Z))

The induction hypothesis, the first two conditions above, and X/r:c dom^h'(Y) mean that s(X)/rc dom^g'(s(Y)) and . Because s preserves type, the third condition and the induction hypothesis imply t(s(X)/r:c) f_i(t(s(Y)), t(s(Z))). G' is legal, by the induction hypothesis; so, by these conditions, G is legal. This establishes the lemma.

Corollary 3–3. For every i, if , then .

We can now present the following theorem.

Theorem 3–16. For a 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 SUB^h)[flow^h(X, Y) flow^g(s(X), s(Y))]

Proof It suffices to show that for every path^h from X to Y there is a path^g from s(X) to s(Y) for which cap(path^h(X, Y)) = cap(path^g(s(X), s(Y)). Induct on the number of links.

Basis. Let the length of the path^h from X to Y be 1. By Definition 3–16, then, , so by Corollary 3–3. Because s preserves type, cap(path^h(X, Y)) = cap(path^g(s(X), s(Y)), verifying the claim.

Induction hypothesis. Assume that the claim holds for every path^h of length k.

Induction step. Consider a path^h from X to Y of length k + 1. Then there exists an entity Z with a path^h from X to Z of length k, and . By the induction hypothesis, there is a path^g from s(X) to s(Z) with the same capacity as the path^h from X to Z. By Corollary 3–3, we have . Because s preserves type, there is a path^g from X to Y with cap(path^h(X, Y)) = cap(path^g(s(X), s(Y)), proving the induction step and therefore the theorem.

Thus, any history derived from an initial state u can be simulated by a corresponding history applied to the fully unfolded state v derived from u. The maximal state corresponding to v is #u; the history deriving this state has no creates. From Theorem 3–16, for every history that derives h from the initial state,

( X, Y SUB^h)[flow^h(X, Y) flow^#u(s(X), s(Y))]

For X SUB⁰, s(X) = X; therefore, ( X, Y SUB⁰)[flow^h(X, Y) flow^#u(X, Y)]. This demonstrates the following corollary.

Corollary 3–4. The state #u is a maximal state for a system with an acyclic attenuating scheme.

Not only is #u derivable from u, it is derivable in time polynomial with respect to |SUB^u| (and therefore to |SUB⁰|). Moreover, the straightforward algorithm for computing flow^#u will be exponential in |TS| in the worst case. This means that for acyclic attenuating schemes, the safety question is decidable.