Partager

Binsec : l’analyse de code binaire pour la sécurité

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.

L'usage

Une analyse au plus près de la machine

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.

Expertise, fonctionnalités, souveraineté

Les principales forces de Binsec :

  • haut niveau en sécurité, analyse automatique de code et en méthodes formelles ;
  • forte visibilité dans le monde académique ;
  • capacités originales : analyse de canaux cachés, preuve niveau binaire, prise en compte des comportements spéculatifs, etc.
Applications

Détection de vulnérabilité, rétro-ingénierie…

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.

Des premières mondiales

Binsec revendique plusieurs premières mondiales qui témoignent de son avance technologique :

  • Analyse automatique des protections (identification & simplification) du malware étatique type APT (2017) ;
  • Preuve de sécurité automatique au niveau binaire d’un noyau embarqué (2019) ;
  • Décompilation de tous les codes C+assembleur de Linux Debian : plus de 1000 défauts de compliance trouvés dans une centaine de packages (2019) ;
  • Analyse de canaux cachés : première preuve au niveau binaire de la sécurité de 196 implémentations cryptographiques, avec trois vulnérabilités découvertes (introduites à la compilation) (2020) ;
  • Campagne de fuzzing de type « patch-oriented » : découverte de 30 nouveaux bugs dans des codes open source, dont 7 failles communes (2020).

Pour en savoir plus

Publications

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.

À lire également

Domaines applicatifs

Cybersécurité : garantir la sûreté et la confidentialité par conception

Au cœur des enjeux de souveraineté numérique, la cybersécurité constitue aujourd’hui un pan essentiel de nos sociétés. Garante de l’autonomie et de la paix dans le cyberespace, elle est un ...
Lire la suite