Vers une certification formelle de produits de sécurité

Thales a sollicité le CEA-List en vue de la certification d’une de ses cartes à puces, produits pour lesquels les exigences en cybersécurité sont particulièrement élevées. Il s’agissait de prouver formellement la sécurité d’un OS JavaCard embarqué sur une carte à puce.

Les mécanismes de protections mis en œuvre pour parvenir à cette sécurité sont différents dans chaque cas, et sont des secrets industriels bien gardés. La mise en œuvre d’outils de modélisation et de preuve formelle, comme Frama-C du CEA-List, Coq (plateforme développée à Inria et utilisée notamment dans  Frama-C pour la vérification formelle et automatisée d’énoncés et de preuves mathématiques) ou l’Atelier B, est difficile : la taille des logiciels étudiés, des modèles formels et leurs preuves se mesure en dizaines de milliers de lignes de code. Pour réussir ce passage à l’échelle, les équipes du CEA-List ont imaginé de nouvelles méthodes pour faciliter le travail des ingénieurs de sécurité, et développé de nouvelles briques technologiques pour automatiser le travail de preuve et de validation.

L’outil Frama-C a ainsi reçu des extensions pour décliner de manière systématique et automatique des propriétés formelles de haut niveau sur chaque ligne de code, amenant à la réalisation de dizaines de milliers de preuves unitaires. Ces avancées ont porté leurs fruits puisque cette collaboration a permis à Thales d’obtenir un certificat Critères Communs de niveau EAL 7 – après avoir atteint le critère EAL6 en 2022 – les plus rigoureux en matière d’exigences et de preuve formelle de sécurité.

Cette expertise méthodologique dans le domaine de la certification à haut niveau d’exigence en cybersécurité ouvre la voie à de nouveaux partenariats avec des industriels à la pointe du domaine. Les défis relevés se matérialisent par des évolutions scientifiques et techniques qui enrichissent nos plateformes au bénéfice de nombreux autres domaines d’applications.