Formal Methods-Based Software Test Design for Pseudo-Exhaustive Error Checking
Abstract
Technological advances enabled by digital engineering allow the United States to maintain its military superiority in an increasingly competitive world. However, the power of digital engineering comes at a price. Apart from the cyber vulnerabilities created by the networked nature of its digital systems, these systems are also only as secure, reliable, and resilient as the software inside them. In the past few decades, flaws and vulnerabilities in software led to devastating accidents and breaches that compromised personal information, cost billions of dollars, and sometimes led to loss of life. In order to meet the Department of Defenses goals of better characterizing the security and reliability of the software in its systems, this research builds upon techniques and ideas from formal methods research, design of experiments, complexity theory, and greybox fuzzing and demonstrates the effectiveness of the resulting test sets against bug-seeded modules of the Traffic Collision Avoidance System (TCAS) software used in commercial aviation. Two new powerful approaches to guided testing are described: the RBCA method that leverages the power of covering arrays while providing the reach of random testing; and the Hamming approach that generates powerful test sets by manipulating a known good seed input. We describe a new type of automated random tester - a "fuzzer" - that uses machine learning to continuously train the hamming algorithm to generate more powerful test sets as it acquires more information.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 03, 2023
- Accession Number
- AD1223452
Entities
People
- Chris Mccormack
- Jackson R. Mayo
- Jinseo Lee
- Laura Epifanovskaya
- Reg Meeson
- Robert C. Armstrong
Organizations
- Institute for Defense Analyses