L'équipe LogicA de l'IRISA de l'université de Rennes 1 développe une solide expertise en sécurité : en collaboration avec la DGA depuis plusieurs années, elle développe l'outil ATSyRA (Attack Tree Synthesis for Risk Analysis) dont le but est d'assister les experts dans la conception d'arbres d'attaque détecter les vulnérabilités de bâtiments critiques ; le modèle d'arbres d'attaque, très répandu dans l'industrie, est préconisé dans le rapport 2008 de l'OTAN pour régir l'évaluation de la menace en analyse de risques. Cet outil connaît aujourd'hui une ouverture à d'autres domaines de la sécurité, tels que la sécurité informatique et la sécurité organisationnelle.
L'outil ATSyRA développé à l'IRISA depuis 2015 offre à l'expert en sécurité de nombreuses fonctionnalités dont le but est d'aider les experts à une analyse des vulnérabilités du système qu'il investigue. L'originalité de l'approche est de corréler une description du système et la construction d'arbres d'attaque [6] pour des objectifs divers, alors que la littérature existante ne le propose pas [8]. Pour l'heure, l'outil repose sur deux hypothèses restrictives - qui dans la majorité des approches pour les arbres d'attaque sont "mathématiquement" éludées, en l'absence du système : (a) un unique acteur, l'attaquant, et (b) qui dispose d'une information parfaite du système. En sus, l'outil ATSyRA ne traite pas encore les arbres d'attaque-défense parce qu'il est force de constater le fait suivant. Dans la littérature [7], l'acteur défenseur n'a pas la même représentation mathématique que celle de l'acteur attaquant : alors que l'attaquant, qui révèle la vulnérabilité du système, est décrit jusqu'aux feuilles, le défenseur qui incarne la robustesse du système, apparaît sous la forme d'annotations de contre-mesures dans les arbres.
Si l'on veut améliorer l'assistance logicielle des experts en sécurité, il est indispensable d'asseoir les fondements des arbres d'attaque-défense pour modéliser des cas réalistes, où les acteurs du système sont multiples avec une information partielle sur le système. À notre connaissance, il n'existe pas aujourd'hui de proposition dans ce sens.
Le sujet de la thèse vise à développer une théorie mathématique solide et exploitable en pratique, qui s'inspire de la théorie des jeux multi-joueurs comme cadre unificateur [2].
- Dans la théorie développée, les acteurs de la défense et de l'attaque seront représentés de façon symétrique, avec le concept de coalition et avec leurs objectifs propres. Les objectifs doivent pouvoir intégrer des aspects épistémiques pour l'information partielle, tels que « l'attaquant vole le document tout en sachant que le vigile ne sait jamais où il se trouve », ou « l'attaquant aboutit sans que le vigile ne l'ait pris pour un personnel ».
- Cette théorie devra circonscrire les cas automatisables (tout n'est pas calculable !) mais qui conservent un bon niveau d'expressivité pour traiter des cas utiles en pratique.
- Outre la notion de stratégies, elle devra permettre une représentation intelligible et exploitable des ensembles de stratégies [9]. Si les arbres d'attaque sont une telle représentation, il faut savoir que l'état de l'art pour leur génération ne concerne qu'un joueur et repose sur des techniques adhoc inapplicables aux cas multi-joueurs.
[1] Alur, R., Henzinger, T. A., & Kupferman, O. (2002). Alternating-time temporal logic. Journal of the ACM (JACM), vol. 49, No. 5, pp. 672-713.
[2] Chatterjee, K., Henzinger, T. A., & Piterman, N. (2010). Strategy logic. Information and Computation, vol. 208, No. 6, pp. 677-693.
[3] Doyen, L., & Raskin, J. F. (2011). Games with imperfect information: Theory and algorithms. Lectures in Game Theory for Computer Scientists, pp. 185-212.
[4] Van Ditmarsch, H., van Der Hoek, W., & Kooi, B. (2007). Dynamic Epistemic Logic, vol. 337. Springer Science & Business Media.
[5] Bastien Maubert, Aniello Murano, Sophie Pinchinat, Francois Schwarzentruber, Silvia Stranieri. Dynamic Epistemic Logic Games with Epistemic Temporal Goals. ECAI 2020 24th European Conference on Artificial Intelligence, Santiago de Compostela, August 29-September 2, 2020.
[6] Maxime Audinot, Barbara Kordy, Sophie Pinchinat, and Wojciech Widel. Beyond 2014: Formal methods for attack tree-based security modeling. ACM Computing Surveys 52(4), 2019.
[7] Kordy, B., Mauw, S., Radomirović, S., & Schweitzer, P. (2014). Attack–defense trees. Journal of Logic and Computation.
[8] Maxime Audinot and Sophie Pinchinat and Barbara Kordy. Is my attack tree correct?
ESORICS 2017 - European Symposium on Research in Computer Security, Oslo, Norway on September 11-13, 2017.
[9] Soumya Paul, Ramaswamy Ramanujam, Sunil Simon. Automata and Compositional Strategies in Extensive Form Games. Models of Strategic Reasoning 2015: 174-201.
[10] Thomas Brihaye, Julie De Pril, Sven Schewe: Multiplayer Cost Games with Simple Nash Equilibria. LFCS 2013: 59-73.
[11] Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, Marie van den Bogaard: The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games. Log. Methods Comput. Sci. 16(4) (2020)