🤖 AI

Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

Cet article présente une correction vérifiée par machine d'un cadre de 2018 pour la sémantique épistémique des politiques de flux d'information, réalisée avec l'assistance d'un assistant de codage IA agentique, afin de fournir un fondement robuste et général pour spécifier et appliquer des exigences de sécurité expressives.

Auteurs originaux : David A. Naumann

Publié 2026-08-04

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : David A. Naumann

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

Les Gardiens du Secret et le Murmure Numérique

Imaginez un monde où chaque programme informatique est une ville bouillonnante, et où l'information est la monnaie qui circule dans ses rues. Dans cette ville, certains secrets sont si précieux — comme une clé maîtresse ou un mot de passe — qu'ils ne doivent jamais quitter un coffre-fort spécifique. C'est le domaine de la sécurité du flux d'informations, une branche de l'informatique dédiée à garantir que les données sensibles ne fuitent pas accidentellement (ou malicieusement) vers de mauvais yeux. Mais la vie n'est pas toujours en noir et blanc. Parfois, un secret doit être partagé, mais seulement sous des conditions très spécifiques. Peut-être qu'une banque veut dire à un client que son compte est en sécurité, mais seulement après qu'il a répondu correctement à une question de sécurité. Ce jeu d'équilibre délicat s'appelle la déclassement (ou downgrading) : prendre un secret de haut niveau et abaisser soigneusement son niveau de protection pour qu'il puisse être vu, mais seulement quand les règles l'autorisent.

Pour donner un sens à ces règles complexes, les scientifiques utilisent une branche de la logique appelée logique épistémique. Considérez cela comme la « logique de la connaissance ». Au lieu de simplement demander « Que s'est-il passé ? », elle demande « Que l'observateur sait-il ? ». Si un pirate observe la ville, que peut-il déduire des secrets dans le coffre-fort en se basant sur le trafic qu'il voit ? Le défi a toujours été d'écrire un livre de règles parfait qui stipule exactement quand un secret peut être partagé sans créer de faille. Pendant des années, les chercheurs ont tenté de construire un cadre mathématique pour cela, mais les plans présentaient sans cesse des fissures. Si les mathématiques sont fausses, la sécurité n'est qu'une illusion.

Réparer le Plan avec un Assistant Robotique

Cet article raconte comment un chercheur, David Naumann, s'est associé à un assistant de codage par intelligence artificielle pour réparer un plan défectueux de ces règles de sécurité. Le plan original, publié en 2018, était une tentative ingénieuse de définir exactement quand un programme est autorisé à « déclasser » un secret. Il utilisait un concept appelé annotations relationnelles, qui sont comme des notes autocollantes placées sur le code disant : « Il est permis de montrer ce secret si le lancer de pièce de monnaie est tombé sur pile ». L'idée était que si deux exécutions différentes du programme tombaient d'accord sur le lancer de pièce, elles pourraient s'accorder sur le fait de montrer le secret.

Cependant, lorsque l'article original a été présenté, l'auteur a réalisé qu'il y avait une faille significative dans sa preuve. C'était comme construire un pont qui semblait robuste mais qui s'effondrait sous un type de vent spécifique. L'auteur avait esquissé une correction, mais les détails étaient désordonnés et non vérifiés. Cet article prend cette esquisse et la transforme en une structure solide et inébranlable.

La découverte principale ici est une preuve vérifiée par machine. L'auteur n'a pas seulement écrit les mathématiques sur papier ; il les a injectées dans un programme informatique appelé Rocq (un assistant de preuve) qui agit comme un tuteur de mathématiques hyper-attentif. Ce tuteur robotique a vérifié chaque étape de la logique pour s'assurer qu'il n'y avait pas de lacunes cachées. Le résultat est un cadre corrigé qui prouve que : si un programme suit un ensemble spécifique de règles de « sûreté » (qui sont faciles à vérifier pendant l'exécution du programme), alors il est mathématiquement garanti d'être sécurisé selon les règles complexes de la « connaissance ».

