Vous êtes ici

Une plate-forme multi-domaine d’aide à la conception et à l’analyse d’arbres d’attaque

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)
Contact(s)
NomAdresse e-mailTéléphone
Sophie Pinchinat
sophie.pinchinat@irisa.fr
0299847254
Sujet de thèse
Descriptif

Contexte : 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éploie une solide expertise en sécurité :
en collaboration avec la DGA (et plus particulièrement avec Lionel van Aertryck) depuis plusieurs années, elle développe un outil ATSyRA (Attack Tree Synthesis for Risk Analysis, voir http://atsyra2.irisa.fr/) [10] dont le but est d’assister les experts dans la conception et l’analyse d’arbres d’attaque pour la
détection de vulnérabilités de systèmes.

État de l'art : Le modèle d’arbres d’attaque [11, 8] 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. Parce
que les systèmes à protéger et les arbres construits manuellement sont devenus très complexes,
on remarque un besoin grandissant pour des outils d’assistance.
On observe la formation d’une communauté (https://www7.in.tum.de/~kraemerj/flyer-workshop.html) de chercheurs en méthodes formelles qui vise à
concevoir des approches mathématiques pour répondre aux besoins des experts, et en particulier,
pour ce qui concerne leur assistance dans la construction et l’analyse des arbres d’attaques.
Les travaux principaux consistent à munir les arbres d’attaque de sémantiques formelles qui
offrent un raisonnement rigoureux et des algorithmes d’analyse (quantitative) [8, 6, 7, 3], de
comparaison d’arbres [5], et de génération automatisées [9, 12, 4]
L’équipe LogicA, membre de cette communauté, est aujourd’hui parmi l’une des équipes
les plus expertes au niveau mondial dans l’application des méthodes formelles basées sur les
techniques de vérification et de synthèse. Ses travaux ont la particularité de raisonner sur
les arbres au regard d’une description formelle du système à protéger [1, 2, 9, 10]. Grâce à
une collaboration pérenne avec la DGA, l’équipe peut orienter ses efforts d’investigation vers
des problèmes pertinents. D’une part, l’outil ATSyRA évolue continuellement pour répondre aux
exigences de fonctionnalités et d’expressivité utiles en pratique aux experts, et d’autre part, les
travaux théoriques menés s’alimentent très sainement de problèmes concrets que les utilisateurs
lui posent. Il est important de souligner que nos collègues à l’étranger ont exprimé leur regret
de ne disposer d’une opportunité telle que la nôtre.

Objectif de la thèse : L’outil ATSyRA, en évolution constante, est le fruit d’un travail qui
a débuté en 2015 par la thèse de Maxime Audinot (en 3ème année actuellement) subventionnée
par la DGA dans le cadre du dispositif PEC. Notre correspondant scientifique à la DGA est Lionel van Aertryck, et cette thèse est co-encadrée par Barbara Kordy (experte en arbres
d’attaque) et membre du projet EMSEC de l’IRISA.
Le logiciel est développé par l’équipe LogicA avec l’aide de Didier Vojtisek (ingénieur de
recherche du SED de l’IRISA et expert en ingénierie dirigée par les modèles). Ce logiciel dispose
d’un large panel de fonctionnalités. Les experts peuvent :
- Décrire le modèle de leur bâtiment ; on peut aujourd’hui s’appuyer sur le logiciel de
modélisation 3D Sketchup 3;
-  Décrire des objectifs d’attaque, des arbres d’attaque ;
- Synthétiser des attaques du système pour un objectif d’attaque donné ;
- Situer une attaque dans un arbre d’attaque (en cours de développement) ;
- Analyser la qualité des raffinements d’un arbre ;
- Synthétiser des arbres d’attaque (en cours de développement).

Même si l’outil ATSyRA est actuellement dédié à l’analyse de risque pour la sécurité physique, l’ensemble des méthodes déployées en son sein offre un potentiel d’ouverture à d’autres
domaines de la sécurité, et en particulier à la sécurité informatique. Un prototype a été réalisé
l’été dernier par l’étudiante Florence Wacheux, candidate principale pour cet appel de sujet de
thèse cyber 2018.

Le sujet de cette thèse propose en axe principal une ouverture d’ATSyRA à la sécurité informatique, mais aussi à la sécurité organisationnelle, et, en axe secondaire, une étude théorique
solide pour un passage à plus grande échelle.

Techniques envisagées : L’ouverture du logiciel ATSyRA à d’autres domaines métier soulève
des questions profondes de conception de la plate-forme. Il s’agit de faire coexister plusieurs
langages dédiés (un langage par domaine, physique, cyber et organisationnel) qui permettront
de spécifier un système hétérogène, donc plus réaliste. Ces considérations doivent être soigneusement étudiées car la solution proposée sera la colonne vertébrale de la plate-forme. Elle devra
permettre de “connecter” plusieurs savoir-faire que nous développerons ou qui proviendront
de modules externes, tels que des outils de simulations.
En parallèle de cet aspect architecture, le coeur même du logiciel requiert davantage d’investigations de nature théorique. En effet, si la première expérience dans le cadre de la thèse
de Maxime Audinot a permis de mettre au point un prototype prometteur déjà entre les mains
des utilisateurs finaux, il n’en reste pas moins qu’elle a mis en évidence des besoins de passage
à l’échelle à plusieurs niveaux.

- le premier niveau est celui de la taille des objets de l’étude (le système spécifié, les arbres
d’attaque considérés, etc.) qui pose des limites à nos algorithmes.
- le second niveau est celui de la lisibilité des résultats présentés à l’utilisateur (typiquement,
les scénarios d’attaques synthétisés peuvent être longs et difficiles à lire).

Concernant le premier niveau, nous envisageons de recourir à des techniques d’abstraction
pour l’analyse qui permettront de raisonner des objets plus simples. Il est en effet possible de procéder à une
simplification du modèle du système avant de vérifier l'atteignabilité
de l'objectif d'attaque et d'engendrer des scénarios d'attaque. On pourra par exemple abstraire certaines variables du système, diminuant
ainsi significativement le nombres d'états possible dans le système
(la suppression d'une seule variable Booléenne divise par deux ce
nombres d'états). Dans la même veine, les techniques de slicing consistent à calculer les dépendances causales entre les variables du systèmes permettant ainsi une suppression plus contrôlée des ces dernières.

Concernant le deuxième niveau, il nous semble approprié de recourir à des techniques de classification, très récentes et en plein essor dans la famille des techniques communément qualifiées d’apprentissage ; elles permettront ainsi de fournir des comptes rendus intelligibles des résultats produits par nos algorithmes de synthèse, dans l'esprit de [13] qui utilise des arbres de décision pour décrire des stratégies dans un jeu stochastique.

Bibliographie

[1] Maxime Audinot and Sophie Pinchinat. On the soundness of attack trees. In Graphical Models for Security - Third International Workshop, GraMSec 2016, Lisbon, Portugal, June 27, 2016, Revised Selected Papers, pages 25–38, 2016.


[2] Maxime Audinot, Sophie Pinchinat, and Barbara Kordy. Is my attack tree correct ? In Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I, pages 83–102, 2017.


[3] Olga Gadyatskaya, René Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay, Mads Chr. Olesen, and Danny Bøgsted Poulsen. Modelling Attack-defense Trees Using Timed Automata. In FORMATS, volume 9884 of Lecture Notes in Computer Science, pages 35–50.
Springer, 2016.

[4] Olga Gadyatskaya, Ravi Jhawar, Sjouke Mauw, Rolando Trujillo-Rasua, and Tim A. C. Willemse. Refinement-aware generation of attack trees. In Security and Trust Management - 13th International Workshop, STM 2017, Oslo, Norway, September 14-15, 2017, Proceedings, pages 164–179, 2017.


[5] Ross Horne, Sjouke Mauw, and Alwen Tiu. Semantics for specialising attack trees based on linear logic. Fundamenta Informaticae, 153(1-2) :57–86, 2017.


[6] Barbara Kordy, Sjouke Mauw, and Patrick Schweitzer. Quantitative questions on attack–defense trees. In International Conference on Information Security and Cryptology, pages
49–64. Springer, 2012.


[7] Rajesh Kumar, Enno Ruijters, and Mariëlle Stoelinga. Quantitative Attack Tree Analy-
sis via Priced Timed Automata. In FORMATS, volume 9268 of LNCS, pages 156–171.
Springer, 2015.

[8] Sjouke Mauw and Martijn Oostdijk. Foundations of Attack Trees. In ICISC, volume 3935 of LNCS, pages 186–198. Springer, 2005.


[9] Sophie Pinchinat, Mathieu Acher, and Didier Vojtisek. Towards synthesis of attack trees for supporting computer-aided risk analysis. In Software Engineering and Formal Methods - SEFM 2014 Collocated Workshops : HOFM, SAFOME, OpenCert, MoKMaSD, WS-
FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers, pages 363–375, 2014.


[10] Sophie Pinchinat, Mathieu Acher, and Didier Vojtisek. Atsyra : An integrated environment for synthesizing attack trees - (tool paper). In Graphical Models for Security - Second
International Workshop, GraMSec 2015, Verona, Italy, July 13, 2015, Revised Selected Papers, pages 97–101, 2015.


[11] Bruce Schneier. Attack Trees : Modeling Security Threats. Dr. Dobb’s Journal of Software Tools, 24(12) :21–29, 1999.


[12] Roberto Vigo, Flemming Nielson, and Hanne Riis Nielson. Automated generation of attack trees. In Computer Security Foundations Symposium (CSF), 2014 IEEE 27th, pages 337–
350. IEEE, 2014.

[13] Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelı́k, Andreas Fellner, and Jan Křetı́nskỳ. Counterexample explanation by learning small strategies in markov decision
processes. In International Conference on Computer Aided Verification, pages 158–177. Springer, 2015.

Début des travaux: 
01/09/2018
Mots clés: 
cyber sécurité, arbres d'attaques, conception, vérification, méthodes formelles
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes