A general theory of composition for trace sets closed under selective interleaving functions

This paper presents a general theory of system composition for “possibilistic” security properties. We see that these properties fall outside of the Alpern-Schneider safety/liveness domain and hence, are not subject to the Abadi-Lamport composition principle. We then introduce a set of trace constructors called selective interleaving functions and show that possibilistic security properties are closure properties with respect to different classes of selective interleaving functions. This provides a uniform framework for analyzing these properties and allows us to construct a partial ordering 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