L'article exclut explicitement l'idée que la preuve de 2018 était correcte telle quelle. Il montre que la définition précédente de la « politique de libération » (le livre de règles pour savoir quand les secrets peuvent être partagés) était défectueuse car elle ne tenait pas compte de toutes les manières dont un programme pourrait rester bloqué ou diverger. L'auteur soutient que l'on ne peut pas simplement faire confiance à l'intuition humaine sur ces scénarios complexes de multi-exécutions ; il faut que la machine vérifie chaque possibilité.

Le Détective et l'Alibi

Pour comprendre comment cela fonctionne, imaginez un détective (le système de sécurité) essayant de déterminer si un suspect (le programme) fuit des secrets. Le détective possède deux outils : la Sûreté (Safety) et la Sécurité (Security).

La Sécurité est l'objectif ultime : « Le suspect n'a rien dit à personne qu'il n'était pas censé savoir. » C'est difficile à prouver car vous devez imaginer tous les scénarios possibles dans lesquels le suspect aurait pu se trouver.
La Sûreté est une vérification locale plus simple : « Le suspect a-t-il suivi les règles étape par étape au fur et à mesure ? »

La grande percée de l'article est de prouver que la Sûreté implique la Sécurité. Si le programme suit les règles de « Sûreté » (qui sont comme une liste de contrôle d'« alibis » pour chaque étape), alors la garantie complexe de « Sécurité » est automatiquement tenue. C'est comme prouver que si un conducteur ne brûle jamais un feu rouge ou ne dépasse pas la vitesse autorisée (Sûreté), il ne causera jamais un type d'accident spécifique (Sécurité).

L'auteur a utilisé un assistant de codage agentique (plus précisément un outil appelé Claude Code) pour l'aider à écrire le code de la preuve Rocq. Ce n'était pas seulement un correcteur orthographique ; l'IA a aidé à traduire les esquisses mathématiques désordonnées en un code rigoureux et a même trouvé certaines des propres erreurs de l'auteur. Par exemple, l'IA a signalé qu'une définition de la « divergence » (lorsqu'un programme reste bloqué dans une boucle infinie) était trop stricte et devait être assouplie pour que la preuve fonctionne. L'IA a également tenté de « rendre les hypothèses plus fortes que nécessaire », mais l'auteur humain l'a repérée et a corrigé le tir.

Le Résultat : Un Livre de Règles Vérifié

L'article conclut que le cadre corrigé est solide. La preuve vérifiée par machine confirme que l'idée originale était sur la bonne voie, mais que les détails nécessitaient une révision majeure. Le nouveau cadre permet une « politique de libération » clairement définie et séparée du contrôle de sécurité lui-même. Cela signifie que les développeurs peuvent écrire leur code avec des instructions « assume » (comme « suppose que l'utilisateur est connecté ») et avoir la garantie mathématique que ces hypothèses contrôlent correctement ce qui est révélé.

L'auteur est très sûr de ce résultat car il a été vérifié par machine. Il ne s'agit pas d'une simulation ou d'une suggestion ; c'est une preuve formelle que la logique tient bon sous l'examen d'un ordinateur. Ils admettent toutefois que le code est actuellement un peu désordonné et nécessite un nettoyage humain pour être véritablement lisible, tel un brouillon brillant griffonné sur une serviette qui doit être transcrit dans un livre propre.

En fin de compte, cet article est une victoire pour la précision. Il montre que même dans le monde abstrait de la sécurité informatique, où la logique peut devenir incroyablement complexe, nous pouvons utiliser à la fois l'intuition humaine et l'assistance de l'IA pour construire un fondement mathématiquement incassable. Il transforme une esquisse fragile en une forteresse vérifiée, garantissant que lorsque nous décidons de partager un secret, nous le faisons exactement quand nous le voulons, et pas un instant avant.

Résumé Technique : En supposant que vous saviez : Correction d'une sémantique épistémique pour les politiques de flux à l'aide de l'IA agentique

1. Énoncé du problème

Les exigences de sécurité de haut niveau concernant le flux d'informations, particulièrement celles impliquant la déclassement sélectif (déclassification), sont notoirement difficiles à formaliser avec précision. Bien que la logique épistémique soit apparue comme un cadre prometteur pour définir la confidentialité (ce qu'un observateur à un niveau de privilège spécifique est autorisé à savoir), un cadre robuste et général pour les politiques de flux expressives est resté insaisissable.

