Automated Security Test Generation with Formal Threat Models

摘要

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.