Vous êtes ici

Théorie des jeux et logiques pour l'analyse de robustesse et de vulnérabilité de systèmes multi-agents. Applications à la sécurité.

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
http://www-logica.irisa.fr/
Directeur de thèse
Sophie Pinchinat
Co-directeur(s), co-encadrant(s)
François Schwarzentruber
Contact(s)
Sujet de thèse
Descriptif

La sécurité fait l'objet d'une attention grandissante dans nos sociétés d'aujourd'hui afin de protéger des ressources critiques dont l'endommagement aurait un coût prohibitif tant en matériel, en environnement, en patrimoine, en connaissances ou en vies humaines.

L'équipe LogicA du laboratoire 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 pour la vulnérabilité 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é, telle que la sécurité informatique et la sécurité organisationnelle.

Pour l'instant, l'outil ATSyRA repose sur l'hypothèse que la seule entité active est un unique attaquant et que ce dernier dispose d'une information complète. Ces premiers travaux prometteurs révèlent la pertinence d'une recherche fondamentale qui permettra de transférer des résultats mathématiques pour mener des analyses encore plus réalistes. En particulier, il n'est aujourd'hui pas encore immédiat de pouvoir aborder l'analyse de vulnérabilité d'un système, qu'il soit physique, informatique ou organisationnel, par génération automatisée de scénarios d'attaque dans le cas réaliste où l'entité attaquante ne dispose que d'une information partielle sur le système ou si les entités du système sont composées de plusieurs agents (plusieurs attaquants, plusieurs vigiles). De plus, on constate que les approches existantes séparent deux points de vue pourtant très corrélés : d'une part, celui du défenseur qui révèle la robustesse du système, et d'autre part, celui de l'attaquant qui révèle sa vulnérabilité.

Le sujet de cette thèse porte sur l'utilisation de la théorie des jeux multi-joueurs comme cadre unificateur dans lequel défense et attaque sont représentées symétriquement. Plus précisément, ce cadre de théorie des jeux devra permettre de considérer aussi bien des objectifs d'attaque que de défense, voire des propriétés plus générales. Ainsi, il sera envisageable d'intégrer des aspects épistémiques liés à l'information partielle, tels que « l'attaquant vole le document en sachant que le vigile ne sait jamais où il se trouve », ou « le vigile ne peut jamais imaginer que l'attaquant fait partie du personnel ». Les outils de la théorie des jeux devront permettre de développer des méthodes/algorithmes pour générer des stratégies complexes, comme par exemple, une stratégie de coordination d'agents de l'entité défenseur optimale (sur des critères attendus tels que le nombre de vigiles, la fréquence de patrouille, les itinéraires de patrouille, ou la fréquence de communication), ou encore une stratégie de coordination d'agents de l'entité attaquante optimale (sur des critères tels que le nombre d'attaquants, ou l'expertise requise pour ces attaquants).

La méthodologie pour ce projet de recherche est de développer des langages adaptés afin de décrire les objectifs et les propriétés : typiquement, on favorisera une utilisation pertinente de logiques pour les systèmes multi-agents mixant dynamique et connaissance, une spécialité de l'équipe LogicA reconnue à l'échelle internationale. Ces logiques ou leur fragmedétection d'intrusion, nts pertinents devront mener à une algorithmique efficace pour réaliser le calcul de stratégies gagnantes et d'équilibres. À plus long terme, ces algorithmes auront pour vocation de venir enrichir la plate-forme ATSyRA.

 

Bibliographie

Cremers, C., & Mauw, S. (2012). Operational semantics and verification of security protocols. Springer Science & Business Media.

 

Fennelly, L. (2016). Effective physical security. Butterworth-Heinemann.

 

Kordy, B., Mauw, S., Radomirović, S., & Schweitzer, P. (2014). Attack–defense trees. Journal of Logic and Computation.

 

Apt, K. R., & Grädel, E. (Eds.). (2011). Lectures in game theory for computer scientists. Cambridge University Press.

 

Nisan, N., Roughgarden, T., Tardos, E., & Vazirani, V. V. (Eds.). (2007). Algorithmic game theory (Vol. 1). Cambridge: Cambridge

University Press.

 

Van Ditmarsch, H., van Der Hoek, W., & Kooi, B. (2007). Dynamic epistemic logic (Vol. 337). Springer Science & Business Media.

 

Alur, R., Henzinger, T. A., & Kupferman, O. (2002). Alternating-time temporal logic. Journal of the ACM (JACM), 49(5), 672-713.

 

Chatterjee, K., Henzinger, T. A., & Piterman, N. (2010). Strategy logic. Information and Computation, 208(6), 677-693.

 

Brihaye, T., Da Costa, A., Laroussinie, F., & Markey, N. (2009, January). ATL with strategy contexts and bounded memory. In International Symposium on Logical Foundations of Computer Science (pp. 92-106). Springer Berlin Heidelberg.

 

Début des travaux: 
01/09/2017
Mots clés: 
sécurité, analyse des vulnérabilités d'un système, théorie des jeux, logiques dynamiques épistémiques
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes