Formal analysis of software security system architectures

We present an approach for analysis of security system architecture. Constraint patterns are introduced to formally specify the generic form of security policies that all implementations of the system architecture must enforce. The analysis is driven by incrementally decomposing a system-wide constraint pattern into a set of constraint patterns of constituent components. Since there are potentially many ways to partition a security system, a key element of the analysis is to verify that the component constraint patterns are collectively consistent with the global constraint pattern under the given architecture. A “consistent” component constraint is then used as the basis for analyzing possible designs of the component. We show that our approach is both flexible and scalable, which not only ensures the consistency of critical early design decisions, but also provides a framework to guide correct implementations of the design