Connection Policies and Controlled Interference

摘要

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 upon 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.