Résumé Technique : La Synthèse de Bouclier comme Analyse de Défendabilité pour les Réseaux Adversaires

1. Énoncé du Problème

Les outils actuels d'évaluation de la sécurité des réseaux souffrent d'une lacune fondamentale. Les outils de vérification statique peuvent confirmer la joignabilité et l'isolement sur des configurations fixes, mais échouent à modéliser des adversaires stratégiques. Inversement, l'apprentissage par renforcement (RL) pour la cybersécurité entraîne des agents adaptatifs contre des attaquants simulés, pourtant une politique qui survit à un adversaire peut échouer face à un autre, et aucune méthode informelle ne peut certifier qu'une topologie de réseau est fondamentalement indéfendable.

Les approches de Apprentissage par Renforcement Protégé (ShRL - Shielded Reinforcement Learning) existantes traitent généralement la synthèse de bouclier comme un mécanisme d'application au moment de l'exécution (runtime). Dans ce paradigme, les spécifications de logique temporelle sont compilées en automates pour restreindre les actions d'un agent pendant l'entraînement ou le déploiement. Cependant, ce cadrage présente de graves limitations :

• Scalabilité : La synthèse à états explicites croît de manière exponentielle avec les variables d'état, limitant le calcul traitable à de petits environnements.
• Fragilité du Modèle : Les garanties sont liées au modèle. Si la dynamique déployée diffère du modèle de transition supposé (mismatch de modèle), le bouclier « sûr » peut affirmer une sécurité là où elle n'existe pas.
• Observabilité Partielle : Les formulations standards peinent avec les processus de décision markoviens partiellement observables (POMDP) sans hypothèses d'abstraction fortes.

Les auteurs soutiennent que traiter la synthèse de bouclier comme un filtre d'exécution est le « mauvais produit ». Ils proposent plutôt de recadrer cette même machinerie de théorie des automates comme un instrument analytique de conception (design-time). L'objectif n'est pas de produire une politique sûre pour un agent déployé, mais de générer des informations structurelles et des certificats formels sur la question de savoir si un système est défendable, où il est vulnérable, et comment les changements architecturaux affectent la défendabilité.

2. Méthodologie

Le papier instancie cette perspective à travers un Jeu de Sécurité à Double Spécification Contrainte pour la défense de réseau.

2.1 Le Jeu de Défense de Réseau

Le système modélise un segment de réseau critique comme un graphe dirigé où les hôtes ont des statuts (Propre, Compromis, Détecté, Isolé, Détruit). Le jeu implique deux joueurs :

• Défenseur : Les actions incluent la surveillance, l'isolement, la restauration et la réparation des hôtes.
• Attaquant : Les actions incluent la propagation de la compromission et la destruction des hôtes.

2.2 Doubles Spécifications et Application Asymétrique

L'innovation architecturale centrale est l'utilisation de deux spécifications de logique temporelle indépendantes compilées en automates à états finis déterministes (DFA), appliquées de manière asymétrique :

1. Spécification du Défenseur ($\phi_D$) : Définit l'objectif de sécurité (ex: les actifs critiques ne doivent pas être simultanément compromis). Cet automate ($A_D$) instancie l'ensemble initial non sûr ($U$) du jeu de sécurité. Si le système entre dans un état où $A_D$ est dans un état de rejet, le jeu est non sûr.
2. Spécification de l'Attaquant ($\phi_A$) : Impose des contraintes opérationnelles sur l'adversaire (ex: un budget d'au plus 2 actions « Détruire » par engagement). Cet automate ($A_A$) filtre les actions légales de l'attaquant lors du calcul de l'attracteur. L'attaquant ne peut choisir que des transitions qui maintiennent $A_A$ dans un état acceptant.

Cette asymétrie est cruciale : $\phi_D$ définit ce qui ne doit jamais arriver, tandis que $\phi_A$ définit ce que l'attaquant ne peut pas faire.

2.3 Solution du Jeu de Sécurité et Calcul de l'Attracteur

Le cadre construit un jeu produit combinant l'état du réseau, l'indicateur de tour, et les états des deux automates. Il calcule la Région Gagnante ($W$) pour le défenseur en utilisant un algorithme d'attracteur à point fixe :

• L'Attracteur ($Attr^*$) est l'ensemble des états à partir desquels l'attaquant peut forcer une violation de $\phi_D$ indépendamment de la stratégie du défenseur.
• Le calcul est modifié pour respecter $\phi_A$ : un sommet d'attaquant n'entre dans l'attracteur que s'il possède un successeur légal (satisfaisant $\phi_A$) déjà présent dans l'attracteur.
• Verdict de Défendabilité : Le produit principal est un certificat binaire : l'état initial $s_0 \in W$ ? Si oui, la topologie est défendable ; si non, aucune stratégie de défense n'existe.
• Extraction du Bouclier : Le bouclier (une table de correspondance des actions sûres) est dérivé comme un témoin du verdict, et non comme un contrôleur d'exécution.

2.4 Métriques de Défendabilité et Empreinte

Pour dépasser le verdict binaire, les auteurs dérivent six métriques pour former une Empreinte de Défendabilité (Defensibility Fingerprint) :

• Niveau 1 (Métriques de Jeu Formel) : Dérivées de la décomposition par couches de l'enveloppe de l'attracteur (la distance des états par rapport à la violation).
  • Attaquabilité (ATK) : Exposition pondérée de la région gagnante à l'attracteur.
  • Ratio de Sinking (SNK) : Fraction des états non violants absorbés dans la région non sûre.
  • Friction du Bouclier (FRC) : Fraction des actions du défenseur bloquées par le bouclier pour maintenir la sécurité.
  • Pente de l'Attracteur (STP) : Entropie de la distribution des couches (escarpée vs pente douce).
  • Proximité de Violation (VPX) : Réciproque du nombre moyen d'étapes avant la violation.
• Niveau 2 (Métrique Opérationnelle) :
  • Ratio de Dominance de l'Attaquant (ADR) : Dérivé de l'Apprentissage par Renforcement Multi-Agent (MARL) Adversaire Protégé. Deux apprenants minimax-Q jouent au sein de la région gagnante $W$. La métrique mesure la fraction moyenne d'hôtes contrôlés par l'attaquant à l'équilibre.

3. Contributions Clés

1. Jeu de Sécurité à Double Spécification Contrainte : Une formulation où l'objectif de sécurité du défenseur et les contraintes opérationnelles de l'attaquant sont compilés dans des DFA séparés avec des rôles d'application asymétriques (amorçage de l'ensemble non sûr vs filtrage des successeurs).
2. Verdict de Défendabilité comme Produit Principal : Élévation de la région gagnante du statut d'étape intermédiaire à celui de livrable principal — un certificat formel de défendabilité.
3. Empreinte de Défendabilité : Un artefact de diagnostic unifié combinant six métriques (cinq formelles, une opérationnelle) pour caractériser les configurations de réseau.
4. MARL Adversaire Protégé comme Diagnostic : Utilisation du comportement post-convergence du MARL (Ratio de Dominance du Défenseur) non pas comme une métrique de performance d'agent, mais comme un diagnostic continu de la topologie.
5. Analyse « What-If » : Démonstration que la sécurité formelle et l'efficacité opérationnelle capturent des aspects distincts de la sécurité, révélant que de petits changements architecturaux peuvent radicalement modifier les résultats opérationnels tout en laissant les marges de sécurité formelle presque inchangées.

