Goal-Oriented Software Security Engineering: The Electronic Smart Card Case Study

We advocate goal-oriented software security engineering to produce highly secure software in a constructive,provable and cost-effective manner. Our approach is to couple goal-oriented semi-formal requirements specifications with formal design and implementation. To this effect, we proposed FADES (formal analysis and design for engineering security)in as the first goal-oriented software security engineering approach that provides a systematic and automated bridge between the goal-directed semi-formal KAOS (knowledge acquisition for automated specifications) framework and the B formal method to derive formal design and implementation from security requirements. In this paper, we demonstrate the applicability of FADES and study its effectiveness through a generic Electronic Smart Card case study and a comparative analysis between FADES and strictly applying formal methods.We use the case study to demonstrate how the goal-oriented formulation of security requirements in FADES paves the way for formal design that provably preserves the security properties.Further, the results of the comparison between FADES and Z show that FADES achieves better requirements completeness,consistency and security quality.