A communication policy is a specification for permitted communication among system agents. A system exhibits noninterference with respect to a policy if every agent is insensitive to the presence of agents with which it may not communicate. A communication policy specifies the presence or absence of communication between agents, but it does not specify how permitted communication may occur. In this paper we present a refinement of a communication policy, which we call a connection policy. A connection policy specifies the channels along which permitted communication may occur. A system observes controlled interference when its connection policy is satisfied. When a connection policy is consistent with a communication policy, controlled interference guarantees noninterference. We discuss Rushby's notion of separation. In light of controlled interference, and briefly relate controlled interference to type enforcement. The formalization of the controlled interference theory is built on the state-based formulation of noninterference previously developed by two of the authors. A theme of this paper is that a state-based approach to these issues is simple and useful.

Concurrency in Gypsy is based on a unique, formal approach to specifying and proving systems of concurrent processes. The specification and proof methods are designed so that proofs of individual processes are totally independent, even when operating concurrently. These methods can be applied both to terminating and non-terminating processes, and the proof methods are well suited to automated verification aids. The basic principles of these methods and their interaction with the design of Gypsy are described.