4. Résultats Expérimentaux

Le cadre a été évalué sur une topologie de référence à 5 hôtes avec un bord de contour de contournement VPN « oublié ». Cinq cas « what-if » ont été analysés :

• Baseline : Topologie de référence.
• Cas 2 (Totalement Connecté) : Augmentation de la connectivité (de 6 à 13 arêtes).
• Cas 3 (Destructions Illimitées) : Suppression des contraintes de ressources de l'attaquant.
• Cas 4 ($\phi_D$ Relaxée) : Réduction de l'exigence de nombre minimum d'hôtes actifs.
• Cas 5 (Suppression du VPN) : Retrait de l'arête spécifique de contournement VPN.

Principales Conclusions :

• Découplage des Couches : Dans le Cas 2 (totalement connecté), les métriques de sécurité formelle (taille de la Région Gagnante, Attaquabilité) sont restées presque identiques à la baseline. Cependant, le résultat opérationnel (Ratio de Dominance du Défenseur) s'est effondré de ~54% à ~23%. Le jeu formel disait « la survie est possible », mais la couche opérationnelle révélait que le défenseur est submergé.
• Sensibilité à une Seule Arête : Dans le Cas 5 (retrait du contournement VPN), la taille de la région gagnante formelle a changé de façon négligeable (23 730 à 23 858 états), mais le Ratio de Dominance du Défenseur a bondi de 53,9% à 80,7%. Cela démontre qu'une seule faille architecturale peut rendre un système formellement défendable opérationnellement indéfendable.
• Perturbation de Spécification : L'assouplissement des contraintes (Cas 3 et 4) a déplacé les deux couches de manière cohérente, confirmant que les spécifications gouvernent la géométrie du jeu, qui dicte à son tour le comportement opérationnel.

5. Signification et Revendications

Le papier affirme que la synthèse de bouclier est la plus précieuse non pas comme mécanisme de déploiement d'agents sûrs, mais comme un cadre pour répondre à des questions architecturales.

• Changement de Produit : Le résultat est un verdict de défendabilité et des informations structurelles, non une politique sûre. Le bouclier est un témoin dérivé, non le livrable.
• Instrument de Conception : Le cadre permet aux architectes de demander « Cette configuration est-elle défendable ? », « À quel point est-elle défendable ? », et « Quels changements améliorent la marge ? » avec des garanties formelles.
• Nécessité des Deux Couches : Le jeu de sécurité formel et la couche MARL opérationnelle sont nécessaires et non redondants. Un système peut être formellement défendable (la survie est possible) mais opérationnellement submergé (la survie est pratiquement impossible face à un adversaire adaptatif).
• Diagnostics Actionnables : L'« Empreinte de Défendabilité » fournit un moyen visuel et quantitatif de comparer les configurations, révélant que de petits changements topologiques (comme une seule règle de pare-feu) peuvent avoir des impacts opérationnels massifs que l'analyse statique ou la simulation informelle pourraient manquer.

Les auteurs reconnaissent les limites, notamment la scalabilité de l'analyse à états explicites (limitée à de petits sous-systèmes, $|V| \le 7$) et l'hypothèse de transitions déterministes. Cependant, ils soutiennent que pour le régime des segments de réseau critiques et restreints où les décisions architecturales sont prises, le cadre offre une méthode rigoureuse et traitable pour quantifier la défendabilité que les outils existants ne peuvent offrir.