Building a secure software system is difficult and requires significant expertise and effort. A secure system requires a secure design, a secure implementation of that design, and a secure platform on which the implementation executes. Furthermore, it must also provide assurances about its security properties. Security patterns have been proposed to help the design of secure systems. However, security patterns are written independently of the specifics of the underlying platforms. This leaves a gap between security patterns and the underlying platform. Furthermore, composition of security patterns is challenging because each pattern uses different design elements and may target different security requirements. The aim of this research is to improve our understanding of the design of high assurance secure applications. The main contributions of this thesis are a pattern-based composition approach to incrementally build and verify application designs. The approach reuses security knowledge from security patterns, and security mechanisms from secure underlying platforms. I propose the concept of a design fragment as an instantiation of a security pattern for a specific platform. This allows for design-level verification to provide assurance about security properties. Six primitive operations are provided for composition and are proven to preserve confidentiality. A collection of 279 security patterns from existing literature is synthesized. Each pattern is defined in a new security pattern template which is based on previous pattern templates. The contributions are evaluated using two case studies from different domains, a Continuous Deployment (CD) pipeline and an electricity Smart Meter. These case studies show that the approach applies across different domains. The design fragments and their verification procedures are reusable and the composition tactics are sufficient to express steps in the design of a secure software system.
展开▼
