8.2 Deterministic Noninterference

The example above suggests an alternative view of security phrased in terms of interference. In essence, a system is secure if groups of subjects cannot interfere with one another. In the first example in Section 8.1, the "interference" would be Matt's interfering with Holly's acquiring the CPU for her process. Intuitively, this notion is more inclusive than "writing" and enables us to express policies and models more simply. Gougen and Meseguer [412] used this approach to define security policies.

To begin, we view a system as a state machine consisting of a set S = { s₁, ... } of subjects, a set S = { s₀, s₁, ... } of states, a set O = { o₁, ... } of outputs, and a set Z = { z₁, ... } of commands. For notational convenience, we define a set of state transition commands C = S x Z, because in what follows the clearance of the subject executing the command affects the actual command that is performed.

Definition 8–1. A state transition function T: C x S S describes the effect of executing command c when in state s, and an output function P: C x S O describes the output of the machine on executing command c in state s. Initially, the system is in state s₀.

We do not define any inputs, because either they select the specific commands to be executed or they can be encoded in the set of state transition commands. If the number x is to be input, we simply define a command that corresponds to reading x. We can encode the initial state as a command; the system begins at the empty state (and the first command moves it to s₀). This notation simplifies the abstract system.

In this system, the state transition commands produce outputs. The outputs are therefore functions of the transition commands, and thus are functions of the inputs and the initial state. We have also assumed that the system is deterministic, since the state transition functions are functions, and time is not considered. We will relax this restriction later.

EXAMPLE: Consider a machine with two bits of state information, H and L (for "high" and "low," respectively). The machine has two commands, xor0 and xor1, which exclusive-or both bits with 0 and 1, respectively. There are two users: Holly (who can read high and low information) and Lucy (who can read only low information). The system keeps two bits of state (H, L). For future reference, this will be called the two-bit machine. For this example, the operation affects both state bits regardless of whether Holly or Lucy executes the instruction. (This is not a requirement of the two-bit machine and will be varied later on.) The set S = { (0, 0), (0, 1), (1, 0), (1, 1) }. The set S = { Holly, Lucy }. The set C = { xor0, xor1 }. Table 8-1 shows the result of the state transition function. The output function for Holly is both bits; for Lucy, it is the L bit only.

Next, let us relate outputs to state. Two observations will make the formulation straightforward. First, T is inductive in the first argument, because T(c₀, s₀) = s₁ and T(c_i+1, s_i+1) = T(c_i+1, T(c_i, s_i)). This gives us the notion of applying a sequence of commands to an initial state, so let C* be the set of sequences of commands in C—that is, C* is the transitive closure of C under composition. Then T*: C* x S S, where

c_s = c₀, ..., c_n T*(c_s, s_i) = T(c_n, T(c_n–1, ..., T(c₀, s_i)...))

Second, the output function P is also inductive in the second argument. This allows us to define a similar function P*: C* x S O, which gives the sequence of outputs resulting from a sequence of commands to a system beginning at an initial state.

Given the assumptions above, the outputs provide a record of the system's functioning. The problem is that some subjects are restricted in the outputs (and actions) they can see. In the first example in Section 8.1, Holly should not have seen Matt's outputs, but Matt could see any outputs from Holly. We make this notion rigorous.

Definition 8–2. Let T*(c_s, s_i) be a sequence of state transitions for a system. Let P*(c_s, s_i) be the corresponding outputs. Then proj(s, c_s, s_i) is the set of outputs in P*(c_s, s_i) that subject s is authorized to see, in the same order as those outputs appear in P*(c_s, s_i).

In this definition, each command may produce some output, but subjects with insufficient clearance may not be able to see that output, lest they deduce information about the previous state of the system. The function proj(s, c_s, s_i) is simply the list of outputs resulting from removing the outputs that s is not authorized to see.

This captures the notion that s may not see all outputs because the security policy may restrict s's access to them. However, s may not have knowledge of all commands, either, and so we need a corresponding definition for them.

