Detection of Security Flaws and Vulnerabilities by Guided Model Checking

Information is an important strategic and operational asset, and, therefore, there is a need to have adequate security measures which can safeguard sensitive information.
Security of computer systems has multiple aspects ranging from cryptography to securing low level implementations. Most practical exploits are based on implementation flaws rather than on flaws of the cryptographic principles or protocols. Despite of its importance, there are no comprehensive research studies in securing the low level implementation. This project proposes to encompass information security, integrity, and availability problems in software by assuring security of the actual implementation given in a language such as ANSI-C.
Among the specific topics of interest are: 1) vulnerability assessment; 2) detection of exploitable software flaws; and consequently 3) protection from malicious code.
The existing techniques for ensuring security properties are mostly ad hoc and informal. In contrast, this project targets the development of techniques that are exhaustive and formally guarantee the correctness of security properties. Model Checking technology is a perfect candidate for this task.
Model Checking exhaustively explores the entire state-space for violations of the property of interest. However, Model Checking suffers from the state explosion problem, i.e., the size of the state-space often exceeds the capacity of the Model Checking tool. The main research challenge when applying Model Checking to large scale software therefore is to address the scalability problem. We propose to tailor state-space reduction algorithms to the code security domain, and thus, to develop specialized model checking algorithms for detecting security vulnerabilities.
The main idea is to derive guiding models for directing the search performed by the symbolic model checker towards areas that likely contain vulnerabilities, and to use the guidance to generate proofs of the absence of such vulnerabilities faster. The guiding techniques we propose to investigate are component local behavior, learning a regular language for normal behavior, and exploit patterns.