Vous êtes ici : Accueil > Le List et Thales innovent en cybersécurité

Actualité

Systèmes numériques intelligents

Le List et Thales innovent en cybersécurité


​Dans le cadre de son laboratoire commun FormalLab avec Thales, le List, institut de CEA Tech, a démontré la pertinence de sa plate-forme de vérification formelle Frama-C pour garantir la sécurité de codes cryptographiques.

Publié le 5 septembre 2017

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.

Haut de page

Haut de page