Specification, detection, and treatment of STRIDE threats for software components: Modeling, formal methods, and tool support

The existence of security threats in software designs can significantly impact the safe and reliable operation of systems. Threats need to be precisely specified before a tool can manipulate them, and though several approaches for threat specification have been proposed, they do not provide the scalability and flexibility required in practice. We take this problem towards an integrated approach for threat detection and treatment by means of security requirements, during the software architecture design time. The general idea of the approach is to: (1) specify threats as properties of a modeled system in a technology-independent specification language; (2) express conditions that reveal these threats in a suitable language with automated tool support for threat detection through model verification; and (3) suggest a set of security requirements to protect against detected threats. The formalized threats and security requirements are then provided as formal model libraries to foster reuse. 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 set to support our approach.