Description
Date depot: 28 février 2019
Titre: Improving Software Security via Symbolic Execution
Directeur de thèse:
Aurelien FRANCILLON (Eurecom)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Symbolic execution has been used for bug finding with great success; it isparticularly useful in cases where simpler methods like random testing cannotreach relevant parts of a program under test. However, despite considerableimprovements, the technique still suffers from scalability problems which makeit unsuitable for many use cases in practice. Moreover, symbolic execution offirmware, i.e., software running inside embedded devices, poses a set ofadditional challenges. In my doctoral studies, I plan to advance the state ofthe art in symbolic execution with the goal of providing software developers atool that can detect faults in software before it is released. Specifically, Iwould like to focus on the interaction between symbolic execution engines andSMT solvers, as well as the symbolic interpreter. I believe that tighterinteraction between symbolic execution and the underlying reasoning engine canalleviate some of the scalability problems we are currently facing, and there ispotential in optimizing the code execution step. I hope thereby to contribute tothe field of software and firmware security at large.
Doctorant.e: Poeplau Sebastian