💻 computer science

Misquoted No More: Securely Extracting F* Programs with IO

Cet article introduit SEIO*, un cadre qui combine la citation relationnelle avec la génération de syntaxe vérifiée pour extraire de manière sécurisée des programmes F* faiblement enchâssés avec des entrées/sorties et des types de raffinement vers un calcul profondément enchâssé, fournissant des preuves vérifiées par machine de la Préservation de l'Hyperpropriété Relationnelle Robuste (RrHP) afin de garantir la sécurité contre tout lien adversaire arbitraire.

Auteurs originaux : Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

Publié 2026-07-20

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le filet de sécurité invisible

Imaginez que vous êtes un architecte de génie qui a conçu une voiture autonome magnifique dans un monde imaginaire parfait où la physique se comporte toujours exactement comme vous le prédisez. Vous avez écrit les plans dans un langage spécial, ultra-précis, qui vous permet de prouver mathématiquement que la voiture ne manquera jamais de collision, ne freinera jamais quand elle ne le devrait pas, et respectera toujours les règles de la route. C'est ce que les informaticiens appellent la « vérification formelle ». C'est comme construire une voiture dans un rêve où vous pouvez être sûr à 100 % de chaque boulon et chaque fil.

Mais voici le hic : ce monde de rêve n'existe pas sur la route réelle. Pour réellement conduire la voiture, vous devez traduire vos plans parfaits dans un langage que les vrais moteurs et pneus comprennent, comme le C ou l'OCaml. Ce processus de traduction est appelé « extraction ». Le problème est que le traducteur (le programme informatique qui effectue la conversion) n'est pas parfait. Il pourrait oublier un boulon, tordre un fil ou mal interpréter une règle. Si la voiture du monde réel est construite sur une erreur commise lors de la traduction, votre preuve de sécurité parfaite devient inutile. La voiture pourrait paraître sûre sur le papier mais s'écraser dans la réalité.

Pendant des années, des scientifiques ont tenté de corriger cela en vérifiant le travail du traducteur après coup, un peu comme un mécanicien inspectant une voiture après sa construction pour voir si elle correspond aux plans. Mais ce document introduit une méthode plus intelligente : au lieu de simplement vérifier la voiture finie, ils construisent un « certificat de sécurité » pendant la traduction qui prouve, mathématiquement, que la vraie voiture est le jumeau parfait de la voiture du rêve, même si le traducteur commet une erreur. Ils appellent cela un cadre d'« extraction sécurisée », et il est conçu pour garder vos créations numériques en sécurité, même lorsqu'elles sont mélangées à du code non vérifié provenant du monde extérieur.

La grande idée du papier : Le tour de magie de la « Citation Relationnelle »

Les auteurs de ce papier, une équipe de chercheurs en informatique, ont construit un nouveau cadre appelé SEIO★ (Secure Extraction of IO-star). Leur objectif était de résoudre le « problème de la traduction » pour les programmes écrits en F★, un langage utilisé pour écrire des logiciels hautement sécurisés comme les outils cryptographiques. Ces programmes F★ sont souvent « faiblement enchâssés » (shallowly embedded), une façon sophistiquée de dire qu'ils sont écrits dans un style abstrait de haut niveau, excellent pour prouver des choses mais difficile à transformer en code réel par les ordinateurs.

