💻 computer science

Security Engineering in IIIf, Part II -- Shadowing the IIIf

Ce document étend l'ingénierie de sécurité du cadre Isabelle Insider and Infrastructure (IIIf) en introduisant le concept de « Shadow » de Morgan pour formaliser la sécurité des flux d'informations, résolvant ainsi le paradoxe du raffinement et établissant des conditions pour des raffinements sécurisés illustrés par un exemple de système de radar aérien.

Auteurs originaux : Florian Kammüller

Publié 2026-06-30

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Florian Kammüller

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

La vue d'ensemble : Le problème du « Radar de vol »

Imaginez que vous regardez une application de radar de vol publique sur votre téléphone. Vous voyez des avions se déplacer sur la carte. Habituellement, cela est inoffensif. Mais que se passe-t-il si un avion prend soudainement un détour bizarre, en zigzag, autour d'une zone spécifique ?

Dans le monde réel, les avions ne volent pas en ligne droite juste pour le plaisir. Si un avion dévie soudainement pour contourner une base militaire secrète ou l'emplacement d'une personnalité importante, ce « détour » est un indice. Même si l'application ne vous montre pas la base secrète, le schéma du mouvement de l'avion vous indique exactement où se trouve la zone de danger.

C'est le problème que traite l'article : Comment empêcher les informations secrètes de « fuiter » à travers les effets secondaires du comportement d'un système ?

Les personnages et le décor

Le Système (IIIf) : Considérez cela comme un immense livre de règles ultra-strict pour une ville numérique. Il suit qui est où, quelles règles ils suivent et comment les choses se déplacent. Les auteurs utilisent un outil informatique puissant appelé « Isabelle » pour écrire ce livre de règles si strictement que l'ordinateur peut prouver qu'il est correct.
L'Attaquant (Eve) : Eve est une observatrice indiscrète qui peut voir tout ce que le système montre au public (comme la position de l'avion sur la carte), mais elle n'est pas censée connaître les secrets (comme l'emplacement d'une base secrète).
Le Secret (Localisation critique) : C'est la « zone interdite » que le système tente de protéger.

Le problème : Le « Paradoxe du Raffinement »

Les auteurs expliquent une situation délicate appelée le Paradoxe du Raffinement.

Imaginez que vous concevez un système sécurisé (la version « Abstraite »). Vous prouvez à l'ordinateur qu'Eve ne peut pas deviner le secret. Parfait !
Ensuite, vous décidez de rendre le système meilleur ou plus détaillé (la version « Raffinée »). Peut-être ajoutez-vous une nouvelle fonctionnalité, comme afficher la vitesse de l'avion.

Le Paradoxe : Même si votre nouvelle fonctionnalité semble inoffensive, elle pourrait accidentellement créer une nouvelle « fuite ».

Analogie : Imaginez que vous cachez un mot secret dans un coffre-fort. Vous prouvez que le coffre est sécurisé. Ensuite, vous décidez d'ajouter une petite poignée décorative au coffre. Vous n'avez pas changé la serrure, mais maintenant, si vous secouez le coffre, la poignée cliquette différemment selon l'endroit où se trouve le mot à l'intérieur. Soudain, la poignée révèle le secret.

Dans l'exemple de l'article, si le système calcule la vitesse de l'avion en se basant sur son chemin réel (caché) plutôt que sur son chemin public, le chiffre de la vitesse sera étrange chaque fois que l'avion évite une zone secrète. Eve voit la vitesse étrange et sait instantanément où se trouve la zone secrète. Le système est devenu « plus détaillé », mais il est devenu moins sécurisé.

La Solution : L'« Ombre »

Pour corriger cela, les auteurs introduisent le concept d'Ombre (Shadow), inspiré par un mathématicien nommé Morgan.

Qu'est-ce qu'une Ombre ?
Considérez l'Ombre comme un « Sac de Possibilités » pour l'information secrète.

Au début, l'Ombre est un sac géant contenant chaque possibilité de l'endroit où le secret pourrait se trouver. L'attaquant est totalement confus ; il n'a aucune idée de l'emplacement du secret.
À mesure que le système fonctionne, l'Ombre devrait rester grande. Si l'Ombre rétrécit, cela signifie que l'attaquant a appris quelque chose de nouveau.

L'Objectif : Un système sécurisé est un système où l'Ombre ne rétrécit jamais. Si l'Ombre reste de la même taille, l'ignorance de l'attaquant est préservée. Il n'en sait pas plus qu'au début.

Comment ils ont réparé le Radar de vol

Les auteurs ont appliqué cette idée d'« Ombre » à leur système de Radar de vol :

La Fuite : Dans la version non sécurisée originale, le mouvement de l'avion révélait l'emplacement du secret. L'Ombre rétrécissait car l'attaquant pouvait éliminer certains emplacements en fonction du trajet de l'avion.
La Correction : Ils ont ajouté un mécanisme de « dissimulation ». Lorsqu'un avion doit éviter une zone secrète, le système enregistre le chemin réel dans une boîte secrète (le composant critpos) mais affiche l'avion comme s'il avait volé en ligne droite à travers la zone secrète sur la carte publique.
Le Résultat : Comme la carte publique semble normale, le « Sac de Possibilités » de l'attaquant (l'Ombre) ne diminue jamais. L'attaquant pense toujours que la zone secrète pourrait être n'importe où.