Definition 8–3. Let G S be a group of subjects, and let A Z be a set of commands. Define p_G(c_s) as the subsequence of c_s obtained by deleting all elements (s, z) in c_s with s G. Define p_A(c_s) as the subsequence of c_s obtained by deleting all elements (s, z) in c_s with z A. Define p_G,A(c_s) as the subsequence of c_s obtained by deleting all elements (s, z) in c_s such that both s G and z A.

This purge function p captures the notion that certain command executions must be invisible to some subjects. Applying the purge function to an output string generates the output string corresponding to those commands that the subject is allowed to see. For a specific system, the desired protection domains would dictate the membership of G and A.

EXAMPLE: In the two-bit machine, let s0 = (0, 1). Holly applies the command xor0, Lucy the command xor1, and Holly the command xor1 to the state machine. The commands affect both state bits, and both bits are output after each command. We take cs to be the sequence (Holly, xor0), (Lucy, xor1), (Holly, xor1). The output is 011001 (where bits are written sequentially, the High bit being first in each pair). proj(Holly, cs, s0) = 011001 proj(Lucy, cs,s0) = 101 pLucy(cs) = pLucy,xor1(cs) = (Holly, xor0), (Holly, xor1) pHolly(cs) = (Lucy, xor1) pLucy,xor0(cs) = (Holly, xor0), (Lucy, xor1), (Holly, xor1) pHolly,xor0(cs) = pxor0(cs) = (Lucy, xor1), (Holly, xor1) pHolly,xor1(cs) = (Holly, xor0), (Lucy, xor1) pxor1(cs) = (Holly, xor0)

Intuitively, if the set of outputs that any user can see corresponds to the set of inputs that that user can see, then the system is secure. The following definition formalizes this as "noninterference."

