Soutenance de doctorat de Gabriel Ballot : Stratégies optimales de défense active basées sur la vérification formelle de systèmes multi-agents
EDF Lab Paris-Saclay, Auditorium (7 Bd Gaspard Monge, F-91120 Palaiseau)
et en visioconférence
Titre original : Optimal Active Cyber Defence Strategies based on Multi-Agent System Verification
Jury
- Frédéric Cuppens, Professeur, Polytechnique Montréal (Rapporteur)
- Laurent Doyen, Chargé de recherche, CNRS LMF (Rapporteur)
- Francesco Belardinelli, Senior Lecturer, Imperial College London (Examinateur)
- Ioana Boureanu, Professor, University of Surrey (Examinatrice)
- Catalin Dima, Professeur, Université Paris-Est Créteil, LACL (Examinateur)
- Eric Goubault, Professeur, École Polytechnique, LIX (Examinateur)
- Jean Leneutre, Maître de conférence, Télécom Paris, LTCI (Directeur de thèse)
- Vadim Malvone, Maître de conférence, Télécom Paris, LTCI (Co-directeur de thèse)
- Jingxuan Ma, Ingénieur de recherche, EDF R&D, Lab Paris-Saclay (Invitée)
- Hassane Chraibi, Ingénieur de recherche, EDF R&D, Lab Paris-Saclay (Invité)
Résumé
De nombreux systèmes informatiques et industriels sont conçus à un instant donné avec les outils et les connaissances de l’époque, puis évoluent peu. Cette staticité avantage les cyberattaquants, qui peuvent longuement observer le système et planifier des attaques ciblées. Les mécanismes de défense active, tels que les moving target defences (qui reconfigurent fréquemment le système) et les honeypots adaptatifs (qui leurrent les attaquants et étudient leurs capacités), permettent de briser cet avantage. Souvent, les moving target defences actuels modifient le système aléatoirement et selon une fréquence empirique. Cependant, une reconfiguration adaptée à l’activité sur le système optimiserait les défenses en ciblant les zones effectivement menacées et en évitant des reconfigurations inutiles. De même, une meilleure stratégie d’adaptation des honeypots offrirait plus de réalisme et permettrait de mieux cerner les objectifs et le profil des attaquants.
Cette thèse propose des outils pour modéliser les systèmes, les attaquants et les défenseurs sous forme de jeux. Elle s’appuie sur des contributions en vérification formelle de systèmes multi-agents, notamment le model checking, afin d’extraire automatiquement des stratégies d’adaptation ou de reconfiguration répondant à des objectifs temporels et épistémiques. Un formalisme logique, Capacity Alternating-time Temporal Logic (CapATL), a été développé pour raisonner sur des systèmes où les agents ont différents profils. Il s’applique à une large variété de systèmes, de profils et d’objectifs, avec des garanties formelles sur la stratégie obtenue. Pour une applicabilité accrue, CapATL a été étendue à des systèmes probabilistes (avec une distribution a priori sur les profils) et à information imparfaite, nécessitant la résolution de nouveaux défis théoriques en vérification. Nous montrons comment ces formalismes permettent de modéliser un honeypot adaptatif non trivial et d’en extraire une stratégie adaptée pour des objectifs de réalisme, de sécurité et d’identification du profil des attaquants.