Symbolic Execution emerged in the mid-2000 and was rapidly adopted by the research community as a tool of choice for bug hunting and automated testing. We consider the general problem of binary- level security investigations, such as vulnerability analysis over third-party components, side channel attacks or malware reverse. While standard symbolic execution can be useful here, security is not safety and, while still useful, a direct adaptation of symbolic execution to security scenarios remains limited in its scope.

In this tutorial, we will show how symbolic execution can be effectively adapted for the case of binary-level security. We will present some challenges symbolic execution faces in this highly demanding field of application, and report on several results and recent achievements toward adapting Symbolic Execution to binary-level security. We will first cover the basics of symbolic execution, how to adapt it and to optimize it for binary-level analysis. Then we will present some of the new challenges faced by formal methods and program analysis in the context of code-level security scenarios. Finally, we will present two security-oriented extensions of symbolic execution, the semi-relational symbolic execution (detection of leaks and side channel attacks) and the adversarial symbolic execution (considering an active code-level attacker).