The BinSec project is funded by the call Ingénierie Numérique & Sécurité - INS 2012 , a program of the Agence Nationale de la Recherche.

The global aim of the BINSEC project is to fill part of the gap between formal methods over executable code on one side, and binary-level security analyses currently used in the security industry. We target two main applicative domains: vulnerability analysis and virus detection. Two other closely related applications will also be investigated: crash analysis and program deobfuscation. For malware detection, we want to design signature methods robust to mutations and able to overcome obfuscation, especially self-modifying code. For vulnerability analysis, we want to develop techniques able to locate potential vulnerabilies in an executable file, and able to distinguish between simple crash bugs and exploitable bugs (exploitability). While a priori distinct, we claim that the different fields addressed in BINSEC share common basic problems and could benefit from similar advances in automated binary code analysis, such as precise recovery of control-flow or data-flow information, or low-level type inference. Finally, we will develop a common (lightweight) open-source infrastructure to ease the development of binary-level analysers and to allow commu- nication between prototypes through a common formal model.

Project structure

• WP1: requirements
• WP2: models and generic analysis for binary-level security
• WP3: vulnerability analysis
• WP4: malware analysis
• WP5: experimental evaluation

News

[04/07/2016] Beta release of tool
[16/10/2014] ANR midterm evaluation
[28/02/2014] First-year Plenary meeting
[15/02/13] Kick-off meeting