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 and binary-level security analyses currently used in the security industry.

We target two main applicative domains:

  • vulnerability analysis;
  • malware detection.

Two other closely related applications will also be investigated:

  • crash analysis;
  • 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 analyzers and to allow communication 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