Résumé technique : Contrôle supervisé actif pour la préservation de l'opacité

Énoncé du problème

L'ingénierie des systèmes modernes repose de plus en plus sur les méthodes formelles pour vérifier la sécurité, pourtant, lorsqu'un système est jugé non sécurisé, une refonte fondamentale est souvent trop coûteuse ou irréalisable, particulièrement pour les systèmes hérités ou embarqués. Les théories classiques de contrôle supervisé traitent ce problème en restreignant dynamiquement les chemins d'exécution du système, en activant ou en désactivant des actions contrôlables pour appliquer des politiques de sûreté ou de sécurité. Cependant, ce paradigme classique de restriction d'actions est insuffisant face aux attaques par analyse temporelle (timing attacks), une classe puissante d'attaques par canal auxiliaire où les adversaires déduisent des données internes sensibles en mesurant les variations de temps d'exécution et de réponse.

Dans de tels scénarios, le simple blocage d'actions échoue car le rythme des événements lui-même fuit des informations critiques. Pour atténuer ces vulnérabilités, les systèmes doivent manipuler le comportement temporel, souvent en insérant des délais artificiels pour lisser les variances temporelles. De plus, les recherches existantes sur l'opacité (une propriété de sécurité basée sur le langage garantissant que les secrets restent cachés aux observateurs) se sont largement concentrées sur les automates finis ou les modèles basés sur les états. Ce document traite de l'écart dans la gestion de l'opacité basée sur le langage au sein d'un cadre d'Algèbre de Processus Temporels (TPA), spécifiquement pour les systèmes équivalents aux machines de Turing, où ni le superviseur ni l'attaquant ne possèdent une information complète sur le comportement du système.

Méthodologie

Le document emploie un cadre d'Algèbre de Processus Temporels (TPA), une extension du Calcul de Systèmes Communiquants (CCS) de Milner. La TPA introduit une action de temps discrète ($t$) pour modéliser l'écoulement du temps, permettant la représentation formelle des attaques temporelles et des fuites d'informations.

Concepts fondamentaux

1. Opacité et fonctions d'observation :

   • L'opacité est définie comme la propriété selon laquelle, pour toute trace satisfaisant un prédicat secret $\phi$, il existe une autre trace ne satisfaisant pas $\phi$ qui est indiscernable pour un observateur sous une fonction d'observation spécifique $O$.
   • Le document formalise diverses fonctions d'observation ($O$) pour modéliser les capacités de l'attaquant :
     • Statique : Les actions sont observées indépendamment du contexte.
     • Dynamique : L'observation d'une action dépend de l'historique des actions précédentes.
     • Orwellienne/m-Orwellienne : L'observation dépend de l'historique complet ou d'une fenêtre de $m$ actions précédentes.
   • Le cadre suppose une information asymétrique : l'attaquant ($O$) et le superviseur ($O_S$) peuvent avoir des fonctions d'observation différentes et une visibilité partielle.

2. Superviseur Actif :

   • Contrairement aux superviseurs traditionnels qui ne font que désactiver des actions, le Superviseur Actif proposé possède une double capacité :
     1. Désactivation d'actions : Il peut interdire des actions contrôlables spécifiques issues d'un ensemble $C$.
     2. Insertion de temps : Il peut injecter dynamiquement des séquences d'actions de temps ($t$) dans le flux d'exécution.
   • Le superviseur opère sous une observabilité partielle ($O_S$) et vise à garantir que la trace supervisée résultante appartient à un ensemble de Traces Sûres ($K_{P,\phi,O}$), où le prédicat secret $\phi$ ne peut être déduit par l'attaquant.

3. Modélisation Formelle :

   • Les fonctions d'observation, les prédicats et les superviseurs sont modélisés comme des processus au sein du cadre TPA. Cela permet d'utiliser les techniques de vérification standard (équivalence de traces, bisimulation) pour analyser les interactions entre le système, le superviseur et l'attaquant.
   • Le système est modélisé comme un contexte $C(P, O_S, Sup)$, où le superviseur intercepte et modifie l'exécution du processus $P$ en fonction de ses observations.

Contributions Clés

Le document présente trois contributions principales :

1. Nouveau cadre de superviseur actif sous visibilité partielle :
   Les auteurs introduisent un modèle de superviseur qui opère sous une information asymétrique et incomplète. Ce modèle combine de manière unique les capacités de désactivation d'actions avec l'insertion dynamique d'actions temporelles pour atténuer activement les fuites d'informations, ciblant spécifiquement les canaux auxiliaires temporels.

