http://sebastien.bardin.free.fr/
sebastien.bardin@cea.fr
CEA LIST, Safety & Security Lab
Titre Binary-level program analysis and its applications to security
Résumé
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 very challenging, due to the very low-level and intricate nature of binary code, and currently they are still relatively poorly tooled — essentially syntactic static analysis (disassembly) which are easy to fool, or dynamic analysis (fuzzing, monitoring) which miss many subtle behaviors. 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. This lecture will discuss the challenges and benefits of adapting program analysis techniques from source-level safety to binary-level security. Especially, we will focus on vulnerability detection (« smart fuzzing »), exploitability assessment and deobfuscation, and we will present some recent formal techniques for binary-level analysis, such as concise formal intermediate representations or binary-level symbolic execution.
Bio
Sébastien Bardin joined CEA LIST, France, in 2006 as a full-time researcher. Since then, its main research interests are the automatic analysis of executable files — from a safety point of view at first, and now from a security point of view, automatic white-box testing through symbolic execution and low-level constraint solving. He is one of the main designers and developers of the binary-level symbolic execution tool OSMOSE (2008), and the Principal Investigator of the ANR projects BINCOA (2009-2012) and BINSEC (2013-2017) about binary-level program analysis, for safety and for security. He is also one of the main designers of the (open-source) BINSEC platform for binary-level code analysis, to be released in Spring 2016.
Sébastien Bardin obtained his PhD in 2005 at ENS Cachan, France, under the guidance of Pr. Alain Finkel. His doctoral work was centered on the verification of infinite-state systems by means of model checking, symbolic representations and loop acceleration. He also co-developed the infinite-state model-checker FAST.
