A threat-driven approach to modeling and verifying secure software

12 years 1 months ago
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 ...
Dianxiang Xu, Kendall E. Nygard
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where KBSE
Authors Dianxiang Xu, Kendall E. Nygard
Comments (0)