La « Magie » de la preuve

L'article fait deux choses principales :

Équivalence : Ils ont prouvé que « l'Ombre ne rétrécit jamais » est exactement la même chose que la « Non-Interférence » (un terme technique sophistiqué signifiant que « les secrets n'affectent pas ce que le public voit »). C'est comme prouver que « le sac reste plein » est la même chose que « personne n'a volé de pommes ».
La Règle de Sécurité pour les Mises à jour : Ils ont créé une règle (Théorème 2) pour vérifier si une mise à jour future (un raffinement) restera sécurisée.
- La Règle : Si vous ajoutez une nouvelle fonctionnalité, vous devez vérifier si elle dépend du secret. Si la nouvelle fonctionnalité dépend du secret, l'Ombre rétrécira, et la mise à jour est dangereuse.
- Le Piège : Si la nouvelle fonctionnalité est totalement indépendante du secret, l'Ombre reste grande, et la mise à jour est sûre.

Résumé

L'article résout un problème où le fait de rendre un système plus détaillé laisse accidentellement fuiter des secrets. Ils utilisent une « Ombre » (un sac de possibilités) pour suivre ce que l'attaquant sait. Si l'Ombre reste pleine, le système est sécurisé. Ils ont prouvé que si vous suivez leurs règles spécifiques lors de l'ajout de nouvelles fonctionnalités, vous pouvez mettre à jour le système sans laisser échapper accidentellement les secrets.

En bref : Ils ont construit un « garde du corps » mathématique qui vérifie chaque fois que vous ajoutez une nouvelle fonctionnalité à un système, garantissant que la nouvelle fonctionnalité ne chuchote pas accidentellement les secrets au public.

Résumé Technique : L'Ombre de l'Isabelle Insider et du Cadre d'Infrastructure

Énoncé du Problème
Le cadre Isabelle Insider and Infrastructure Framework (IIIf) fournit une base formelle pour l'ingénierie de la sécurité des systèmes impliquant des acteurs humains, des politiques et des composants physiques/logiques, en utilisant un cycle de Raffinement-Risque (RR). Bien que le IIIf supporte le raffinement basé sur les traces et la préservation des propriétés pour les propriétés de sûreté standards (ex: accessibilité), il fait face à une limitation critique concernant le Contrôle de Flux d'Information (IFC). Plus précisément, la propriété de Non-Interférence (NI) — qui garantit que les états de haute sécurité (secrets) n'influencent pas les observations de basse sécurité (publiques) — n'est pas généralement préservée lors du raffinement de la spécification. Ce phénomène, connu sous le nom de « paradoxe du raffinement », signifie qu'une spécification satisfaisant la NI peut engendrer une implémentation raffinée qui fuit des informations via des flux implicites. Les approches de model-checking existantes au sein du IIIf sont insuffisantes pour vérifier de telles propriétés de ensembles de traces, nécessitant une nouvelle méthodologie pour caractériser et garantir des raffinements sécurisés.

Méthodologie
Pour répondre au paradoxe du raffinement, l'article introduit une formalisation du concept de « Shadow » (Ombre) de Morgan dans le cadre du IIIf. La méthodologie procède selon les étapes suivantes :

