Binsec renforce la sécurité des logiciels en analysant de manière formelle leur code exécutable. Il met en œuvre des techniques à la pointe de la recherche pour détecter la présence de vulnérabilités, d’erreurs ou de logiciels malveillants et apporter la preuve de la sécurité du code. Reconnu mondialement pour ses innovations, Binsec est disponible en open source.
Binsec est un outil d’analyse formelle de code binaire orienté sur la sécurité. Il analyse les codes exécutables de logiciels pour en détecter les vulnérabilités et y chercher la présence de logiciels malveillants (malwares) et d’erreurs.
Binsec repose sur des techniques à la pointe de la recherche dans les domaines de l’analyse de code, des méthodes formelles et de la sécurité. Il prend en compte les codes s’exécutant sur les principales architectures : x86, ARM et Risc, y compris dans leurs versions les plus récentes, 64 bits.
Binsec est développé en partenariat avec le LORIA (UMR CNRS, Inria, Université de Lorraine) et l’université Grenoble-Alpes. Il est accessible en open source.
Les principales forces de Binsec :
Binsec est utilisé, notamment, pour vérifier un logiciel en l’absence d’accès total ou partiel au code source (logiciels sur étagère, applications mobiles, par exemple). On l’emploie aussi après la compilation pour s’assurer que les propriétés de sécurité ont été conservées lors de cette étape ou pour répondre à des besoins de garanties fortes et de preuves formelles de sécurité.
Binsec peut également aider à la rétro-ingénierie de logiciels malveillants (malwares), par exemple, afin d’identifier et de casser des protections (« obfuscation ») en empêchant la compréhension.
Binsec revendique plusieurs premières mondiales qui témoignent de son avance technologique :
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.
Accéder à la page Binsec sur Github.
