Binary-level Code Analysis: Benefits, Challenges and Some Results

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 for security.

In this talk, we will present some of the challenges faced by formal methods and program analysis, especially symbolic execution, in the context of binary-level security as well as early results and achievements, based on recent works on decompilation, vulnerability analysis and adaptation of SMT solving to security issues.

Sébastien Bardin obtained his PhD in 2005 at Ecole Normale Supérieure de 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, automatic software verification and constraint solving. For several 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, vulnerability detection & assessment, code protection 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 regularly presents his work at top-tiers international conferences in Formal Methods, Security and Software Engineering. He has served as a PI for several research projects on binary-level security analysis, and he is regularly invited to international events and to security-related summer schools.