Sébastien BARDIN CEA - Researcher position at the Software Safety & Security Lab of CEA (Saclay, Paris Area, France) Digital Security
Date: - Location: Eurecom
DIGITAL SECURITY TALK EURECOM ************** Time : 02:00pm , Tuesday 28 th of August Place : Room 151, level -1 , EURECOM Speaker : Sébastien BARDIN CEA Title: "Formal methods: from source-level safety to binary-level security" Abstract:Several major classes of security analysis have to be performed on raw executable files, such as vulnerability analysis of mobile code or commercial off-the-shelf, deobfuscation or malware inspection. These analysis are highly challenging, due to the very low-level and intricate nature of binary code, and there is a clear need for more sophisticated and automated tools than currently available syntactic and dynamic approaches. On the other hand, source-level program analysis and formal methods have made tremendous progress in the past decade, and they are now an industrial reality for safety-critical applications. Our long term goal is precisely to fulfill part of this gap, by developing state-of-the-art binary-level semantic analyses. In this talk, we first present the benefits of binary-level security analysis and the new challenges brought to formal methods, then we describe our early results and achievements, including the open-source BINSEC platform and its underlying key technologies as well as case-studies on deobfuscation and vulnerability analysis. Biography:Sebastien Bardin holds a researcher position at the Software Safety & Security Lab of CEA (Saclay, Paris Area, France). He works in the domain of formal methods and automatic program analysis. In a general way, he is interested in developing methods and tools that help achieving high level of confidence in trust-sensitive, software-intensive systems. He is currently interested in the application of formal methods to software security, with a strong focus on binary-level security analyses such as vulnerability detection & assessment, reverse engineering or malware deobfuscation. Hiw other current research interests include software testing, theorem proving, symbolic execution and static analysis. Before that, he prepared his Ph.D. in the Laboratoire Spécification et Vérification (ENS Cachan, Paris Area, France), where he worked on the verification of infinite state systems via symbolic model checking techniques.