2. Formalisation des fonctions d'observation asymétriques :
   L'étude formalise les scénarios où l'attaquant et le superviseur possèdent des fonctions d'observation distinctes (par exemple, statique vs dynamique, ou différents niveaux de visibilité). Cela permet de modéliser des contextes de sécurité réalistes où aucune des deux entités n'a une visibilité totale, et où leurs vues de l'historique d'exécution divergent.

3. Délimitation des frontières de décidabilité :
   Le document établit un ensemble complet de résultats de décidabilité et d'indécidabilité concernant l'existence de tels superviseurs. Il cartographie les limites de la faisabilité de la vérification à travers divers types de systèmes (états finis vs équivalents à Turing), des granularités d'observation et des capacités respectives des attaquants et des superviseurs.

Résultats

L'analyse théorique produit les résultats clés suivants :

• Indécidabilité dans les cas généraux :

  • Vérifier si un superviseur spécifique est valide pour un processus et une opacité de langage donné est indécidable en général (Proposition 3).
  • Déterminer s'il existe un quelconque superviseur garantissant la sécurité pour un processus donné est également indécidable (Proposition 4). Cela découle de l'indécidabilité de l'opacité de langage elle-même dans les modèles équivalents à Turing.

• Décidabilité dans les cas restreints :

  • Si le processus $P$ est à états finis, que les fonctions d'observation sont statiques et que le prédicat secret $\phi$ (et sa négation) est définissable de manière finie (modélisé par des processus de test à états finis), alors :
    • Vérifier si un superviseur est valide est décidable.
    • Comparer les superviseurs et trouver un superviseur maximal (celui qui restreint le plus faiblement le comportement du système) est décidable.
    • L'existence d'un superviseur maximal à états finis est garantie (Propositions 7 et 8).

• Attaques temporelles et atténuation :

  • Le document définit un système comme étant sujet aux attaques temporelles s'il est opaque sous une observation "abstraite par le temps" mais ne l'est pas sous une observation "sensible au temps".
  • Il prouve que si un prédicat est temporellement dépendant (signifiant qu'une trace secrète peut devenir non-secrète par l'insertion de délais temporels) et que le superviseur possède une précision d'observation au moins égale à celle de l'attaquant ($O \preceq O_S$), un superviseur existe même avec un ensemble vide d'actions contrôlables ($C = \emptyset$). Dans ce cas, la sécurité est obtenue uniquement par l'insertion de délais temporels (Proposition 9).

• Contraintes de contrôlabilité :

  • Si l'ensemble des traces sûres n'est pas contrôlable (c'est-à-dire qu'il existe une trace sûre suivie d'une action incontrôlable menant à une trace non sûre), aucun superviseur n'existe (Proposition 2).

Signification et Revendications

Le document prétend fournir un fondement théorique rigoureux pour l'analyse de la sécurité des systèmes dans un contexte d'algèbre de processus, en abordant spécifiquement les limites du contrôle supervisé traditionnel face aux attaques temporelles.

• Pont entre les paradigmes : Il jette un pont entre l'application logique (blocage d'actions) et la manipulation temporelle (insertion de délais), offrant un mécanisme de contrôle unifié pour l'opacité basée sur le langage.
• Modélisation adverse réaliste : En modélisant les attaquants et les superviseurs avec des fonctions d'observation puissantes et asymétriques, le cadre capture la dynamique réaliste des systèmes décentralisés modernes où les agents opèrent sous une visibilité partielle.
• Vérification pratique : Les auteurs affirment que pour les systèmes à états finis avec des observations statiques, le cadre proposé permet la vérification exacte et la synthèse de superviseurs en utilisant des outils existants comme CAAL (Concurrency Workbench Alternating-Time Logic), à condition que les prédicats soient exprimés via le $\mu$-calcul.
• Orientations futures : Le document esquisse modestement des travaux futurs axés sur la synthèse de superviseurs minimisant l'insertion de temps pour réduire la surcharge temporelle (maintenir la QoS) et l'extension du cadre algébrique pour inclure la distribution spatiale, les architectures réseau et les métriques de consommation d'énergie pour la vérification de sécurité multi-domaines.

Ce travail ne propose pas de nouvelles implémentations expérimentales mais établit les conditions mathématiques sous lesquelles un contrôle supervisé actif et sécurisé est théoriquement possible ou impossible, guidant ainsi la conception d'architectures robustes pour les systèmes embarqués et cyber-physiques.