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.