Goal-Oriented, B-Based Formal Derivation of Security Design Specifications from Security Requirements

This paper proposes a requirements-driven security engineering approach for modeling, specifying, and analyzing application-specific security requirements that are formally derived into security design specifications preserving security requirements properties. The approach adopts and non-trivially extends the goal-oriented KAOS (Knowledge Acquisition in automated Specifications) framework developed by Lamsweerde to formally construct a complete, consistent, and clear security requirements model. The resulting model is then extended using the B method to produce security design specifications and further implementation while preserving requirements properties. In our approach, we firstly transform the KAOS requirements model to an abstract B model and secondly, we refine the model using B refinement mechanism to generate design specifications and implementation. This unique treatment of secure software engineering is systematic, constructive and considers security early in the development lifecycle while ensuring no loss of the security requirements properties of completeness, consistency and clarity at later development phases. Moreover, our approach allows for requirement traceability at the various phases of development.