Towards safe and productive development of secure software: FADES and model-based software engineering

Cost effective development of secure software is a key goal for many software organizations as they seek to manage the risks of misbehaving software. Employing Formal Methods (FMs) in the Model-Based Software Engineering (MBSE) paradigm that systematically produces software systems through modeling, simulation, reuse and automation provides a reasonable approach for developing highly secure software in a productive manner. MBSE approaches introduce some complexities at the beginning of the lifecycle, but save substantial time in production and delivery by identifying and resolving defects/errors early and reducing rework. On the other hand, the expertise needed for FMs and the concomitant costs often inhibit their wide employment in securing large and complex software systems. In this paper, we report our experience with Formal Analysis and Design for Engineering Security (FADES) an approach we introduced two years ago at this venue. Through systematic and automated transformation from semiformal requirements specifications to formal design, FADES facilitates embedding FMs into the development lifecycle of secure software systems. We outline the case studies and validation of FADES feasibility for the design and implementation of secure software systems. Promising experience with FADES was a necessary precursor to our work on generalizing FADES and our proposal to direct FADES toward being an MBSE approach. We discuss how the formality, transformation, reuse and automation in FADES may further enhance the MBSE-based production and delivery of secure software.