Vers l’émergence d’un Internet de la preuve ?

Des programmes pour tout

En quelques décennies, l’informatique est devenue partie intégrante de notre quotidien. Si certains logiciels peuvent être considérés comme accessoires (jeux, domotique…), nombreux sont ceux qui ont permis à notre société d’atteindre son niveau de progrès actuel dans le domaine des transports, des télécommunications, de l’industrie…

Cette omniprésence des programmes – qui aident à concevoir, analysent et automatisent des pans de plus en plus nombreux de nos vies – a des conséquences bien différentes en fonction de la criticité des applications en jeu. Si le site mobile de votre mairie connaît un bug passager, l’impact sera moins important qu’une erreur dans un programme dirigeant une centrale électrique. Pour les systèmes les plus critiques, il est donc essentiel de prouver que les logiciels impliqués font bien ce pour quoi ils ont été conçus.

De l’importance de la preuve

Démontrer la validité d’un programme ou d’un système électronique fait appel à la logique mathématique, et plus particulièrement à des techniques de raisonnement nommées "méthodes formelles". Issues de la recherche fondamentale en informatique, elles se sont avérées un outil particulièrement adapté à la vérification de programmes. Elles permettent de produire des "preuves formelles", c’est-à-dire une très forte assurance de l'absence de bugs dans les logiciels analysés. Chacune de ces preuves est construite spécifiquement, grâce à un démonstrateur automatique de théorème, ou assistant à la preuve, pour vérifier un programme en particulier. Et parce qu’elle a été conçue sur mesure, une preuve n’est en général pas lisible par d’autres assistants, ni même adaptée à une autre version du programme.

Par conséquent, à l’heure actuelle, pour vérifier qu’un programme fonctionne bien tel qu’il est censé le faire, il faut construire soi-même une preuve formelle. Pouvoir partager et réutiliser ces preuves d’un assistant de preuve à un autre permettrait donc un gain de temps de travail et une amélioration de la confiance dans les infrastructures informatiques. Mais cette nécessité est entravée par le grand nombre de démonstrateurs et de formats de preuve existants.

Les piliers du partage : standardiser…

Plusieurs initiatives ont émergé pour surmonter ces différences en proposant une forme de standardisation. L’une d’entre elle, Dedukti, est issue d’Inria. Elle consiste à développer une structure universelle qui soit suffisamment flexible pour couvrir les besoins de types de preuves très disparates. Celle-ci doit pouvoir être prise en charge par de nombreux assistants à la preuve, sans nécessiter de les modifier massivement pour correspondre à ce nouveau standard.

Une autre approche est celle de ProofCert, le projet pour lequel Dale Miller, lorsqu’il dirigeait l’équipe-projet Parsifal, a reçu une ERC Advanced Grant pour la période 2012-2016. Ici l’idée était de laisser chacun produire son format de preuve, mais de l’assortir d’une description formelle de la logique sous-tendant les expressions symboliques. Cette définition de la sémantique des preuves formelles devait aider à leur réutilisation.

… et certifier

Mais pour s’appuyer sur les preuves produites par d’autres systèmes et d’autres personnes, l’existence de standards ne suffit pas. Il faut également pouvoir faire confiance à celui qui a produit la preuve formelle vérifiant le programme qui nous intéresse, et être certain que celle-ci n’a pas pu être modifiée depuis sa création.  Donc certifier à la fois l’émetteur et le contenu de la preuve. Deux enjeux auxquels répondent les outils de cryptographie, comme l’explique Dale Miller, qui fait maintenant partie de l’équipe-projet Partout* : « Si je vérifie une preuve, je vais utiliser un certain outil. Je peux donc générer un document disant "Moi, Dale Miller, ce jour-ci, avec tel outil, dis que ceci est prouvé." Je peux ensuite le signer cryptographiquement, afin de m’authentifier comme auteur et associer à la preuve une empreinte cryptographique qui certifie qu’elle n’a pas été corrompue. »

Si un chercheur ou une institution est à l’origine d’un certain nombre de preuves qui, une fois revérifiées par d’autres personnes, s’avèrent toujours correctes, alors la confiance qu’on peut avoir en leur travail est augmentée. Bien que ce système rappelle le peer review, qui est un des fondements de la solidité des résultats publiés dans la littérature scientifique, il n’en a pas la structure hiérarchique. Dans l’idée de Dale Miller, pas de revues vedettes ni d’éditeur ou de reviewer identifiés. Chacun devrait être en mesure de proposer des preuves et de vérifier celles des autres, tissant ainsi un réseau de confiance très horizontal et distribué.

Trois ans pour explorer une refonte totale du système de partage des preuves

C’est tout l’enjeu de l’action exploratoire pour laquelle il vient de recevoir le soutien d’Inria, sous la forme d’un financement de thèse pour trois ans. W3Proof, comme il l’a intitulée, a pour objectif de créer une infrastructure qui s’inspire du World Wide Web à ses débuts : un réseau de partage et de liens entre preuves formelles régi par quelques grands standards (comme le HTML et le http qui ont permis l’émergence d’Internet), à même d’être pris en main par tout un chacun.

L’idée de Dale Miller est qu’en utilisant un format d’export certifiable par quelques grands démonstrateurs de confiance, n’importe quel assistant à la preuve pourra participer à la production et la réutilisation des preuves formelles. Pour assurer une mise en réseau transparente et fiable, il compte s’appuyer non pas sur des serveurs centralisés mais sur l’informatique distribuée, grâce à des protocoles d’échanges de type pair-à-pair. Répondre aux besoins spécifiques du partage des preuves formelles nécessitera "simplement" de coupler ces protocoles à des méthodes de stockage à même de garantir l’intégrité et la permanence de la preuve, par exemple à l’aide d’une clé d’identification unique. Durant les trois prochaines années, Dale Miller et son futur doctorant vont ainsi tenter d’explorer la faisabilité de cette idée, en modifiant un démonstrateur pour en faire un prototype capable de dialoguer avec d’autres.

Loin d’être limitée au domaine de la vérification de programmes, la nouvelle infrastructure de partage de données certifiées que cette action exploratoire espère préfigurer pourrait bénéficier à d’autres secteurs.  C’est notamment le cas de ceux du journalisme, de la lutte contre les fake news et de la production scientifique, pour laquelle la reproductibilité des résultats est un enjeu majeur.

*Automatisation et ReprésenTation : fOndation du calcUl et de la déducTion