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, and we are welcoming feedback.
The code is documented here.
Tutorials are under way …