[ Changed 4th March 1997 ]
The ability to design and construct complex systems that enforce a security property presupposes an understanding of security properties themselves, as well as the security properties of a system that is composed from secure components. This talk will present a general theory of possibilistic security properties and of system composition for such properties.
It has been demonstrated that security properties do not fit into the saftey/liveness framework defined by Alpern and Schneider. That is, a security property can not be expressed as a property of a trace. (A trace is an ordered stream of events that can occur at the inputs and outputs of a component). However, we demonstrate that security properties can be expressed as a predicate over the set of all traces of a component that are consistent with a given low-level view of a trace.
The issue of composition with feedback has been the focus of much research, we demonstrate that the problem with feedback composition is related to the synchronization of the communications events between the various components. This allows us to provide necessary and sufficient conditions for determining when feedback composition will fail for Generalized Noninterference and for all properties stronger than Generalized Noninterference.
An understanding of what is a security property allows us to provide a method of constructing a system that satisfies a desired security property. This analysis yields a condition that can be used to determine how a property may emerge under composition.