From LaTeX and OCaml to LEAN4 and Executables: Lean-Checked Theorems and Generating Proof-Carrying Rust

Dans le monde du logiciel, il existe une tension constante entre la façon dont nous écrivons le code et la façon dont nous savons qu'il est sûr. Les programmeurs utilisent des langages de haut niveau pour décrire une logique complexe d'une manière lisible et gérable, mais les machines qui exécutent ce code parlent un langage beaucoup plus simple et plus rigide. Pour passer de l'un à l'autre, les compilateurs agissent comme des traducteurs, mais c'est dans ce processus de traduction que les erreurs se cachent souvent. Une erreur dans la traduction peut transformer une instruction sûre en une instruction dangereuse, provoquant le plantage d'un programme ou un comportement imprévisible. Pendant des décennies, le moyen le plus fiable de garantir la sécurité a été de vérifier le code machine final, mais cela est difficile car la signification de haut niveau du programme original est souvent perdue au cours du processus. La question que se posent les chercheurs est de savoir si nous pouvons conserver la clarté du langage de haut niveau d'origine tout en prouvant, avec une certitude absolue, que les instructions machine finales feront exactement ce que nous prévoyons.

Brent Hartshorn a construit un système qui répond à cette question en traitant un seul morceau de code comme deux choses différentes à la fois. Imaginez un document qui peut être lu simultanément comme une preuve mathématique et comme un ensemble d'instructions pour une machine. Dans ce nouveau travail, l'auteur prend un sous-ensemble d'un langage de programmation appelé OCaml, connu pour ses règles strictes sur la gestion des données, et donne à chaque définition deux significations distinctes. Premièrement, le code est lu comme un argument logique, où la structure du programme lui-même sert de preuve que certaines conditions seront toujours respectées. Deuxièmement, le même code est traduit dans un langage différent appelé Rust, conçu pour la vitesse et la sécurité, puis compilé en un programme qu'un ordinateur peut réellement exécuter. La brillance de l'approche réside dans la vérification : la preuve logique est vérifiée par un petit moteur mathématique de confiance, tandis que le programme en cours d'exécution est vérifié par rapport à un interprète de référence qui simule le code étape par étape. Si les deux correspondent, et si la preuve logique tient bon, le résultat est un logiciel qui vient avec son propre certificat de sécurité.

Les chercheurs ont commencé par construire un traducteur qui comprend une tranche spécifique d'OCaml. Ce traducteur, écrit en Python, est assez petit pour être lu et compris par une seule personne, ce qui est crucial car si le traducteur lui-même est trop complexe, nous ne pouvons pas faire confiance à sa production. Il prend le code OCaml et le sépare en deux chemins. Sur le chemin de la preuve, il convertit le code en un format qu'un noyau mathématique peut vérifier. Ce noyau est un petit programme qui agit comme un juge, vérifiant que la logique est saine sans faire d'hypothèses. Sur le chemin du programme, le traductur convertit le code en Rust, un langage qui est compilé en code machine natif rapide. Pour s'assurer que la traduction était parfaite, l'équipe a également construit un interprète de référence qui exécute le code OCaml d'origine directement. Ils ont ensuite fait passer treize programmes d'exemple différents par la version Rust compilée et par l'interprète. Dans chaque cas, le code compilé a produit exactement la même sortie que l'interprète, prouvant que le processus de traduction n'a pas altéré le comportement des programmes.

Une fois le code traduit avec succès, l'équipe a appliqué un contrôle de sécurité rigoureux à la version Rust compilée. Ils ont traité le code compilé comme un contrat, où des règles spécifiques sur la façon dont le programme doit se comporter étaient écrites sous forme de théorèmes mathématiques. Par exemple, ils ont vérifié que les calculs d'entiers ne causeraient jamais accidentellement un dépassement de capacité (overflow) et ne reviendraient pas à un nombre négatif, une source courante de bogues dans les logiciels. Ils ont constaté que si la plupart de ces règles de sécurité étaient respectées, il existait des cas limites spécifiques où les règles étaient rompues. Dans onze scénarios différents, le code compilé atteignait un point où un calcul d'entier pouvait déborder, comme lorsqu'on soustrait le plus petit nombre possible de zéro. Le système a correctement identifié ces points comme des obligations ouvertes, signifiant que le code est sûr partout sauf pour ces limites spécifiques et connues. Sur un total de quatre-vingt-dix contrôles de sécurité effectués sur les programmes d'exemple, soixante-dix-neuf ont été pleinement prouvés, tandis que les onze restants ont été laissés ouverts car ils représentaient des limites réelles et atteignables dans la façon dont l'ordinateur gère les nombres.

Le projet est allé plus loin en appliissant cette méthode à un petit noyau de système d'exploitation, une pièce centrale de logiciel qui gère les ressources de l'ordinateur. Les chercheurs ont pris un noyau qui avait été précédemment écrit en Python et en Rust et l'ont réécrit dans leur sous-ensemble d'OCaml. Ils l'ont ensuite traduit en Rust et l'ont compilé. Le résultat est une troisième implémentation du même noyau. Lors des tests contre la version Python originale, la nouvelle version dérivée d'OCaml a répondu correctement à l'ensemble des 236 cas de test. L'équipe a ensuite tenté de prouver la sécurité de ce nouveau noyau. Ils ont réussi à prouver 227 des 236 obligations de sécurité. Les quelques cas restés non prouvés n'étaient pas des erreurs dans le code, mais plutôt des lacunes dans les outils mathématiques utilisés pour les vérifier, spécifiquement concernant la manière dont le système gère les boucles complexes et les compteurs. Cela a démontré que la méthode pouvait passer de petits exemples à un composant fonctionnel de système d'exploitation.

Peut-être la partie la plus frappante du travail était la capacité de transformer une équation mathématique directement en un programme opérationnel. Les chercheurs ont pris une équation formelle décrivant le comportement d'un noyau, écrite dans une notation mathématique standard, et l'ont injectée dans un outil qui la convertissait en code OCaml. Ce code a ensuite été compilé et exécuté. Le programme résultant se comportait exactement comme l'équation le décrivait, correspondant à la sortie du modèle Python original dans chaque instance. Ce processus a montré qu'une description mathématique de haut niveau pouvait être transformée en un binaire exécutable vérifié sans perdre son sens. L'équipe a prouvé que la version compilée de cette équation satisfaisait la plupart de ses contrats de sécurité, bien que certaines des étapes logiques plus complexes nécessitent un affinement des outils de vérification.

Les conclusions de ce travail suggèrent une nouvelle voie pour la construction de logiciels fiables. En conservant le code source de haut niveau et en vérifiant à la fois sa signification logique et sa forme compilée, les chercheurs ont créé un système où la sécurité du programme final est soutenue par une preuve mathématique. La méthode a identifié avec succès les limitations du monde réel dans la gestion des nombres par les ordinateurs, tels que le dépassement d'entier, et a distingué ces cas des véritables bogues. Bien que le système n'ait pas prouvé chaque règle de sécurité pour les parties les plus complexes du noyau, il en a prouvé la grande majorité, et les cas restés ouverts ont été clairement identifiés comme des domaines où les outils de vérification, plutôt que le code lui-même, devaient être améliorés. Ce travail constitue une démonstration qu'il est possible de maîtriser le processus de traduction du code de haut niveau vers les instructions machine, garantissant que l'exécutable final porte un certificat de sécurité aussi rigoureux que la logique qui l'a créé.