L’objectif de la collaboration est d’étendre les outils d’analyse formelle Frama-C (code source C) et BINSEC (code binaire) du CEA-List pour prendre en compte de nouvelles structures de code ou fonctionnalités spécifiques à la sécurité, selon les demandes de la DGA et de ses fournisseurs.
Pour BINSEC, deux démonstrateurs ont été réalisés :
Pour Frama-C, les travaux ont porté sur l’outil de validation de la conformité d’un programme à sa spécification. Ils consistent en une modélisation mixte de la mémoire qui permet d’analyser finement les opérations bas-niveau sans que le temps d’analyse total ne soit rédhibitoire. Cette analyse du programme est effectuée sur deux modèles de fonctionnement du code : un modèle haut niveau des opérations usuelles et un modèle des opérations bas niveau complexes qui agissent directement sur la mémoire de travail du programme [1].
Deux études de faisabilité ont été réalisées sur Frama-C, pour la vérification de propriétés de flot d’information (pas de fuite de données secrètes) et la détection de nouveaux comportements indéterminés sur les accès mémoire.
Ces résultats concluants ont incité la DGA à lancer de nouveaux projets : l’implantation dans Frama-C des résultats ainsi qu’une extension de BINSEC sur la détection de failles de type canaux cachés dans les primitives de cryptographie post-quantique, c’est-à -dire les algorithmes de sécurité face à un attaquant opérant avec un ordinateur quantique.
L’expertise du CEA-List en analyse formelle de logiciels répond au besoin de la DGA pour la validation de codes de produits de sécurité.
