C'est une première en cybersécurité : un code opérationnel de logiciels de chiffrement de données sensibles a été analysé par les méthodes formelles du List. L'enjeu est de taille : les logiciels de communication chiffrée contrôlent une large part des échanges numériques actuels, et tout défaut dans ces logiciels peut compromettre la sécurité de grandes quantités de données. Dans le cadre de leur laboratoire commun FormalLab, Thales a sollicité l'expertise du List en analyse et vérification de code sur ses propres composants de cryptographie.
Concrètement, les exigences de sécurité exprimées en langage courant ont d'abord été déclinées en un cahier des charges précis des fonctionnalités logicielles. Le résultat ainsi obtenu a ensuite été comparé au code existant grâce à des outils de raisonnement fondés sur des méthodes mathématiques.
Ces travaux ont permis, en lien étroit avec l'équipe de développement de Thales, de mettre en œuvre la plate-forme Frama-C du List sur ce cas opérationnel. Thales lance actuellement un pilote de déploiement pour systématiser cette approche et garantir l'absence de vulnérabilité de sécurité dans ses codes cryptographiques. Le FormalLab poursuit par ailleurs le développement des prochaines générations d'analyse de code.