Detection of Security Flaws and Vulnerabilities by Guided Model Checking

The research problem addressed by this project is the development of tools for automated detection of security flaws. The focus of the project are security flaws that are instances of potential or actual vulnerabilities. A flaw may have been planted intentionally in the code or may merely be caused by a programming error. In this context, an attack (or intrusion) is a sequence of operations that exploits the vulnerability, typically intentionally.

As an overall goal, this project proposes to tailor state-space reduction algorithms to the code security domain, and thus, to develop specialized model checking algorithms for detecting security vulnerabilities. This project builds on the earlier work of the principal investigators and exploits an expressive modeling formalism (namely, state/event-based formalism) and efficient computational engines (namely, symbolic model checking, symbolic execution, SAT-solvers).

The focus of the project is:

1. collection of security-critical open source programs and classification of known vulnerabilities and security exploits;
2. formalization of exploitable behaviors and security policies for various benchmarks using state-event notation;
3. experimentation and quantitative evaluation using unguided software model checking on the collected benchmarks, and
4. state-space reduction techniques tailored to security domains.

This is a joint project between USI and ETHZ, funded by SNSF