8.4 Generalized Noninterference

The preceding discussion of noninterference tacitly assumed that the systems involved were deterministic. Specifically, input and output were synchronous. Output depended only on commands triggered by input, and input was processed one datum at a time. This does not model real systems, where asynchronous events (inputs and commands) are the rule rather than the exception.

McCullough [672, 673] generalized noninterference to include nondeterministic systems; such systems that meet the noninterference property are said to meet the generalized noninterference-secure property. McCullough also pointed out that noninterference security is more robust than nondeducible security. Minor changes of assumptions can affect whether or not a system is nondeducibly secure. The following example illustrates this point.

EXAMPLE: Consider a system with two levels (High and Low), two users (Holly, who is cleared for High, and Lucy, who is at the Low level), and one text file at the High level. This file has a fixed size, and the special text symbol marks those locations that are empty (unused). Holly can edit the file. Lucy can execute a program that does the following (where char_in_file[n] returns the nth character in the file): while true do begin n := read_integer_from_user; if n > file_length or char_in_file[n] = then print random_character; else print char_in_file[n]; end; This system is not noninterference-secure, because the high-level inputs (the changes that Holly makes to the text file) affect the low-level outputs. However, the system is deducibly secure if Lucy cannot deduce the contents of the file from the program outputs. If the output of the program is meaningful (for example, "This book is interesting") or can be made meaningful (for example, "Thqs book ir interexting"), then the system is not nondeducibly secure; otherwise, it is. This sensitivity to assumption requires that deducible security be carefully defined in terms of allowed inferences, and that assumptions be made explicit.

8.4.1 Composition of Generalized Noninterference Systems

Composing systems that meet the generalized noninterference-secure property does not necessarily produce systems that meet this property. McCullough's demonstration [673] provides insight into both the nature of generalized nonrestrictiveness and the characteristics that make it noncomposable.

Consider a machine cat, which has two levels, HIGH and LOW, of inputs and outputs. (See Figure 8-3.) Inputs may come from the right or left, and outputs may go to the right or left. The machine accepts HIGH inputs. The HIGH inputs are output on the right, and after some number of inputs, the machine emits two LOW outputs, the first a stop_count output and the second a 0 or a 1, the former if an even number of HIGH inputs and outputs occur, and the latter if an odd number of HIGH inputs and outputs occur.

Cat is noninterference-secure. If there is an even number of HIGH inputs, the output could be 0 (meaning an even number of outputs) or 1 (meaning an odd number of outputs). If there is an odd number of HIGH inputs, the output could be 0 (meaning an odd number of outputs) or 1 (meaning an even number of outputs). So the high-level inputs do not affect the output, as required.

Now define a machine dog to work like cat, with the following changes:

• Its HIGH outputs are to the left.

• Its LOW outputs of 0 or 1 are to the right.

• stop_count is an input from the left, causing dog to emit the 0 or 1.

This machine is summarized in Figure 8-4.

As with cat, dog is noninterference-secure. When stop_count arrives, there may or may not be inputs for which there are not yet corresponding outputs. Hence, the high-level inputs do not affect the low-level output, just as for the machine cat.

Compose these two noninterference-secure machines. (See Figure 8-5.) We require that once an output is transmitted from cat to dog (or vice versa), it arrives. However, the stop_count message may arrive at dog before all input messages have generated corresponding outputs. Suppose cat emits 0 and dog emits 1. Then an even number of HIGH inputs and outputs have occurred on cat, and an odd number on dog. Because every HIGH input on cat is sent to dog, and vice versa, several scenarios arise:

So, if the composite machine catdog emits a 0 to the left and a 1 to the right, it must have received at least one input from the left. A similar result holds if catdog emits a 1 to the left and a 0 to the right.

It can also be shown (see Exercise 7) that if the outputs from both sides are the same, catdog has received no inputs from the left. Thus, the HIGH inputs affect the LOW outputs, and so the machine catdog is not noninterference-secure.

Zakinthinos and Lee [1069] proved some interesting results related to the composition of noninterference-secure systems. They center their results on the absence of feedback. Intuitively, once information flows from one component to another, no information flows from the second component back to the first.

Definition 8–13. Consider a system with n distinct components. Components c_i and c_j are connected if any output of c_i is an input to c_j. If for all c_i connected to c_j, c_j is not connected to any c_i, then the system is a feedback-free system.

In other words, for all pairs of components, information can flow in only one direction. Zakinthinos and Lee prove the following theorem.

Theorem 8–3. A feedback-free system composed of noninterference-secure systems is itself noninterference-secure.

Proof See [1069].

Feedback can be allowed under specific conditions. If at least one low-level input or output occurs before any high-level output is translated into a high-level input, then noninterference is preserved.

Lemma 8–3. A noninterference-secure system can feed a high-level output o to a high-level input i if the arrival of o (at the input of the next component) is delayed until after the next low-level input or output.

Proof See [1069].

This lemma leads to the following theorem.

Theorem 8–4. A system with feedback as described in Lemma 8–3 and composed of noninterference-secure systems is itself noninterference-secure.

Proof See [1069].