Un travail antérieur, désigné par CN (Naumann et al., CSF 2018), a tenté de fournir un cadre unificateur pour les modèles de programmes réactifs. Dans CN, les politiques étaient exprimées via des instructions assume au sein du code, tandis que la politique de libération dérivée était exprimée uniquement en termes de flux d'entrée. Cependant, la formalisation dans CN contenait une faille significative dans sa preuve, annoncée lors de la présentation à la conférence. La définition originale de la politique de libération et la preuve subséquente que la sûreté implique la sécurité étaient approximatives et incorrectes. De plus, les adaptations vérifiées par machine existantes (par exemple, Murray et al. pour les programmes C concurrents) reposent souvent sur des propriétés fortes comme l'exécution en temps constant, ce qui trivialise les complexités de l'alignement de multiples exécutions requises pour le raisonnement épistémique.

Le défi central est de fournir une formalisation corrigée et vérifiée par machine qui :

Révise la sémantique épistémique pour gérer correctement le déclassement dépendant de l'état.
Définit explicitement la sémantique d'une politique de libération dérivée des annotations de code.
Prouve qu'une propriété orientée programme appelée sûreté implique la propriété de sécurité épistémique.

2. Méthodologie

L'auteur emploie une approche de vérification formelle utilisant l'assistant de preuve Rocq (anciennement Coq). La méthodologie implique :

Modèle de programme : Un petit langage impératif réactif avec des gestionnaires d'entrées pour des niveaux de sécurité spécifiques. Les programmes consomment des flux d'entrée et produisent des sorties.
Annotations : Le cadre utilise des assertions relationnelles (assert) et des hypothèses (assume) pour spécifier les exigences de flux d'informations. Ces annotations permettent des flux conditionnels qui dévient de la politique de non-interférence de base.
Sémantique épistémique : La sécurité est définie en termes de connaissance d'un observateur. Un observateur au niveau $\ell$ connaît un ensemble d'histoires d'entrées possibles cohérentes avec ses observations visibles (entrées et sorties aux niveaux $\ell' \sqsubseteq \ell$ ).
Politique de libération ( $RP_\ell$ ) : Définie comme l'ensemble des listes d'entrées qu'un observateur est autorisé à apprendre, dérivée des instructions assume dans le code. Cette politique est interprétée via des alignements entre un pré-run "majeur" (exécution réelle) et des pré-runs "mineurs" (exécutions possibles avec des entrées différentes).
Condition de sûreté : Une propriété orientée programme définie par l'absence de "défaillances" (échecs d'assertion, échecs d'alignement) ou la présence de "fiat" spécifiques (fiat d'hypothèse, fiat de divergence) lors de la comparaison d'un run majeur contre tous les runs mineurs possibles.
Assistance par l'IA agentique : La formalisation a été développée avec l'aide de Claude Code, un assistant de codage IA agentique. L'IA a été guidée pour traduire les définitions LaTeX en spécifications Rocq et pour aider à la construction des preuves, bien qu'elle ait nécessité une importante curation humaine pour corriger les erreurs logiques, affiner les définitions et gérer la stratégie de preuve.

3. Contributions clés

A. Sémantique épistémique corrigée

Le papier présente une formalisation révisée de la sémantique épistémique pour les politiques de flux. Les révisions techniques clés incluent :

