Intervention de Claude Kirchner

Votre deuxième question a posé le problème consistant à vérifier que les logiciels et les systèmes sont « sûrs », c'est-à-dire travaillent de façon nominale par rapport à leurs spécifications, par exemple que 1 + 1 fasse bien 2. On distingue le système « sûr » du système « sécure », celui dont la sécurité est avérée, parce qu'il va résister à des attaques malignes intentionnelles. Ces questions de sûreté et de sécurité sont un des domaines d'excellence de la recherche française, en particulier à l'INRIA. Dans nos équipes, dans nos plans stratégiques, nous veillons à entretenir un défi renouvelé sur ces problématiques et nous constatons des avancées remarquables de nos équipes projets. Récemment, nous avons été capables de construire un compilateur prouvé correct, donc avec une preuve et non pas une simple vérification. Et c'est un compilateur qui devient de plus en plus utilisé au niveau industriel. À partir du moment où l'on est sûr que le code produit est conforme au code qui est rentré, le degré de confiance devient énorme. C'est un joli succès qui doit se poursuivre pour faire en sorte que l'ensemble de la chaîne opérationnelle soit certifié. Nous avons deux types de certifications à cibler. D'une part, les certifications de type sûreté, qui correspondent au fait que quand on appuie sur la pédale de freins, les freins de la voiture vont bien fonctionner, mais aussi les certifications de type sécurité, qui garantissent en l'occurrence qu'avec son téléphone, un intrus ne va pas dérégler le système de freinage de la voiture. Dans les premiers systèmes aéronautiques, un seul réseau desservait l'ensemble de l'avion et un certain nombre de tests avait prouvé que ce n'était pas prudent, car quelqu'un pouvait prendre le contrôle de l'avion depuis son siège. En France, on a les capacités, on a les scientifiques, on a des domaines d'excellence, on a des relations avec les mathématiciens sur ce domaine. Un premier succès a été réalisé dans le cadre de notre laboratoire de recherche commun avec Microsoft Research. Nos équipes communes ont démontré, il y a six ans, le théorème des quatre couleurs de façon formelle ; il fallait s'assurer que l'ensemble de la démarche logique et mathématique était correcte, ce qui imposait une démonstration très calculatoire.

Nous avons connu un deuxième très grand succès grâce aux travaux de Georges Gonthier, un ancien directeur de recherche de l'INRIA, maintenant en poste au laboratoire de recherche Microsoft à Cambridge, en lien avec nos équipes de Rocquencourt et de Sofia Antipolis. Ces travaux ont conduit à démontrer de façon formelle – et en corrigeant des inexactitudes dans la preuve qui était proposée jusqu'alors – le théorème de Feit et Thompson, qui permet d'aboutir à la classification des groupes finis, le plus gros édifice mathématique existant à ce jour. Cette recherche a duré six ans. L'objectif était de montrer aux mathématiciens que les outils que l'INRIA développe d'un point de vue algorithmique, logique et informatique servent directement la science. Désormais, ces outils sont à la disposition des mathématiciens. Maintenant, il s'agit d'aller plus loin et de prouver la sûreté d'un système d'exploitation. Des start up comme Prove and Run sont déjà capables de démontrer qu'un système d'exploitation destiné à nos téléphones n'est pas vulnérable aux attaques, en utilisant une preuve et pas seulement une vérification. Il s'agit maintenant de garantir par une preuve ses propriétés. Dans ce domaine, là aussi, nous avons d'excellentes équipes, notamment une équipe qui collabore avec Airbus de façon à pouvoir certifier les éléments de pilotage des Airbus A 380 et A 350.