Vulnerability Assessment Tool Using Model Checking

Research Summary: 

This activity focused on identification of potential vulnerabilities in software. We used a combination of symbolic execution and model checking to systematically analyze corruptions of application data and identify cases that can lead to successful attacks. The results from such analysis can be used to remove application-level vulnerabilities and guide design of defense mechanisms to protect applications from attacks. Our specific goal was to design a technique and a tool to discover vulnerabilities in an application. The core component of the approach we developed is SymPLFIED, a formal framework that uses symbolic execution and model checking to identify conditions under which an attacker can penetrate a system, to introduce memory errors and propagate the error’s consequences using symbolic execution and model checking, and to determine memory locations that need to be protected to prevent application failure or system compromise. The analysis conducted using the SymPLFIED-based formal framework allows generation of trusted signatures, which can be used to implement runtime checking. The tool was demonstrated on real-world applications, including embedded code and network applications, e.g., SSH.