Habituellement, lorsque vous transformez ces programmes abstraits en code réel, vous devez utiliser un « métaprogramme » (un programme qui écrit d'autres programmes) pour faire le gros du travail. L'ancienne méthode était risquée : le métaprogramme écrivait le nouveau code, puis essayait d'écrire une preuve que le nouveau code était correct. Si la preuve échouait, il fallait recommencer. Si la preuve réussissait, il fallait quand même faire confiance au fait que le métaprogramme n'avait pas glissé un bug lors de l'écriture de la preuve. C'était comme demander à un élève de corriger ses propres devoirs en espérant qu'il ne triche pas.

La percée des auteurs est une technique qu'ils appellent la Citation Relationnelle (Relational Quotation). Au lieu de demander au métaprogramme d'écrire le code final et la preuve, ils lui demandent de faire quelque chose de beaucoup plus simple : écrire une dérivation de typage. Voyez cela comme une fiche de recette étape par étape qui dit : « Étape 1 : Prenez cet ingrédient. Étape 2 : Mélangez-le avec celui-là. » Cette fiche de recette ne cuisine pas réellement le plat ; elle prouve simplement que les ingrédients pourraient être cuisinés en un plat spécifique.

Voici la partie ingénieuse :

Le Métaprogramme (Le rédacteur de recettes) : Le métaprogramme non vérifié regarde le programme abstrait original et génère cette « fiche de recette » (la dérivation de typage). Comme la fiche de recette suit exactement la structure du programme original, il est très facile de l'écrire.
Le Contrôle (L'inspecteur) : Le langage F★ lui-même vérifie cette fiche de recette. Il demande : « Cette recette décrit-elle réellement le programme original ? » Si le métaprogramme a fait une erreur et a écrit une recette de gâteau alors que l'original était une soupe, le contrôle échoue. Mais si la recette correspond, le langage F★ est sûr à 100 % que la recette est valide.
L'Étape Vérifiée (Le Maître Chef) : Une fois que la fiche de recette est vérifiée, une autre fonction, entièrement vérifiée (un « Maître Chef » qui a été mathématiquement prouvé comme étant parfait), prend cette recette et cuisine le plat final (le code réel). Parce que la recette a été prouvée conforme à l'original, et que le chef est prouvé pour cuisiner exactement ce que la recette indique, le plat final est garanti d'être un jumeau parfait de l'original.

Cette approche minimise la « confiance » que l'on doit accorder au métaprogramme non vérifié. On ne lui fait confiance que pour écrire la recette, pas pour cuisiner le plat ou corriger les devoirs. La partie difficile — prouver que la nourriture est sûre — est réalisée par le Maître Chef vérifié.

Le superpouvoir de la « Compilation Sécurisée »

Le papier ne se contente pas de s'assurer que le code est correct ; il va plus loin pour garantir qu'il est sécurisé. Dans le monde réel, votre programme vérifié peut être lié à d'autres codes qui ne sont pas vérifiés — peut-être du code écrit par un hacker, ou simplement du code négligent provenant d'une autre équipe. Ce code « adversaire » essaie de briser les règles de votre programme.

Les auteurs prouvent que leur cadre SEIO★ satisfait une règle de sécurité extrêmement forte appelée Préservation de l'Hyperpropriété Relationnelle Robuste (Robust Relational Hyperproperty Preservation - RrHP). Pour comprendre cela, imaginez que votre programme vérifié est une forteresse.

Les anciennes méthodes pourraient dire : « Les murs de la forteresse sont solides, donc elle est sûre. »
Ce papier dit : « Même si un hacker tente de s'introduire par la porte dérobée, ou s'il tente de tromper les gardes, ou s'il tente de changer les règles du jeu, votre forteresse se comportera toujours exactement comme vous l'avez conçu. »

Ils prouvent cela en utilisant deux « relations logiques », qui sont comme des miroirs sans tain. Un miroir vérifie si le code réel fait tout ce que le code abstrait pourrait faire. L'autre mière vérifie que le code réel ne fait pas ce que le code abstrait ne pourrait pas faire. En prouvant les deux, ils montrent que le code réel est une ombre parfaite et sécurisée de l'original, peu importe le code désordonné avec lequel il est lié.

Ce qu'ils ont fait (et ce qu'ils n'ont pas fait)

L'équipe a construit ce cadre entièrement à l'intérieur du langage F★ et a utilisé un ordinateur pour vérifier chaque étape de leur preuve. Ils n'ont pas seulement supposé ou simulé ; ils ont prouvé cela mathématiquement.

Ce qui fonctionne : Ils ont réussi à extraire des programmes qui gèrent les entrées/sorties de fichiers (lecture et écriture de fichiers) et utilisent des « types de raffinement » (des types avec des règles supplémentaires, comme « ce nombre doit être positif »). Ils ont montré que même avec ces fonctionnalités complexes, l'extraction reste sécurisée.
Ce qui est encore un travail en cours : Le papier admet que leur système actuel ne gère pas les fonctions récursives (fonctions qui s'appellent elles-mêmes) ou les « types dépendants » complets (où les types peuvent dépendre de valeurs) de la manière la plus naturelle. Ils ont dû utiliser une solution de contournement impliquant des itérateurs (boucles) pour la récursion. Ils notent également que leur métaprogramme doit parfois deviner où placer certains contrôles de sécurité, ce qui peut être un peu maladroit.
L'essentiel : Ils n'ont pas résolu tous les problèmes de l'univers de la programmation, mais ils ont construit un nouveau pont beaucoup plus sûr entre le monde des preuves parfaites et le monde désordonné du code réel. Ils ont prouvé qu'en divisant le travail en une phase de « rédaction de recette » et une phase de « cuisine », on peut obtenir de fortes garanties de sécurité sans avoir à faire une confiance totale au rédacteur de la recette.

En bref, SEIO★ est un nouvel outil qui permet aux programmeurs de prendre leurs idées parfaites et vérifiées pour les transformer en logiciels du monde réel avec un filet de sécurité mathématiquement garanti, assurant que même si le processus de traduction est imparfait, le résultat final reste à l'abri du chaos du monde extérieur.

Résumé Technique : Misquoted No More: Securely Extracting F★Programs with IO

1. Énoncé du Problème

Le langage orienté preuve F★ est largement utilisé pour écrire et vérifier des programmes qui sont faiblement enchâssés (shallowly embedded) à l'aide de monades pour représenter les effets (par exemple, l'E/S ou I/O). Une fois vérifiés, ces programmes sont typiquement extraits vers des langages courants comme OCaml ou C pour l'exécution. Cependant, ce processus d'extraction est actuellement non vérifié et constitue une partie de la base de confiance (TCB - Trusted Computing Base).

Le défi central réside dans l'étape de « quotation » requise pour extraire les programmes faiblement enchâssés. La quotation implique la traduction d'un programme faiblement enchâssé (où les effets sont représentés par des types monadiques) vers une syntaxe d'arbre d'abstraction profondément enchâssée (deeply embedded) (une représentation concrète du langage cible). Vérifier ce métaprogramme de quotation est un défi majeur non résolu, car cela nécessite une méta-théorie mécanisée pour le langage source, et même pour des systèmes matures comme Rocq, la vérification de la quotation reste non résolue.

Les approches précédentes pour certifier l'extraction reposent fortement sur la validation de traduction (translation validation), où un métaprogramme génère à la fois le code extrait et une preuve de correction, laquelle est ensuite vérifiée par le typage. Bien que cela réduise la TCB par rapport à la vérification du métaprogramme, cela repose toujours sur le fait que le métaprogramme génère des preuves valides, ce qui peut échouer ou être incorrect. De plus, les travaux existants se concentrent principalement sur la correction (préservation du comportement fonctionnel) plutôt que sur la sécurité. Lorsque le code extrait est lié à du code adverse non vérifié, les garanties formelles du programme original vérifié peuvent être compromises, menant à une unsoundness (incohérence) ou à des failles de sécurité.

2. Méthodologie

Les auteurs introduisent SEIO★, un cadre pour extraire des programmes F★ faiblement enchâssés avec des E/S et des types de raffinement vers un $\lambda$ -calcul simplement typé profondément enchâssé ( $\lambda_{io}$ ). La méthodologie divise le processus d'extraction en deux phases distinctes afin de minimiser la dépendance à la validation de traduction :

Phase 1 : Quotation Relationnelle (Validation de Traduction)
Au lieu de générer directement le code cible, le cadre utilise un métaprogramme pour générer une dérivation de typage pour le programme original faiblement enchâssé.

Relation de Typage Relationnelle : Les auteurs définissent une relation de typage qui caractérise le sous-ensemble de F★ (appelé IO★) extrait. Cette relation opère sur des « valeurs F★ ouvertes » (fonctions allant des environnements d'évaluation vers des valeurs) plutôt que sur des expressions syntaxiques, ce qui lui permet de gérer les variables libres dans un enchâssement faible.
Métaprogramme : Un métaprogramme simple parcourt la structure du programme source et construit une dérivation de typage correspondante.
Validation : La dérivation générée est vérifiée par le typage de F★. Parce que la relation de typage utilise des types dépendants, le vérificateur de types s'assure que la dérivation correspond syntaxiquement et sémantiquement au programme original. Cette étape est la seule partie reposant sur la validation de traduction.

Phase 2 : Génération de Syntaxe Vérifiée
Une fois qu'une dérivation de typage valide est obtenue, une fonction F★ pure et vérifiée parcourt récursivement la dérivation pour générer la syntaxe $\lambda_{io}$ cible.

Puisque la dérivation de typage est structurellement liée au programme source via des types dépendants, la fonction de génération de syntaxe est garantie de produire du code sémantiquement lié à l'original.
Cette étape est entièrement vérifiée dans F★, éliminant ainsi le besoin de validation de traduction pour la phase de génération de code.

Garanties de Sécurité via les Relations Logiques
Pour prouver la sécurité, les auteurs définissent deux relations logiques inter-langages entre le langage source (IO★) et le langage cible ( $\lambda_{io}$ ) :

Cible-vers-Source : Relie un programme cible à un programme source, garantissant que tout comportement cible possède un comportement source correspondant.
Source-vers-Cible : Relie un programme source à un programme cible, garantissant que tout comportement source possède un comportement cible correspondant.

Ces relations sont définies sur des sémantiques produisant des traces, où les opérations d'E/S génèrent des événements (traces). Les auteurs prouvent que SEIO★ satisfait la Robust Relational Hyperproperty Preservation (RrHP), le critère de compilation sécurisée le plus fort défini par Abate et al. [1]. La RrHP implique l'abstraction complète (préservation de l'équivalence observationnelle) ainsi que la préservation des propriétés de traces et des hyperpropriétés (ex: non-interférence) contre des contextes adverses arbitraires.

Gestion des Types de Raffinement
Le cadre est étendu pour supporter les types de raffinement (contraintes logiques sur les types). Étant donné que F★ traite les preuves de raffinement via des solveurs SMT sans produire de termes de preuve explicites, le métaprogramme de quotation relationnelle doit re-calculer les préconditions les plus faibles (weakest preconditions) à partir de zéro lors de la quotation et les re-prouver pour garantir que la dérivation de typage reste valide.

3. Contributions Clés

Quotation Relationnelle : Une nouvelle technique de validation de traduction qui utilise des types dépendants pour définir une relation de typage pour les programmes faiblement enchâssés. Elle permet à un métaprogramme de générer une dérivation de typage qui est vérifiée par le typage pour assurer sa correspondance avec le programme source, évitant ainsi de devoir vérifier le métaprogramme lui-même.
Cadre SEIO★ : Un cadre d'extraction complet pour les programmes F★ avec E/S et types de raffinement, les extrayant vers un $\lambda$ -calcul profondément enchâssé.
Compilation Sécurisée Formelle : Une preuve vérifiée par machine dans F★ démontrant que SEIO★ satisfait la RrHP. C'est le premier cadre d'extraction pour un langage orienté preuve fournissant des garanties de sécurité aussi fortes contre du code adverse lié arbitraire.
Relations Logiques Inter-langages : La définition et la preuve de deux relations logiques asymétriques qui comblent le fossé entre un langage faiblement enchâssé avec une sémantique produisant des traces et un langage profondément enchâssé avec des sémantiques opérationnelles standards.
Support des Types de Raffinement : Une extension du cadre pour gérer les types de raffinement en recalculant et en revérifiant les préconditions lors de la quotation.

4. Résultats

Les auteurs ont implémenté SEIO★ dans F★, incluant plus de 900 définitions de haut niveau.
Ils ont extrait avec succès un exemple exécutable : un wrapper de validation pour des agents d'IA non vérifiés qui lit un fichier, appelle un agent et vérifie le résultat.
Le cadre a été testé avec divers agents (tant corrects que malveillants) écrits directement dans le langage cible $\lambda_{io}$ .
La preuve vérifiée par machine confirme que l'extraction préserve les propriétés de sécurité même lorsqu'elle est liée à du code arbitraire non vérifié, satisfaisant la RrHP.
L'artéfact inclut un pipeline pour compiler le code $\lambda_{io}$ extrait vers OCaml en utilisant le framework Peregrine et Malfunction, permettant une exécution pratique.

5. Signification et Revendications

Le papier affirme faire progresser l'état de l'art de deux manières clés :

Minimiser la Validation de Traduction : En confinant la validation de traduction à la génération d'une dérivation de typage (quotation relationnelle) et en vérifiant l'étape de génération de syntaxe subséquente, le cadre réduit la dépendance aux métaprogrammes non vérifiés par rapport aux travaux précédents de certification d'extraction.
Sécurité sur la Correction : Contrairement aux travaux précédents qui se concentraient sur la correction fonctionnelle, SEIO★ fournit des garanties de compilation sécurisée formelles. Il garantit que les programmes F★ vérifiés conservent leurs propriétés de sécurité (telles que la non-interférence et les propriétés de traces) même lorsqu'ils sont liés à du code arbitraire, non vérifié ou adverse.

Les auteurs notent que ce travail va au-delà de l'état de l'art actuel, qui n'a pas encore fourni de garanties de compilation sécurisée aussi fortes pour l'extraction à partir de langages orientés preuve. Ils reconnaissent des limites, telles que l'absence actuelle de support pour les fonctions récursives générales et les types dépendants complets, qui sont laissées comme travaux futurs. Le papier souligne que bien que le métaprogramme de quotation relationnelle soit non vérifié, sa simplicité et la vérification rigoureuse des étapes suivantes rendent l'approche globale robuste.