State Machine Model Assume a state machine of the type discussed in Section 9.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 σj, there is an element cm ∈ C* such that T* (cm, σj) = σn, where σn ≠ σj. There exists an equivalence relation ≡ such that: If the system is in state σi and a sequence of HIGH inputs causes a transition from σi to σj, then σi ≡ σj. If σi ≡ σj and a sequence of LOW inputs i1, ..., in causes a system in state σi to transition to state , then there is a state such that and the inputs i1, ..., in cause a system in state σj to transition to state Let σi ≡ σj. If a sequence of HIGH outputs o1, ..., on indicates a system in state σi transitioned to state , then for some state with , a sequence of HIGH outputs indicates a system in state σj transitioned to state Let σi ≡ σj, let c and d be HIGH output sequences, and let e be a LOW output. If the output sequence ced indicates that a system in state σi transitions to state , then there are HIGH output sequences c′ and d ′ and a state such that c′ed′ indicates that a system in state σj transitions to state 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 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 commands. The second part concerns two different states with the same LOW projection. The states resulting from giving the same LOW commands to the two equivalent, original states have the same LOW projections. Taken together, the two parts of property 2 say that if two states are equivalent, HIGH commands do not affect the LOW projection of the states . Only LOW commands affect the LOW projections. Property 3 says that HIGH outputs do not indicate changes in the LOW projections of states. Property 4 states that intermingled LOW and HIGH outputs cause changes in the LOW state that reflect the LOW outputs only. Assume that two states have the same LOW 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 projection. Hence, the LOW outputs indicate nothing about the HIGH state of the system; only the LOW state is visible, and regardless of the output sequence, the LOW projections of the two results are the same. Definition 9–14. A system is restrictive if it meets the four properties above. 9.5.2 Composition of Restrictive Systems Intuitively, the problem with composition of generalized noninterference-secure systems is that a HIGH output followed by a LOW output may not have the same effect as the LOW 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 μ1i (1 ≤ i ≤ n1) be the states of M1 and let μ2i (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 (μ1a, μ2a) to (μ1b, μ2b) if any of the following conditions holds: When M1 is in state μ1a and e occurs, M1 transitions to state μ1b; e is not an event for M2; and μ2a = μ2b. When M2 is in state μ2a and e occurs, M2 transitions to state μ2b; e is not an event for M1; and μ1a = μ1b. When M1 is in state μ1a and e occurs, M1 transitions to state μ1b; when M2 is in state μ2a and e occurs, M2 transitions to state μ2b; 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 9–15. (σa, σb) ≡ C (σc, σd) if and only if σa ≡ σc and σb ≡ σd. The equivalence relation ≡ C corresponds to the equivalence relation in property 2 for the composite system. From these, can you prove that the system resulting from the composition of two restrictive systems is itself restrictive?
Restrictiveness
The problem with the preceding composition is the need for a machine to act the same way whether a LOW input is preceded by a HIGH input, a LOW 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 input precedes stop count, dog may emit either a 0 or a 1.
State Machine Model
Assume a state machine of the type discussed in Section 9.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 σj, there is an element cm ∈ C* such that T* (cm, σj) = σn, where σn ≠ σj.
There exists an equivalence relation ≡ such that:
If the system is in state σi and a sequence of HIGH inputs causes a transition from σi to σj, then σi ≡ σj.
If σi ≡ σj and a sequence of LOW inputs i1, ..., in causes a system in state σi to transition to state
, then there is a state
such that
and the inputs i1, ..., in cause a system in state σj to transition to state
Let σi ≡ σj. If a sequence of HIGH outputs o1, ..., on indicates a system in state σi transitioned to state
, then for some state
with
, a sequence of HIGH outputs
indicates a system in state σj transitioned to state
Let σi ≡ σj, let c and d be HIGH output sequences, and let e be a LOW output. If the output sequence ced indicates that a system in state σi transitions to state
, then there are HIGH output sequences c′ and d ′ and a state
such that c′ed′ indicates that a system in state σj transitions to state
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 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 commands. The second part concerns two different states with the same LOW projection. The states resulting from giving the same LOW commands to the two equivalent, original states have the same LOW projections. Taken together, the two parts of property 2 say that if two states are equivalent, HIGH commands do not affect the LOW projection of the states . Only LOW commands affect the LOW projections.
Property 3 says that HIGH outputs do not indicate changes in the LOW projections of states. Property 4 states that intermingled LOW and HIGH outputs cause changes in the LOW state that reflect the LOW outputs only. Assume that two states have the same LOW 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 projection. Hence, the LOW outputs indicate nothing about the HIGH state of the system; only the LOW state is visible, and regardless of the output sequence, the LOW projections of the two results are the same.
Definition 9–14. A system is restrictive if it meets the four properties above.
9.5.2 Composition of Restrictive Systems
Intuitively, the problem with composition of generalized noninterference-secure systems is that a HIGH output followed by a LOW output may not have the same effect as the LOW 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 μ1i (1 ≤ i ≤ n1) be the states of M1 and let μ2i (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 (μ1a, μ2a) to (μ1b, μ2b) if any of the following conditions holds:
When M1 is in state μ1a and e occurs, M1 transitions to state μ1b; e is not an event for M2; and μ2a = μ2b.
When M2 is in state μ2a and e occurs, M2 transitions to state μ2b; e is not an event for M1; and μ1a = μ1b.
When M1 is in state μ1a and e occurs, M1 transitions to state μ1b; when M2 is in state μ2a and e occurs, M2 transitions to state μ2b; 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 9–15. (σa, σb) ≡ C (σc, σd) if and only if σa ≡ σc and σb ≡ σd.
The equivalence relation ≡ C corresponds to the equivalence relation in property 2 for the composite system.
From these, can you prove that the system resulting from the composition of two restrictive systems is itself restrictive?
Trending now
This is a popular solution!
Step by step
Solved in 3 steps
