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:
Currently, BINSEC only supports x86-32/ELF, with an experimental PE loader.
Feedback is welcome at
binsec _at_ saxifrage.saclay.cea.fr
Our first non-beta release. It’s still a work-in-progress, though.
This release fixes the tarball issue of the initial beta. It also provides minor fixes to the x86 decoder and refactoring to the disassembly module.
This is our first public release. We are anticipating some rough edges, though, and are welcoming feedback.
The code is documented here.
Tutorials are under way …