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.
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.
Binsec offers several major advantages:
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, with its advanced technology, is behind a number of world firsts:
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.
