BINSEC: Binary-level semantic analysis to the rescue
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 they are still relatively poorly tooled – essentially syntactic static analysis (disassembly) which is easy to fool, or dynamic analysis (fuzzing, monitoring) which may miss 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.
The open-source BINSEC platform humbly tries to fulfill part of this gap, by providing state-of-the-art binary-level semantic analyses. The platform is built around a concise and generic Intermediate Representation, making it easy to support new architectures and add new analyses. The main analyses so far include a dynamic symbolic execution engine enabling to discover new subtle behaviours in an executable file, and a semantic static analysis engine able to reason about all paths of a portion of the code under analysis.
In this this talk, we will present the platform and highlight the key technologies behind the platform, through a few examples taken from deobfuscation and vulnerability analysis.
The BINSEC project is a joint effort involving CEA, INRIA, LORIA, Université de Grenoble-Alpes and Airbus Group. The project is still in its infancy (first release Spring 2016) and under heavy development. While it is primarily a research tool, we want to make it robust enough so that adventurous hackers can take advantage from it.
Sébastien Bardin
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 security. He is now 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.
