Reusable Formal Models for Threat Specification, Detection, and Treatment.

One of the main challenges in engineering secure software systems is the formalization of threats for the automation of security architecture threat detection, analysis, and mitigation. On top of that, there is a growing need for the development of reusable security solutions to support secure systems engineering at early stages of development. We address this challenge by proposing an integrated approach for threat specification, detection, and treatment in component-based software architecture models via reusable security threat and requirement formal model libraries. Our solution is based on metamodeling techniques that enable the specification of the software architecture structure and on formal techniques for the purposes of precise specification and verification of security aspects as properties of a modeled system. To validate our work, we explore a set of representative threats from categories based on Microsoft's STRIDE threat classification in the context of secure component-based software architecture development. In addition, we use model-driven engineering techniques for the development of a tool suite to support our approach.