An extension of classical noninterference security for deterministic
state machines, as introduced by Goguen and Meseguer and elegantly
formalized by Rushby, to nondeterministic systems should satisfy two
fundamental requirements: it should be based on a mathematically precise
theory of nondeterminism, and should be equivalent to (or at least not
weaker than) the classical notion in the degenerate deterministic case.
This paper proposes a definition of noninterference security applying
to Hoare's Communicating Sequential Processes (CSP) in the general case of
a possibly intransitive noninterference policy, and proves the
equivalence of this security property to classical noninterference
security for processes representing deterministic state machines.
Furthermore, McCullough's generalized noninterference security is shown
to be weaker than both the proposed notion of CSP noninterference security
for a generic process, and classical noninterference security for processes
representing deterministic state machines. This renders CSP noninterference
security preferable as an extension of classical noninterference security
to nondeterministic systems.
|