On the composition of security properties
E. S. Lee, A. Zakinthinos · 1997
This thesis presents a general theory of system composition for possibilistic security properties. It is shown that possibilistic security properties can be viewed as a predicate over the traces that are consistent with a low level observation $\rm\tau\sb{low}.$ We provide a uniform framework for analyzing and comparing these properties. We demonstrate how to determine what security property a system satisfies given the security properties satisfied by its constituent components. Also, we show how to construct 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. We examine the reasons for the failure of feedback composition and provide necessary and sufficient conditions for determining when feedback composition will fail for all properties based on Generalized Noninterference. Unwinding theorems are given for a large class of security properties.