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 discuss several security-oriented extensions of symbolic execution, such as relational symbolic execution (detection of leaks and side channel attacks), adversarial symbolic execution (considering an active code-level attacker) or robust symbolic execution (trying to define and find meaningful bugs).

This tutorial will comprise a lecture and hands-on exercises on the open-source BINSEC platform https://binsec.github.io/.

Organization

• 1h30 lecture

• 1h30 hands-on

Main takeaways for the audience

• an exposure of the benefits and challenges of binary-level security analysis

• insights on how program analysis in general, and symbolic execution in particular, can be adapted to such scenarios

• hands-on experience on practical security cases with the BINSEC platform

The tutorial will be based on parts of the following material:

• Sébastien Bardin, Robin David, and Jean-Yves Marion. Backward-bounded DSE: targeting infeasibility questions on obfuscated codes. S&P 2017.

• L. Daniel, S. Bardin, and T. Rezk. Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. S&P 2020.

• Soline Ducousso, Sébastien Bardin, and Marie-Laure Potet. Adversarial reachability for program-level security analysis. ESOP 2023.

• Guillaume Girol, Benjamin Farinier, and Sébastien Bardin. Not all bugs are created equal, but robust reachability can tell the difference. CAV 2021.

• Guillaume Girol, Guilhem Lacombe, Sébastien Bardin. Quantitative Robustness for Vulnerability Assessment. PLDI 2024

• Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, Sébastien Bardin. Inference of Robust Reachability Constraints. POPL 2024

Biographies:

• Sébastien Bardin is a senior researcher at CEA LIST (Saclay, Paris Area, France), where he has initiated and now leads the binary-level security analysis group. His research interests lay at the crossroad of formal methods, program analysis, automated reasoning, software engineering and security. For a few years now, Sébastien has been interested in automating binary-level security analysis by lifting formal methods developed for the safety-critical industry, with applications to vulnerability analysis, reverse, deobfuscation and code protection. He particularly focuses on symbolic execution and he is the main designer of the (open-source) BINSEC platform for binary-level code analysis. Sébastien is associate editor of ACM TOPS and he co-chairs the French national working group on Formal Methods & Security.

• Frédéric Recoules graduated from INSA and Université Toulouse Paul-Sabatier in 2016, then received a PhD in Computer Science from Université Grenoble-Alpes in 2021. His area of expertises spans formal methods, low-level programming, decompilation and reverse engineering. He notably obtained an ICSE distinguished paper award and a 2nd best GDR GPL PhD award (thematic: software engineering, formal methods and programming languages) for his work on formal verification of inline assembly code. He is currently Research Engineer at CEA where he is the main developer and maintainer of the binary-level program analysis platform BINSEC. His research addresses scalability issues in symbolic analysis at binary level, vulnerability analysis and reverse engineering for security.