Formal methods: from source-level safety to binary-level security

Thursday, February 28, 2019, 11:00 am PDTiCal
MDR Conference Room 1135 (Large)
This event is open to the public.
ISI Seminar Talk
Dr. Sébastien Bardin, CEA
Video Recording:


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 analyses 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 first results and achievements, including the open-source BINSEC platform and its underlying key technologies as well as case-studies on deobfuscation and vulnerability analysis.

Speaker Bio:

Sébastien Bardin obtained his PhD in 2005 at ENS Cachan, France, in the field of formal methods. He joined CEA LIST, France, in 2006 as a full-time researcher, with research activities centered on program analysis and automatic software verification. For a few years now, Sébastien has been interested in automating software-level security analysis by lifting formal methods developed for the safety-critical industry. In particular, he focuses on binary-level formal methods (especially, symbolic execution, abstract interpretation and low-level constraint solving), vulnerability detection & assessment, and malware deobfuscation. He leads the /binary-level security/ group at CEA LIST where he is the main designer of the open-source BINSEC platform for binary-level code analysis. Sébastien has served as a PI for several research projects on binary-level security analysis (ANR BINCOA 2008-2012, DGA SASSE 2013-2016, ANR BINSEC 2013-2017). He is regularly invited to international events -- especially, the three Dagstuhl seminars on binary code analysis (2012, 2014, 2017) and the Nii Shonan meeting on binary-level security (2015), and to security-related summer schools  -- French Summer School on Cybersecurity (2016), International Summer School on Software protection (2017).

Institute Description:

CEA is the largest French applied research center, with activities ranging from energy and quantum physics to biology, neuroscience and computer science. It has been ranked 1st in 2016 Reuter's ranking of the most innovative public research institutes (2nd in 2017). CEA LIST is the IT department of CEA, focusing on factory of the future, cyber-physical systems, artificial intelligence and digital health.

The LSL Laboratory of CEA LIST has been conceiving and developing software verification tools for many years, and counts several successful industrial transfers, most notably its open source Frama-C platform used at Airbus, EDF and NASA. More recently, LSL has acquired a strong expertise in applying formal methods to software security (e.g., verification of PolarSSL, collaborations with Thales and Bureau Veritas), especially for binary-level security analysis through the BINSEC platform. LSL is also strongly involved in several validation- and security-related committees, both national (Allistene GT Cybersecurity) and European (ECSO GTs Certification & Roadmap).          

ISI Host:  Dr. Christophe Hauser, Networking and Cybersecurity Division


« Return to Upcoming Events