8.3 Nondeducibility

Gougen and Meseguer [412] characterize security in terms of state transitions. If state transitions caused by high-level commands interfere with a sequence of transitions caused by low-level commands, then the system is not noninterference-secure. But their definition skirts the intent of what a secure system is to provide. The point of security, in the Bell-LaPadula sense, is to restrict the flow of information from a high-level entity to a low-level entity. That is, given a set of low-level outputs, no low-level subject should be able to deduce anything about the high-level outputs. Sutherland [984] reconsidered this issue in these terms.

Consider a system as a "black box" with two sets of inputs, one classified High and the other Low. It also has two outputs, again, one High and the other Low. This is merely a reformulation of the state machine model, because the inputs drive the commands used to create state transitions and generate output. However, the difference in view allows a more intuitive definition of security.

If an observer cleared only for Low can take a sequence of Low inputs and Low outputs, and from them deduce information about the High inputs or outputs, then information has leaked from High to Low. The difference between this notion and that of noninterference is subtle.

EXAMPLE: Revisit the two-bit system. When operations are executed by High, only the High state bit changes, and the same is true for Low. Let s0 = (0, 0). The commands are (Holly, xor1), (Lucy, xor0), (Lucy, xor1), (Lucy, xor0), (Holly, xor1), and (Lucy, xor0), and both bits are output after each command. So, the output string (which includes the initial state) is 00101011110101, the even-numbered bits being Low and the odd-numbered bits being High. These functions are not noninterference-secure with respect to Lucy. Because Lucy is cleared only for Low, she sees the output string as 0001111. But deleting the High commands would produce the string 00111 for Lucy, which is different (and thereby violates Definition 8–4). However, given the string 00111, Lucy cannot deduce what instructions were deleted because they do not affect the values in the output string; the deletions only affect its length. Hence, this version of the two-bit system is secure with respect to the property described above.

We now formalize this notion of "secure." In what follows, it suffices to consider the Low user deducing information about the High inputs, because the High inputs and Low inputs define the High outputs.^[3]

^[3] When outputs contain High information that is not a function of the inputs, high-level outputs need to be protected [431]. Such systems are not common, so we explicitly exclude them from this analysis.

Definition 8–10. An event system is a 4-tuple (E, I, O, T), where E is a set of events, I E is a set of input events, O E is a set of output events, and T is the set of all possible finite sequences of events that are legal within the system. The set E is also partitioned into H, the set of High events, and L, the set of Low events.

The sets of High inputs and outputs are H I and H O, respectively; the sets of Low inputs and outputs are L I and L O. Let T_Low contain the set of all possible finite sequences of Low events that are legal within the system.

Define a projection function p_L: T T_Low that deletes all High inputs from a given trace. Then a Low observer should be unable to deduce anything about the set of High inputs from a trace t_Low T_Low. In other words, given any such t_Low, the trace t T that produced t_Low is equally likely to be any trace such that p(t) = t_Low. More formally:

Definition 8–11. A system is deducibly secure if, for every trace t_Low T_Low, the corresponding set of high-level traces contains every possible trace t T for which p_L(t) ₌ t_Low.

EXAMPLE: Consider the two-bit machine in Section 8.2, and assume that xor0 and xor1 apply to both the High and Low bits and that both bits are output after each command. For notational convenience, the first input at each level is the initial state; successive inputs of 0 and 1 correspond to xor0 and xor1, respectively. The first two inputs will be at the High and Low levels. The sequence of inputs 1H010H10 occurs (where a subscript H indicates a High input and unsubscripted numbers indicate a Low input). Then the output will be 1001011010 (where the odd-numbered bits are Low and the even bits High). Lucy will see this as 01100. She knows that the first input was 0, the second was 1, and the third is not visible. However, the result is to leave the 1 unchanged; knowing the operation of the system, Lucy deduces that the High input was 0 (because 1 xor 0 = 1 and 1 xor 1 = 0). Hence, this system is not deducibly secure. Now assume that the xor0 and xor1 apply only to the Low or High bits depending on whether the user executing them is at the Low or High state, respectively. Then the output sequence of the inputs above is 1011111011; Lucy will see this as 01101. However, she can deduce nothing about the High inputs; any of the input sequences 0H010H10, 01H0101H10, 1H010H10, or 1H011H10 could have produced the Low output sequence. Hence, this system is deducibly secure.

8.3.1 Compositon of Deducibly Secure Systems

In general, systems that are deducibly secure are not composable [673]. However, the following modification appears to eliminate the problem that arose during composition of noninterference-secure systems.

Definition 8–12. Strong noninterference is the property of deducible security augmented by the requirement that no High-level output occurs unless a High-level input causes it.

EXAMPLE: The two-bit machine that applies operations only to the state bit with the appropriate level, and outputs both High and Low state bits after each operation, does not meet the strong noninterference property even though it is deducibly secure. But if it only outputs the bit at the level of the operation, it will meet the strong noninterference property.

Weber^[4] has shown that systems meeting the strong noninterference property are composable. But this property is too restrictive, in the sense that it forbids systems that are obviously secure.

^[4] See [673], p. 183.

EXAMPLE: [673] The system up takes low-level inputs and emits them as high-level outputs. This is clearly deducibly secure, because the low-level user sees no outputs (at either the high or low level). However, it does not meet the requirement of strong noninterference, because there are no high-level inputs.