Symbolic Execution, from Software Testing to Security Analysis
Symbolic Execution is a recent and fruitful approach to automatic code-based test generation, having already detected many (acknowledged) bugs in several classes of software, such as drivers or media readers. The key idea behind Symbolic Execution is that, considering a path of the program under analysis, it is often possible to build a *path predicate* for that path, i.e. a formula whose solutions correspond exactly to the program input exercising that path at run time. Then, solving the path predicate yields input that effectively cover the path, and enumerating over all (bounded) paths allows for a systematic exploration of the program behaviors. This talk intends to give an overview of Symbolic Execution and of its applications to software testing and security.
First, we will present the key ideas and algorithms behind the technique, as well as the current state of the art.
Then, we will discuss the problem of using Symbolic Execution for generating test suites satisfying complex coverage criteria such as those found in software testing, introducing the Frama-C/LTest testing prototype for C programs.
Finally, we will present a few applications of Symbolic Execution to binary-level security analysis, introducing the BINSEC/SE prototype.
Thème(s) : Conférences Recherche