Inria collabore avec l’ANSSI autour du logiciel Coq

La certification joue un rôle essentiel dans le secteur des produits et services numériques. En garantissant aux utilisateurs un certain niveau de robustesse et de sécurité, celle-ci, en plus de répondre à des objectifs réglementaires et contractuels, offre un véritable avantage concurrentiel aux fournisseurs de produits et prestataires de services qui en font la demande.

La capacité d’un produit ou service à résister à une attaque, quelle qu’elle soit, est éprouvée par une évaluation, qui se base sur une analyse de sa conformité et de sa vulnérabilité.

En France, il existe à ce jour deux types de certification : la certification de sécurité de premier niveau (CSPN), qui permet d’analyser dans un délai assez court la capacité d’un produit à résister à des attaques de niveau modéré, et la certification critères communs (CC), un standard internationalement reconnu qui classe le niveau de sécurité des produits en sept paliers. Plus le niveau d’assurance visé est élevé, plus les éléments de preuve attendus sont précis et l’effort d’évaluation important.

Malgré cela, le domaine de la certification se retrouve confronté à une problématique de taille : le manque d’homogénéisation des activités d’évaluation à travers le monde. Il existe ainsi, aujourd’hui, différents systèmes de certification de sécurité, qui, s’ils suivent une norme internationale, varient en fonction des pays.

Une problématique sur laquelle s’est penchée l'ANSSI, l'autorité nationale en matière de sécurité et de défense des systèmes d'information. Considérée comme l’un des premiers émetteurs de certifications CC au monde, celle-ci a ainsi décidé de collaborer avec Inria autour d’un document introduisant des lignes directrices et des règles pour les analyses formelles soutenues par Coq.

Les objectifs : présenter Coq comme exemple de référence pour un outil de méthodes formelles et alerter sur les exigences d’utilisation d’autres outils. Plus globalement, le but est également de mettre en avant les interprétations françaises auprès des spécialistes étrangers de la certification, qui peuvent ensuite décider d'adopter la même approche qu'en France.

« Les Critères Communs établissent qu'à partir d'un certain niveau d'assurance, il est nécessaire que les bonnes propriétés de sécurité de la spécification fonctionnelle du produit évalué soient formellement prouvées. En pratique, cela pose la question de ce que veut dire "être formellement prouvé" et des méthodes et outils utilisables pour établir une telle preuve. Le développeur peut choisir ces outils selon sa convenance, mais il revient à l'évaluateur de s'assurer que la solution choisie soit effectivement d'une "qualité" suffisante », explique Thomas Letan, expert en méthodes formelles pour la sécurité au sein du Laboratoire Sécurité du Logiciel de l'ANSSI.

Évalué comme un outil adéquat pour les évaluations Critères Communs, Coq a ainsi hérité d’un document de travail. De quoi permettre aux développeurs, notamment, d’utiliser le logiciel dans de bonnes conditions : « Les critères communs recommandent l'utilisation de méthodes formelles pour les niveaux élevés de certification. Le but de cette collaboration était d'éviter que les utilisateurs aient un faux sentiment de sécurité parce qu'ils auraient utilisé Coq de façon maladroite », précise Yves Bertot, directeur de recherche Inria.

La France est à la pointe en termes de certification, et compte bien y rester. Ce travail mené par l'ANSSI et Inria fait partie de cette démarche : proposer les outils fiables à utiliser pour la certification, et proposer des guidelines pour bien les utiliser. Mais pas que.

Cette collaboration a également permis à l'ANSSI de profiter d’un retour rapide et éclairé des équipes Inria sur les règles qu’elle préconise : « Nous avons modifié certaines de nos exigences en nous basant sur les retours d'Yves Bertot, Maxime Dénès et Vincent Laporte », précise Thomas Letan.

De leur côté, les chercheurs Inria impliqués dans ce partenariat ont pu clarifier les enjeux de Coq vis-à-vis des évaluations de sécurité, mais aussi gagner en visibilité : « Notre mission, c’est de faire en sorte que les résultats de recherche se transforment dans l’industrie, que Coq y soit mieux adopté et utilisé. Le fait que l'ANSSI connaisse Coq, reconnaisse sa pertinence dans le cadre des Critères Communs et partage une note d'utilisation dédiée répond à cet objectif », explique Yves Bertot.

Ce projet s’inscrit dans une démarche partenariale amorcée depuis plusieurs années entre l'ANSSI et Inria, destinée à renforcer le partage des expertises au profit de la recherche et de l’innovation.