BINSEC is the name of the tool platform produced by the BINSEC project. It is released under the terms of LGPL v2.1.


The general objective of the open-source BINSEC platform is to foster the next generation of binary-level analysis tools, by proposing binary-level semantic approaches, i.e. analysis methods based on the meaning of the program, and able to cover all of its behaviors – or at least a very significant part.

Our general philosophy consists in building on the success of source-level formal methods for safety analysis of critical systems, and adapting these results to binary-level security analysis. Besides, we follow a pragmatic way, exploring combinations of techniques and trade-offs, and we base our approach on a bedrock of basic analysis, complemented by dedicated domain-specific tools.

BINSEC offers the following features:

  • a formal Intermediate Representation (IR) well adapted to formal analysis;
  • basic syntactic disassembly techniques : recursive, linear and combination of both;
  • partial exploration of the behaviors of a given executable file (binary-level symbolic execution);
  • static analysis of all behaviors of a given executable file, in order to recover the high-level structure of a (non-obfuscated) binary code.

Currently, BINSEC only supports x86-32/ELF, with an experimental PE loader.


Feedback is welcome at binsec _at_


  • 20170301 0.1 (md5)

    Our first non-beta release. It’s still a work-in-progress, though, and we are welcoming feedback.


The code is documented here.

Tutorials are under way …