Composing and decomposing systems under security properties

We investigate the formal relationship between separability of processes and the types of non-interference properties they enjoy. Though intuitively appealing, separability – the ability to define a process as a parallel composition of disjoint components – alone cannot adequately prove the absence of information flow. We present a number of laws for the composition of secure systems, and an example to show how such laws can be applied. Separability is an idea which has origin in the design of secure operating systems [Rus81]. Informally, a system is separable if its users (or user processes) can be isolated from each other. The purpose of this isolation is to achieve mutual non-interference between users. The separability condition has been formalised elsewhere (e.g. [Bur89, Jac90]), and we adopt the definition that a process is separable if equivalent to a parallel composition of sub-processes with disjoint alphabets. This condition is succinctly expressed in the process alge...

• Type: Conference
• Year: 1995
• Where: CSFW
• Authors: A. W. Roscoe, L. Wulf
• Keywords: CSFW 1995, Disjoint Components, Information flow, Parallel Composition, Security Privacy