Définition de la politique de libération : La définition de la politique de libération $RP_\ell(gs)$ est corrigée pour être un prédicat sur les pré-runs (préfixes d'exécution finis) plutôt que sur de simples traces d'événements observés. Elle est définie via la semi-conformance : une relation entre un pré-run majeur et des pré-runs mineurs qui les alignent à des points d'annotation spécifiques.
Sécurité insensible au progrès : Le cadre adopte une définition de sécurité insensible au progrès. Il utilise une notion de connaissance de progrès ( $k_\ell^\to$ ) pour gérer la divergence, garantissant que les garanties de sécurité tiennent même si le programme diverge, à condition que la divergence elle-même ne fuite pas d'informations sur les entrées cachées.
Programmes bien spécifiés : L'auteur introduit des "annotations de base" (hypothèses au début des gestionnaires et assertions avant les sorties) pour rationaliser la formalisation et garantir que les politiques de base sont encodées sans altérer le comportement observable.

B. La sûreté implique la sécurité

Le résultat théorique central est le Théorème 2 : Pour tous les niveaux $\ell$ , tout pré-run qui est sûr pour $\ell$ est sécurisé pour $\ell$ .

La sûreté est définie par l'absence d'échecs d'assertion/alignement et la présence de fiats valides (hypothèse ou divergence) pour toute liste d'entrées alternative.
La preuve démontre que si un programme est sûr, l'ensemble des entrées qu'un observateur apprend ( $k_\ell$ ) est un sous-ensemble des entrées autorisées par la politique de libération ( $RP_\ell$ ), intersecté avec la connaissance de progrès.
Ce résultat valide l'approche consistant à imposer la sécurité via la vérification relationnelle des annotations du programme plutôt que par une surveillance complexe du temps d'exécution de toutes les exécutions possibles.

C. Vérification vérifiée par machine

L'ensemble du développement, y compris les définitions corrigées et le théorème principal, a été vérifié par machine dans Rocq. Cela confirme que les corrections apportées au papier CN sont fondamentalement saines, tout en mettant en lumière des détails subtils dans les preuves qui avaient été manqués dans les esquisses originales écrites par l'humain.

D. Expérience avec l'IA agentique

Le papier documente l'utilisation d'une IA agentique (Claude Code) dans le processus de formalisation. L'auteur note que bien que l'IA ait été capable de générer des infrastructures non triviales et des preuves de routine, elle a nécessité une supervision humaine pour :

Corriger les formalisations erronées de lemmes (ex: Lemme 3).
Identifier et corriger les lacunes logiques dans la définition du "fiat de divergence".
Affiner les définitions de la connaissance ( $k_\ell$ ) pour utiliser des préfixes plutôt que l'égalité, un changement imposé par des contre-exemples trouvés par l'IA.
Empêcher l'IA de renforcer excessivement les hypothèses ou d'introduire des hypothèses de décidabilité inutiles.

4. Résultats

Correction formelle : La preuve vérifiée par machine confirme que la condition de sûreté révisée implique correctement la propriété de sécurité épistémique pour le modèle de programme réactif.
Résolution des failles de CN : Les failles spécifiques de la preuve CN de 2018 concernant l'alignement des exécutions et la définition de la politique de libération ont été résolues.
Faisabilité de la formalisation assistée par l'IA : L'étude démontre que l'IA agentique peut efficacement aider à traduire des spécifications mathématiques complexes en preuves vérifiées par machine, à condition que l'expert humain guide activement l'outil, corrige ses erreurs logiques et gère l'architecture globale de la preuve.

5. Signification et revendications

Le papier revendique des contributions modestes mais significatives :

Cadre unificateur : Il offre un cadre corrigé et général pour exprimer et vérifier des politiques de flux expressives en utilisant la logique épistémique et les annotations relationnelles.
Vérification pratique : En montrant que la sûreté (une propriété amenable à la surveillance au runtime et à la preuve inductive) implique la sécurité, ce travail comble le fossé entre les spécifications de politiques de haut niveau et les propriétés de programme imposables.
Fiabilité de la vérification par machine : Ce travail souligne la nécessité de la vérification par machine, même pour des développements théoriques dans des contextes idéalisés, car elle expose des erreurs subtiles que la revue humaine pourrait manquer.
L'IA dans les méthodes formelles : Il fournit un cas d'étude concret de l'utilisation de l'IA agentique pour des développements formels substantiels, soulignant à la fois le potentiel de gains d'efficacité et le besoin critique d'expertise humaine pour garantir la rigueur logique.

L'auteur déclare explicitement que le développement de règles de preuve compositionnelles pour la condition de sûreté reste un problème ouvert et que le présent travail se concentre sur les fondements sémantiques et le théorème d'implication principal. Le papier est dédié à David Basin, en reconnaissance de son rôle pionnier dans la formalisation vérifiée par machine.