Stratégies Optimales de Cybersécurité basées sur la Vérification Formelle de Systèmes Multi-Agents

De nombreux systèmes informatiques et industriels sont conçus à un instant donné avec les outils et les connaissances de l’époque, mais évoluent peu par la suite. Ce statisme profite aux cyberattaquants, dont les techniques progressent fréquemment et qui peuvent observer longuement le système et planifier des attaques ciblées. Les mécanismes de cyberdéfense active – tels que les défenses par cible mouvante qui reconfigurent fréquemment le système, et les pots de miel adaptatifs qui piègent les attaquants et analysent leurs capacités – réduisent cette vulnérabilité. Trouver une stratégie de cyberdéfense active efficace pour sécuriser le système et leurrer les attaquants constitue un défi majeur. Les solutions actuelles, fondées sur la théorie des jeux analytique et l’apprentissage automatique, n’offrent pas une solution générale pour déterminer des stratégies de défense avec de fortes garanties face à des attaques multi-étapes. Ces limites peuvent être surmontées en utilisant la vérification formelle de systèmes multi-agents. Cependant, ce domaine ne permet pas de modéliser un aspect essentiel en cybersécurité : les profils d’attaquant.Cette thèse propose des outils pour modéliser les systèmes de cyberdéfense active interagissant avec des attaquants aux profils variés, formaliser des objectifs de sécurité, et déduire des stratégies de défense ayant des garanties élevées. Une contribution centrale est l’introduction du concept de capacité, qui modélise les profils d’agent et donne lieu à un nouveau formalisme logique: Capacity Alternating-time Temporal Logic (CapATL). Il offre la possibilité d’exprimer et vérifier des objectifs stratégiques, temporels et de capacité (e.g. identification du profil d’attaquant), permettant ainsi de caractériser le comportement stratégique souhaité des cyberdéfenses actives. CapATL a été étendu aux environnements à information imparfaite (CapATEL) et probabilistes (ATL-SA) pour tenir compte des contraintes des systèmes réels, nécessitant la résolution de nouveaux défis théoriques en vérification. Nous montrons comment ces formalismes permettent de modéliser un pot de miel adaptatif non trivial et d’en extraire une stratégie adaptée pour des objectifs de réalisme, sécurité, gestion de ressources et identification du profil des attaquants.