Using Composition and Refinement to Support Security Architecture Trade-Off Analysis

This paper demonstrates that composition and refinement techniques are a promising solution for performing rigorous, security architecture trade-off analysis. Such analysis typically occurs in one of two forms: comparing two architectures for implementation and determining the impact of change to an implemented architecture. Composition and refinement techniques reduce the overhead of such analysis significantly over traditional formal methods by facilitating specification and proof reuse and by providing powerful reasoning tools. In this paper, we propose an approach for applying composition and refinement techniques to trade-off analysis. Our approach relies on a formal composition and refinement framework, which is not described here. We describe the approach and apply it to a simple example. We conclude with lessons learned and future work.