BINSEC utilise l’exécution symbolique au niveau binaire pour détecter les problèmes de sécurité. La correction de l’ensemble des vulnérabilités d’un logiciel étant coûteuse, il est crucial d’identifier les plus susceptibles d’être exploitées.
Une nouvelle fonctionnalité de BINSEC, l’algorithme PyAbd, se concentre sur les vulnérabilités liées aux entrées contrôlables par un attaquant, car elles sont plus faciles à exploiter. PyAbd génère automatiquement des contraintes logiques pour éviter l’exploitation des vulnérabilités. Cet algorithme est prouvé correct, complet et minimal, garantissant que chaque contrainte qu’il propose reflète la gravité d’un bug. Il évalue mieux la criticité des bugs que les techniques existantes et facilite l’interprétation des résultats pour les
évaluateurs de sécurité. Les résultats ont été présentés à la conférence POPL 2024.
BINSEC est utilisé dans plusieurs projets du PEPR Cybersécurité de la stratégie nationale, notamment au sein des défis SecurEval, Rev et DefMal.
Les Critères Communs constituent la certification de sécurité la plus exigeante des systèmes d’information, reconnue internationalement. Les deux plus hauts niveaux (Evaluation Assurance Level EAL6 et EAL7) imposent l’utilisation de méthodes formelles pour prouver les propriétés de sécurité (confidentialité, intégrité et disponibilité des données).
L’expertise de nos chercheurs en sécurité et méthodes formelles les a conduits à travailler sur ces niveaux de certification. IDEMIA, acteur industriel reconnu en sécurité, a ainsi sollicité nos experts avec succès : grâce à cette collaboration, IDEMIA a obtenu en 2023 aux Pays-Bas une certification Critères Communs EAL6, via un modèle formel indépendant du code.
THALES, autre acteur de référence, a noué un partenariat avec le CEA-List dès 2015 sur les méthodes formelles pour la sécurité. L’une de leurs innovations récentes réside dans le couplage de deux plugins de Frama-C, WP et MetACSL, pour la vérification de propriétés comme la confidentialité et l’intégrité des données.
Ce résultat est reconnu par l’ANSSI comme le troisième outil basé sur les méthodes formelles capable de répondre aux plus hauts niveaux des Critères Communs.
En utilisant Frama-C, Thales a obtenu de l’ANSSI un certificat EAL6 en 2021 pour un de ses produits, puis un certificat EAL7 en 2022. La preuve directement sur le code du produit augmente les garanties de cette certification. Ces résultats traduisent la capacité des outils formels pour la certification de haut niveau en cybersécurité et le rôle clé du CEA-List en tant que fournisseur d’outils spécialisés.
Frama-C est également impliqué dans le projet SecurEval du PEPR cybersécurité et l’ANSSI et la DGA collaborent avec nos équipes autour de Frama-C et BINSEC pour l’évaluation avancée des logiciels.
Fournir des outils à haut niveau de garantie est essentiel en cybersécurité, que ce soit pour la détection des vulnérabilités ou pour la preuve de propriétés de sécurité.