Definition 8–4. Let G, G' S be distinct groups of subjects and let A Z be a set of commands. Users in G executing commands in A are noninterfering with users in G' (written A,G :| G') if and only if, for all sequences c_s with elements in C*, and for all s G', proj(s, c_s, s_i) = proj(s, p_G,A(c_s), s_i).

If either A or G is not present, we handle it in the obvious way.

EXAMPLE: Consider the sequence cs = (Holly, xor0), (Lucy, xor1), (Holly, xor1) in the two-bit machine with operations affecting both state bits and both bits being output after each command. Take G = { Holly }, G' = { Lucy }, and A = Ø. Then pHolly(cs) = (Lucy, xor1), so proj(Lucy, pHolly(cs), s0) = 1. This means that the statement { Holly } :| { Lucy } is false, because proj(Lucy, cs, s0) = 101 proj(Lucy, pHolly(cs), s0). Intuitively, this makes sense, because commands issued to change the H bit also affect the L bit.

EXAMPLE: Modify the set of commands above so that Holly can alter only the H bit and Lucy only the L bit. Consider the sequence cs = (Holly, xor0), (Lucy, xor1), (Holly, xor1). Given an initial state of (0, 0), the output is 0H1L1H, where the subscripts indicate the security level of the output. Take G = { Holly }, G' = { Lucy }, and A = Ø; so pHolly(cs) = (Lucy, xor1) and proj(Lucy, pHolly(cs), s0) = (1). Now we have proj(Lucy, cs, s0) = proj(Lucy, pHolly(cs), s0), and { Holly } :| { Lucy } holds. Again, intuition suggests that it should, because no action that Holly takes has an effect on the part of the system that Lucy can observe.

We can now formulate an alternative definition of a security policy. By Definition 4–1, a security policy describes states in which forbidden interferences do not occur (authorized states). Viewed in this light [412], we have:

Definition 8–5. A security policy is a set of noninterference assertions.

The set of noninterference relations defined in Definition 8–4 characterize the security policy completely. An alternative, less common but more elegant, approach begins with the notion of a security policy and characterizes noninterference in terms of that definition [858].

Consider a system X as a set of protection domains D = { d₁, …, d_n }. Associated with X are states, commands, subjects, and transition commands. Whenever a transition command c is executed, the domain in which it is executed is written dom(c).

Definition 8–5A. Let r be a reflexive relation on D x D. Then r defines a security policy for M.

The relation r defines how information can flow. If d_ird_j, then information can flow from domain d_i to domain d_j. Otherwise, it cannot. Because information can flow within a protection domain, d_ird_i. Note that this definition says nothing about the content of the security policy; it merely defines what a "policy" is.

We can define a function p' analogous to the p in Definition 8–3, but the commands in A and the subjects in G and G' are now part of the protection domains, so we express p' in terms of protection domains.

Definition 8–3A. Let d D, c C, and c_s C*. Then p_d'(n) = n, where n is the empty sequence. If dom(c)rd, then p_d'(c_sc) = p_d'(c_s)c. Otherwise, p_d'(c_sc) = p_d'(c_s).

This says that if executing c will interfere with protection domain d, then c will be "visible." Otherwise, the resulting command sequence has the same effect as if c were not executed.

Given this definition, defining noninterference security is immediate.

Definition 8–4A. Let a system consist of a set of domains D. Then it is noninterference-secure with respect to the policy r if P*(c, T*(c_s, s₀)) = P*(c, T*(p_d'(c_s), s₀)).

Rather than defining a projection function (as in Definition 8–2), consider the set of states related by an equivalence relation with respect to a domain of a command.

Definition 8–2A. Let c C and dom(c) D, and let ~^dom(c) be an equivalence relation on the states of a system X. Then ~^dom(c) is output-consistent if s_a ~^dom(c) s_b implies P(c, s_a) = P(c, s_b).

Two states are output-equivalent if, for the subjects in dom(c), the projections of the outputs for both states after c is applied are the same. This immediately leads to the following lemma.

Lemma 8–1. Let T*(c_s, s₀) ~^d T*(p_d(c_s), s₀) for c C. Then, if ~^d is output-consistent, X is noninterference-secure with respect to the policy r.

Proof Take d = dom(c) for some c C. Applying Definition 8–2A to the hypothesis of this claim, P*(c, T*(c_s, s₀)) = P*(c, T*(p_dom(c)(c_s), s₀)). But this is the definition of noninterference-secure with respect to r (see Definition 8–4A).

Contrasting this approach with the more common first approach illuminates the importance of the security policy. In the first approach, the security policy was defined in terms of noninterference, but it arose from the conditions that caused the particular set of subjects G and the commands A. So, in some sense, Definition 8–5 is circular. The second approach eliminates this circularity, because noninterference is characterized in terms of a defined security policy. However, the second approach obscures the relationship among subjects, commands, and noninterference requirements because of the abstraction of "protection domains." The notion of outputs characterizing commands is crucial, because information flow is defined in terms of outputs. So both characterizations have their places.

8.2.1 Unwinding Theorem

The unwinding theorem links the security of sequences of state transition commands to the security of the individual state transition commands. The name comes from "unwinding" of the sequence of commands. This theorem is central to the analysis of systems using noninterference, because it reduces the problem of proving that a system design is multilevel-secure to proving that if the system design matches the specifications from which certain lemmata are derived, then the design is mathematically certain to provide multilevel-security correctly.^[2]

^[2] This says nothing about the implementation of that design, of course. See Part 6, "Assurance."

We follow Rushby's treatment [858]. The next two definitions provide the necessary background.

Definition 8–6. Let r be a policy. Then a system X locally respects r if dom(c) being noninterfering with d D implies s_a ~^d T(c, s_a).

If the command c does not have any effect on domain d under policy r, then the result of applying c to the current state should appear to have no effect with respect to domain d. When this is true, the system locally respects r.

Definition 8–7. Let r be a policy and d D. If s_a ~^d s_b implies T(c, s_a) ~^d T(c, s_b), the system X is transition-consistent under policy r.

Transition consistency simply means that states remain equivalent with respect to d for all commands c.

Lemma 8–2. Let c₁, c₂ C, d D, and for some policy r, (dom(c₁), d) r and (dom(c₂), d) r. Then T*(c₁c₂, s) = T(c₁, T(c₂, s)) = T(c₂, T(c₁, s)).

Proof See Exercise 2.

Theorem 8–1. Unwinding Theorem. Let r be a policy, and let X be a system that is output consistent, transition consistent, and locally respects r. Then X is non-interference secure with respect to the policy r.

Proof The goal is to establish that s_a ~^d s_b implies T*(c_s, s_a) ~^d T*(p_d'(c_s), s_b). We do this by induction on the length of c_s.

Basis. If c_s = n, T*(c_s, s_a) = s_a and p_d'(n) = n. The claim follows immediately.

Hypothesis. Let c_s = c₁...c_n. Then s_a ~^d s_b implies T*(c_s, s_a) ~^d T*(p_d'(c_s), s_b).

Step. Consider c_sc_n+1. We assume s_a ~^d s_b. We must show the consequent. We consider two distinct cases for T*(p_d'(c_sc_n+1), s_b).

1. If (dom(c_n+1), d) r, by definition of T* and definition 8-3A,

   T*(p_d'(c_sc_n+1), s_b) = T*(p_d'(c_s)c_n+1, s_b) = T(c_n+1, T*(p_d'(c_s), s_b)).

   As X is transition consistent, if s_a ~^d s_b, then T(c_n+1, s_a) ~^d T(c_n+1, s_b). From this and the induction hypothesis,

   T(c_n+1, T*(c_s, s_a)) ~^d T(c_n+1, T*(p_d'(c_s), s_b)).

   Substituting for the right side from the previous equality,

   T(c_n+1, T*(c_s, s_a)) ~^d T*(p_d'(c_sc_n+1), s_b).

   From the definition of T*, this becomes

   T*(c_sc_n+1, s_a) ~^d T*(p_d'(c_sc_n+1), s_b).

   proving the hypothesis.

2. If (dom(c_n+1), d) r, by definition 8-3A,

   T*(p_d'(c_sc_n+1), s_b) = T*(p_d'(c_s), s_b).

   From the induction hypothesis, this means

   T*(c_s, s_a) ~^d T*(p_d'(c_sc_n+1), s_b).

   As X locally respects r, s ~^d T(c_n+1, s) for any s. Then T(c_n+1, s_a) ~^d s_a, so

   T(c_n+1, T*(c_s, s_a)) ~^d T*(c_s, s_a).

   Substituting back, this becomes

   T(c_n+1, T*(c_s, s_a)) ~^d T*(p_d'(c_sc_n+1), s_b)

   verifying the hypotheses.

In either case, then, the hypothesis holds, completing the induction step.

Having completed the induction, take s_a = s_b = s₀. Then, by Lemma 8–1, if ~^d is output consistent, X is non-interference secure with respect to the policy r.

The significance of Theorem 8–1 is that it provides a basis for analyzing systems that purport to enforce a noninterference policy. Essentially, one establishes the conditions of the theorem for a particular set of commands and states with respect to some policy and a set of protection domains. Then noninterference security with respect to r follows.

8.2.2 Access Control Matrix Interpretation

Rushby presented a simple example of the use of the unwinding theorem [858]. The goal is to apply the theorem to a system with a static access control matrix. Our question is whether or not the given conditions are sufficient to provide noninterference security.

We begin with a model of the system. As usual, it is composed of subjects and objects. The objects are locations in memory containing some data. The access control matrix controls the reading and writing of the data. The system is in a particular state; the state encapsulates the values in the access control matrix.

Specifically, let L = { 1₁, …, l_m } be the set of objects (locations) in memory or on disk. Let V = { v₁, …, v_n } be the set of values that the objects may assume. As usual, the set of states is S = { s₁, …, s_k }. The set D = { d₁, …, d_j } is the set of protection domains. We also define three functions for convenience.

Let s be a subject in the protection domain d, and let o be an object. The functions represent the access control matrix A because the entry corresponding to A[s, o] contains "read" if o read(d) and contains "write" if o write(d). This also leads to a natural interpretation of the equivalence relation in Definition 8–2A—namely, that two states are equivalent with respect to a given protection domain if and only if the values of all objects that can be read under that protection domain are the same. Symbolically,

[s_a ~^dom(c) s_b] [ l_i read(d) [value(l_i, s_a) value(l_i, T(c, s_a))] ]

The system X enforces the relevant access control policy r when the following three conditions are met.

These requirements are standard for access control mechanisms (in particular, note that they are independent of any particular security policy, although such a policy must exist). We now augment our system with two more requirements for some security policy r.

This requirement says that if u can interfere with v, then every object that can be read in protection domain u can also be read in protection domain v. This follows from the need of v to read information from something in u. Given this, if an object that could not be read in u could be read in v, but some other object in u could be read in v, information could flow from the first object to the second and hence out of domain u.

This simply says that if a subject can read an object in domain v, and another subject can read that object in domain u, then domain v can interfere with domain u.

Theorem 8–2. Let X be a system satisfying the five conditions above. Then X is noninterference-secure with respect to the policy r.

Proof Taking the equivalence relation to be ~^d in Definition 8–2A, condition 1 and the definition of "output-consistent" are the same.

We use proof by contradiction to show that X locally respects r. Assume that (dom(c), d) r but that s_a ~^d T(c, s_a) does not hold. By the interpretation of ~^d, this means that there is some object whose value is changed by c:

l_i read(d) [value(l_i, s_a) value(l_i, T(c, s_a))]

By condition 3, l_i write(dom(c)). Combining this with the selection of l_i, both parts of condition 5 hold. By that condition, (dom(c), d) r. This contradicts the hypothesis, so s_a ~^d T(c, s_a) must hold and X locally respects r.

We next consider transition consistency. Assume that s_a ~^d s_b; we must show that value(l_i, T(c, s_a)) = value(l_i, T(c, s_b)) for l_i read(d). We consider three cases, each dealing with the change that c makes in l_i in states s_a and s_b.

In all three cases, X is transition-consistent.

Under the stated conditions, X is output-consistent, locally respects r, and is transition-consistent. By the unwinding theorem (Theorem 8–1), then, X is noninterference-secure with respect to the policy r.

All that remains is to verify that the five conditions hold for the system being modeled.

8.2.3 Security Policies That Change over Time

We now extend the preceding noninterference analysis to include policies that are not static. As an example of such a policy, consider an access control matrix for a discretionary access control mechanism. Subjects may revoke permissions, or add permissions, over objects they own. The analysis above assumes that the matrix will be constant; in practice, the matrix rarely is.

EXAMPLE: Let w be the sequence of elements of C leading up to the current state. Let cando(w, s, z) be true if the subject s has permission to execute the command z in the current state. We condition noninterference for the system on cando. In the current state, if cando(w, Holly, "read f") is false, then Holly cannot interfere with any other user by reading file f.

We now generalize the notion of noninterference to handle this case. First, we must define a function analogous to p_G,A(w).

Definition 8–8. Let G S be a group of subjects and let A Z be a set of commands. Let p be a predicate defined over elements of C*. Let c_s = c₁, …, c_n C*. Let n represent the empty sequence. Then p''(n) = n, and p"((c₁, ..., c_n)) = (c₁', ..., c_n'), where c_i' = n if p(c₁', ..., c_i–1') and c_i = (s, z) with s G and z A; and c_i' = c_i otherwise.

The essence of the definition lies in the use of the predicate. Informally, p"(c_s) is c_s; however, when the predicate p is true and an element of c_s involves a subject in G and a command in A, the corresponding element of c_s is replaced by n. This deletes that element. From this, the extension to noninterference is straightforward.

Definition 8–9. Let G, G' S be groups of subjects and let A Z be a set of commands. Let P be a predicate defined over elements of C*. Users in G executing commands in A are noninterfering with users in G' under the condition p (written A,G :| G' if p) if and only if proj(s, c_s, s_i) = proj(s, p''(c_s), s_i) for all sequences c_s C* and all s G.

EXAMPLE: Return to the discretionary access control example. A very simple security policy based on noninterference is (s S)(z Z)[ {z}, {s} :| S if ¬cando(w, s, z)] This says that if a subject cannot execute the command in any state, that subject cannot use that command to interfere with any subject in the system.

EXAMPLE: Gougen and Meseguer [412] amplify this policy by considering systems in which rights can be passed to other users. Define the command pass(s, z), s S and z Z, to grant to s the right to execute command z. Let wn = v1…vn be a sequence of n elements, vi C*; then prev(wn) = wn–1 and last(wn) = vn. Our policy will say that no subject s can use z to interfere if, in the previous state, s did not have the right to z, and no subject having that right gave it to s: { z }, { s } :| S if [ ¬cando(prev(w), s, z) [ cando(prev(w), s', pass(s, z)) ¬last(w) = (s', pass(s, z)) ] ] Suppose the user s1 S has the right to execute pass(s2, z), s2 S, z Z, so for all sequences w, cando(w, s1, pass(s2, z)) is true. Initially, s2 does not have the right to execute z; thus, cando(n, s2, z) is true. Now, let z' Z be such that (s3, z'), s3 S, is noninterfering with (s2, z); in other words, for each wn with vn = (s3, z'), cando(wn, s2, z) = cando(wn–1, s2, z). Then this policy says that for all s S: proj(s, ((s2, z), (s1, pass(s2, z)), (s3, z'), (s2, z)), si) = proj(s, ((s1, pass(s2, z)), (s3, z'), (s2, z)), si) So s2's first execution of z does not affect any subject's observation of the system.

8.2.4 Composition of Deterministic Noninterference-Secure Systems

As noted earlier, Gougen and Meseguer [412] assume that the output is a function of the input. This implies determinism, because a nondeterministic mapping (that is, one with two or more elements of the range corresponding to one element of the domain) is not a function. It also implies uninterruptibility, because differences in timing of interrupts can result in differences in state, and hence in output. For example, suppose a user enters a command to delete a file. This appears to take some time, so the user interrupts the command. If the interrupt occurs before the deletion, the system will be in a different state than if the interrupt occurs after the deletion (but before the command can terminate properly).

McCullough [673] has examined the implications of the determinism for composing systems. Consider composing the following systems. Systems Louie and Dewey compute at the LOW level. System Hughie computes at the HIGH level. The composed system has one output buffer, b_L, which anyone can read. It also has one input buffer, b_H, which receives input from a HIGH source. Three buffers connect the three systems. Buffer b_LH connects Louie to Hughie, and buffer b_DH connects Dewey to Hughie. Dewey and Louie write to these buffers, and Hughie reads from them. Both Dewey and Louie can write to the third buffer, b_LDH, from which Hughie can read. Figure 8-2 summarizes this composition. Note that all three systems are noninterference-secure. Hughie never outputs anything, so its inputs clearly do not interfere with its (nonexistent) outputs. Similarly, neither Dewey nor Louie input anything, so their (nonexistent) inputs do not interfere with their outputs.

If all buffers are of finite capacity, and blocking sends and receives are used, the system is not noninterference-secure. Without loss of generality, assume that buffers b_DH and b_LH have capacity 1. Louie cycles through the following algorithm.

Dewey follows the same algorithm, but uses b_DH for b_LH and writes a 1 to b_L. Hughie reads a bit from b_H, receives a message from b_LH (if the bit read from b_H is 0) or from b_DH (if the bit read from b_H is 1), and finally does a receive on b_LDH (to wait for the buffer to be filled).

Suppose Hughie reads a 0 from b_H. It reads a message from b_LH. At that point, Louie's second message can go into the buffer and Louie completes step 2. Louie then writes a 0 into b_L. Dewey, meanwhile, is blocked at step 1 and so cannot write anything to b_L. A similar argument shows that if Hughie reads a 1 from b_H, a 1 will appear in the buffer b_L. Hence, a HIGH input is copied to a LOW output.

So, even though the systems are noninterference-secure, their composition is not. Exercise 3 examines the influence of the requirement that buffers be finite and of the use of blocking sends and receives.