Intégration d'une Étude de Cas : Les auteurs utilisent une spécification de système de radar de vol (précédemment formalisée dans le IIIf) comme exemple fil rouge. Ce système implique des positions d'aéronefs, des routes et des lieux critiques. La spécification initiale démontre comment des flux d'informations implicites se produisent lorsqu'un aéronef contourne un lieu critique, révélant l'existence de cette criticité à travers des irrégularités observables de la trajectoire de vol.
Formalisation de la Non-Interférence (NI) : La NI est définie dans le IIIf comme une relation d'indistinguabilité sur les transitions d'état. Deux états sont indistinguables pour un attaquant (ayant un niveau d'habilitation $a$ ) si leurs composants observables (ceux avec des étiquettes de sécurité $\leq a$ ) sont identiques. La NI est respectée si, pour toute paire d'états initiaux indistinguables, leurs traces d'exécution subséquentes restent indistinguables.
Définition de l'Ombre (Shadow) : Inspirée par la logique épistémique de Morgan, une « Ombre » est définie comme l'ensemble de toutes les valeurs possibles qu'un composant d'état de sécurité critique pourrait prendre du point de vue de l'attaquant.
- Initialisation : Un composant d'ombre est initialisé à l'« univers » de son type (toutes les valeurs possibles), représentant une ignorance maximale.
- Réduction (Shrinking) : Pendant les transitions d'état, l'ombre « rétrécit » (réduit l'ensemble des valeurs possibles) uniquement si la transition révèle des informations sur le composant secret à l'attaquant.
- Invariant : Un système sécurisé doit satisfaire l'invariant $IFC_a$ , où l'ombre d'un composant secret ne rétrécit pas pendant l'exécution. Si l'ombre rétrécit, cela implique que l'attaquant a acquis des connaissances sur le secret, indiquant une violation de la NI.
Preuve d'Équivalence : L'article établit formellement (sur papier, en raison des limites de quantification de type dans la Logique d'Ordre Supérieur) que l'invariant d'ombre $IFC_a$ est équivalent à la Non-Interférence ( $NI_a$ ). Plus précisément, la négation de la NI (l'existence d'un flux d'information illicite) est montrée comme étant équivalente à l'existence d'un composant dont l'ombre rétrécit.
Caractérisation du Raffinement Sécurisé : Les auteurs définissent une condition pour un raffinement sécurisé. Un raffinement d'un système abstrait $A$ vers un système concret $C$ préserve la sécurité si la fonction de raffinement $E$ , lorsqu'elle est restreinte aux composants d'ombre de $C$ , est injective et compatible avec l'ombre abstraite.

Contributions Clés

Formalisation de l'Ombre dans le IIIf : L'article étend le IIIf avec une définition formelle des composants d'ombre pour les états d'infrastructure, permettant de suivre l'incertitude d'un attaquant concernant les composants d'état secrets.
Équivalence de l'Ombre et de la NI : Il prouve que l'invariant d'ombre ( $IFC_a$ ) est équivalent à la propriété de Non-Interférence ( $NI_a$ ) dans le contexte du modèle de transition d'état du IIIf.
Théorème de Raffinement Sécurisé (Théorème 2) : La contribution principale est un théorème caractérisant le raffinement sécurisé. Il stipule que si une fonction de raffinement $E$ est injective sur les composants d'ombre du système concret et compatible avec l'ombre abstraite, alors l'invariant d'ombre (et donc la NI) est préservé de l'abstrait vers le concret.
Résolution du Paradoxe du Raffinement : La méthodologie fournit un mécanisme pour vérifier qu'une étape de raffinement n'introduit pas de nouveaux flux d'information qui violeraient la NI, répondant ainsi à une faille connue du cycle RR standard du IIIf.

Résultats

Application au Système de Radar de Vol : Les auteurs appliquent la définition de l'ombre au cas d'étude du radar de vol.
- Dans une version non sécurisée (sans mécanismes de dissimulation), l'ombre du composant de localisation critique rétrécit lorsque l'avion contourne une zone critique, prouvant la violation de $IFC_a$ et de la NI.
- Dans une version sécurisée (utilisant un composant critpos pour masquer le contournement réel), l'invariant d'ombre est respecté, confirmant l'absence de flux illicites.
Analyse de Raffinement : L'article démontre que l'ajout d'un nouveau composant (ex: « vitesse ») calculé sur la base de positions cachées constitue un raffinement non sécurisé car il provoque le rétrécissement de l'ombre, violant les conditions d'injectivité/compatibilité du Théorème 2. Inversement, il montre que l'ajout de composants qui ne dépendent pas des secrets et qui sont gérés correctement par la fonction de raffinement préserve la sécurité.
Limites Méta-Théoriques : Les auteurs notent que bien que l'équivalence entre l'Ombre et la NI puisse être raisonnée, la formalisation complète du théorème d'équivalence sur tous les types d'infrastructure est limitée par le système de types d'Isabelle/HOL, car elle nécessite une quantification sur des composants de types différents de l'état.

Signification et Revendications
L'article prétend étendre les capacités d'ingénierie de la sécurité du cadre IIIf en y intégrant le Contrôle de Flux d'Information. Sa signification réside dans :

Réponse au Paradoxe du Raffinement : Il offre une méthodologie concrète pour garantir que les propriétés de sécurité (spécifiquement la NI) sont préservées lors du processus de raffinement, une capacité qui faisait défaut au cadre précédemment.
Pont entre Abstraction et Implémentation : En utilisant le concept d'ombre, le cadre peut désormais raisonner formellement sur l'« ignorance » d'un attaquant et garantir que les raffinements ne réduisent pas par inadvertance cette ignorance (c'est-à-dire ne fuient pas d'informations).
Vérification Pratique : L'approche permet la vérification de systèmes complexes et hétérogènes (combinant des aspects physiques et logiques) là où le model-checking standard échoue.

Les auteurs restent modestes quant à la portée de leur travail, reconnaissant que les preuves d'équivalence sont actuellement établies « sur papier » en raison des contraintes de la théorie des types dans Isabelle/HOL, et que la méthodologie est spécifiquement adaptée au modèle d'infrastructure IIIf plutôt qu'à une logique de langage de programmation généraliste. Ce travail s'appuie sur les concepts fondamentaux de Morgan mais les adapte à un système de transition d'état avec des acteurs et des politiques explicites, évitant le besoin d'une logique épistémique dédiée en exploitant le modèle de droits d'accès des acteurs déjà présent dans le IIIf.