A threat-driven approach to modeling and verifying secure software

This paper presents a formal approach to threat-driven modeling and verification of secure software using aspect-oriented Petri nets. Based on the behavior model of intended functions, we identify and build formal models of security threats, which are potential misuses and anomalies of the intended functions that violate security goals. Threat mitigations are further modeled in an aspect-oriented paradigm. Taking Petri nets as a formal basis for modeling behaviors, threats, and mitigations as a whole, we verify properties of and consistency between behaviors and threats, and absence of identified threats from the integrated model of functions and threat mitigations. This makes it possible to achieve a design that is provably resistant to the anticipated threats and thus reduce significant design-level vulnerabilities. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software and program verification – formal methods, correctness proofs. F.3.1 [Logics and Meanings of ...

• Type: Conference
• Year: 2005
• Where: KBSE
• Authors: Dianxiang Xu, Kendall E. Nygard
• Keywords: Aspect-oriented Petri Nets, KBSE 2005, Petri Nets, Software Engineering, Threat Mitigations