A general theory of composition for a class of “possibilistic” properties

Since the initial work of Daryl McCullough (1987) on the subject, the security community has struggled with the problem of composing “possibilistic” information-flow properties. Such properties fall outside of the Alpern-Schneider safety/liveness domain, and hence, they are not subject to the Abadi-Lamport Composition Principle. The paper introduces a set of trace constructors called selective interleaving functions and shows that possibilistic information-flow properties are closure properties with respect to different classes of selective interleaving functions. This provides a uniform framework for analyzing these properties, allowing us to construct both a partial ordering for them and a theory of composition for them. We present a number of composition constructs, show the extent to which each preserves closure with respect to different classes of selective interleaving functions, and show that they are sufficient for forming the general hook-up construction. We see that although closure under a class of selective interleaving functions is generally preserved by product and cascading, it is not generally preserved by feedback, internal system composition constructs, or refinement. We examine the reason for this