|
|
|
The problem with the preceding composition is the need for a machine to act the same way whether a low-level input is preceded by a high-level input, a low-level input, or no input. The machine dog does not meet this criterion. If the first message to dog is stop_count, dog emits a 0. If a high-level input precedes stop_count, dog may emit either a 0 or a 1. McCullough used a state model to capture the criteria [673].
Assume a state machine of the type discussed in Section 8.2. Let the machine have two levels, Low and High.
Now consider such a system with the following properties.
For every input ik and state sj there is an element cm 
C* such that T*(cm, sj) = sn, where sn 
sj.
There exists an equivalence relation 
such that:
if the system is in state si and a high-level sequence of inputs causes a transition from si to sj, then si sj.
if si sj and a low-level sequence of inputs i1, …, in causes a system in state si to transition to state si', then there is a state sj' such that si' sj' and the inputs i1, …, in cause a system in state sj to transition to state sj'.
Let si sj. If a high-level sequence of outputs o1, …, on indicates a system in state si transitioned to state si', then for some state sj' with sj' si', a high-level sequence of outputs o1', …, om' indicates a system in state sj transitioned to state sj'.
Let si sj, let c and d be high-level output sequences, and let e be a low-level output. If the output sequence ced indicates that a system in state si transitions to state si', then there are high-level output sequences c' and d' and a state sj' such that c'ed' indicates that a system in state sj transitions to state sj'.
Property 1 says that T* is a total function and that inputs and commands always move the system to a different state.
Property 2 defines an equivalence relation between two states. The equivalence relation holds if the low-level projections of both states are the same. The first part of this property says that two states are equivalent if either is reachable from the other using only high-level commands. The second part concerns two different states with the same low-level projection. The states resulting from giving the same low-level commands to the two equivalent, original states have the same low-level projections. Taken together, the two parts of property 2 say that if two states are equivalent, high-level commands do not affect the low-level projection of the states (which is, of course, the same). Only low-level commands affect the low-level projections.
Property 3 says that high-level outputs do not indicate changes in the low-level projections of states. Property 4 states that intermingled low-level and high-level outputs cause changes in the low-level state that reflect the low-level outputs only. Assume that two states have the same low-level projection. If there is an output sequence leading from one of these states to a third state, then there is another output sequence leading from the other state to a fourth state, and the third and fourth states have the same low-level projection. Hence, the low-level outputs indicate nothing about the high-level state of the system; only the low-level state is visible, and regardless of the output sequence, the low-level projections of the two results are the same.
Definition 8–14. A system is restrictive if it meets the four properties above.
Intuitively, the problem with composition of generalized noninterference-secure systems is that a high-level output followed by a low-level output may not have the same effect as the low-level input, as we have seen. However, by properties 3 and 4, a restrictive system does not have this problem. Thus, the composition of restrictive systems should be restrictive.
Consider the following composition. Let M1 and M2 be two systems, and let the outputs of M1 be acceptable as inputs to M2. Let m1i (1 
i n1) be the states of M1 and let m2i (1 i n2) be the states of M2. The states of the composite machine are pairs of the states of each component. Let e be an event causing a transition. Then e causes the composite machine to change state from (m1a, m2a) to (m1b, m2b) if any of the following conditions holds.
When M1 is in state m1a and e occurs, M1 transitions to state m1b; e is not an event for M2; and m2a = m2b.
When M2 is in state m2a and e occurs, M2 transitions to state m2b; e is not an event for M1; and m1a = m1b.
When M1 is in state m1a and e occurs, M1 transitions to state m1b; when M2 is in state m2a and e occurs, M2 transitions to state m2b; and e is an input to one machine and an output from the other.
Intuitively, these conditions state that an event causing a transition in the composite system must cause a transition in at least one of the components. Furthermore, if the transition occurs in exactly one of the components, the event must not cause a transition in the other component system when it is not connected to the composite system.
Definition 8–15. (sa, sa)
The equivalence relation C corresponds to the equivalence relation in property 2 for the composite system.
From these, we can show:
Theorem 8–5. The system resulting from the composition of two restrictive systems is itself restrictive.
Proof See Exercise 8.
|
|
|
| Top |