Applying noninterference to composition of systems: a more practical approach

As we know, current hookup or composable properties may impose over-strong security requirements on component systems. To overcome this problem, connectivities of the components have to be considered in order to appropriately handle their composition. Based on such a consideration, in this paper we adopt the concept of rely- and guarantee-conditions to present a composable property of noninterference. We enforce the requirement of noninterference only on some input-output entities of each component with regard to its connectivity, and communication constraints on its others so as to ensure that their entire system can satisfy noninterference. This enables the system and its components to possess different security properties, i.e. the security property of the system can be logically stronger than security properties of its components