A GENERAL-THEORY OF COMPOSITION FOR A CLASS OF POSSIBILISTIC PROPERTIES

Since the initial work of Daryl McCullough on the subject, the securit y community has struggled with the problem of composing ''possibilisti c'' information-flow properties. Such properties fall outside of the A lpern-Schneider safety/liveness domain, and hence, they are not subjec t to the Abadi-Lamport Composition Principle. This paper introduces a set of trace constructors called selective interleaving functions and shows that possibilistic information-flow properties are closure prope rties with respect to different classes of selective interleaving func tions. This provides a uniform framework for analyzing these propertie s, allowing us to construct both a partial ordering for them and a the ory of composition for them. We present a number of composition constr ucts, show the extent to which each preserves closure with respect to different classes of selective interleaving functions, and show that t hey are sufficient for forming the general hook-up construction. We se e that although closure under a class of selective interleaving functi ons is generally preserved by product and cascading, it is not general ly preserved by feedback, internal system composition constructs, or r efinement. We examine the reason for this.