Binsec: Binary code analysis for more secure software

Binsec makes software more secure by running a formal analysis on the software’s executable code. Using state-of-the-art techniques developed by CEA-List, Binsec can identify vulnerabilities, errors, and malware and provide proof that a software application’s executable code is secure. This innovative open-source software has earned international recognition.


Bringing code analysis as close to the machine as possible

Binsec is a formal binary-code analysis tool designed to improve software security. It scans executable code for vulnerabilities, malware, and errors.

It was developed based on CEA-List’s advanced code analysis, formal methods, and security research. It can scan code running on all major hardware architectures—from x86 and ARM to RISC—including the most recent 64-bit versions of these architectures.

Binsec is developed in partnership with LORIA (a joint research unit of CNRS, Inria, and the University of Lorraine) and Grenoble-Alpes University. It is available under an open-source license.

An advanced, feature-rich solution that supports digital sovereignty

Binsec offers several major advantages:

  • State-of-the-art features for security, automated code analysis, and formal methods.
  • Well-known in the academic research community.
  • Original capabilities like covert channel analysis, binary-level proof, speculative behavior can be integrated into analyses, etc.

From vulnerability detection to reverse engineering of malware

Binsec can verify software even if the source code (or part of the source code) is not available, such as for off-the-shelf software and mobile apps. It can also be used for post-compilation verification to ensure that security properties have been maintained, or if a particularly strong guarantee (and formal proof) of security is required, for example.

Finally, Binsec is a powerful malware reverse-engineering tool that can be used to identify and counter obfuscation, a technique hackers use to make malware hard to detect.

Binsec world firsts

Binsec, with its advanced technology, is behind a number of world firsts:

  • Automated identification and simplification of protections on APT-class government malware (2017).
  • Automated binary-level security proof on an embedded kernel (2019).
  • Decompiled all Debian Linux C+ Assembler code, identifying more than 1,000 compliance flaws in a hundred packages (2019).
  • Covert channel analysis: first binary-level proof of security on 196 cryptographic implementations, with three vulnerabilities introduced at compile time identified (2020).
  • Patch-oriented fuzz testing campaign: 30 new bugs in open-source codes identified, including 7 common vulnerabilities (2020).

Learn more


Binsec/rel: efficient relational symbolic execution for constant-time at binary-level, Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk. Security and Privacy, S&P 2020.

Get rid of inline assembly through verification-oriented lifting, Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Laurent Mounier, Marie-Laure Potet. Automated software Engineering, ASE 2019.

Model Generation for Quantified Formulas: a Taint-based Approach, Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet. Computer-aided Verification, CAV 2018.

Arrays made simpler: an efficient, scalable and thorough preprocessing, Benjamin Farinier, Robin David, Sébastien Bardin, Matthieu Lemerre. Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2018.

Backward-bounded DSE: targeting infeasibility questions on obfuscated codes, Sébastien Bardin, Robin David, Jean-Yves Marion. Security and Privacy, S&P 2017.


Go to the Binsec page on Github.

À lire également

Focus areas

Cybersecurity: toward safety and privacy by design

Cybersecurity is at the heart of digital sovereignty, and an essential constituent of modern societies. As a crucial element for peace and security in cyberspace, it is an invisible but key enabler fo...
Read more