Issue No.04 - July-Aug. (2012 vol.9)
Manghui Tu , Dakota State University, Madison
Michael Sanford , Dakota State University, Madison
Lijo Thomas , Dakota State University, Madison
Daniel Woodraska , Dakota State University, Madison
Dianxiang Xu , Dakota State University, Madison
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TDSC.2012.24
Security attacks typically result from unintended behaviors or invalid inputs. Security testing is labor intensive because a real-world program usually has too many invalid inputs. It is highly desirable to automate or partially automate security-testing process. This paper presents an approach to automated generation of security tests by using formal threat models represented as Predicate/Transition nets. It generates all attack paths, i.e., security tests, from a threat model and converts them into executable test code according to the given Model-Implementation Mapping (MIM) specification. We have applied this approach to two real-world systems, Magento (a web-based shopping system being used by many online stores) and FileZilla Server (a popular FTP server implementation in C++). Threat models are built systematically by examining all potential STRIDE (spoofing identity, tampering with data, repudiation, information disclosure, denial of service, and elevation of privilege) threats to system functions. The security tests generated from these models have found multiple security risks in each system. The test code for most of the security tests can be generated and executed automatically. To further evaluate the vulnerability detection capability of the testing approach, the security tests have been applied to a number of security mutants where vulnerabilities are injected deliberately. The mutants are created according to the common vulnerabilities in C++ and web applications. Our experiments show that the security tests have killed the majority of the mutants.
Keywords—Software security, threat modeling, security testing, software testing, model-based testing, Petri nets.
Manghui Tu, Michael Sanford, Lijo Thomas, Daniel Woodraska, Dianxiang Xu, "Automated Security Test Generation with Formal Threat Models", IEEE Transactions on Dependable and Secure Computing, vol.9, no. 4, pp. 525-539, July-Aug. 2012, doi:10.1109/TDSC.2012.24