Foundations of Attack-Defense Trees With Dynamic Semantics

J'ai le plaisir de vous inviter à ma défense publique de thèse, intitulée "Foundations of Attack-Defense Trees With Dynamic Semantics".

Elle aura lieu le 13 mars 2025 à 15h dans la salle Mirzakhani du bâtiment De Vinci, sur le campus de la plaine de Nimy - 15 Avenue Victor Maistriau 7000 Mons.

La présentation sera aussi accessible via zoom à l'adresse suivante:  https://us06web.zoom.us/j/88587746476?pwd=INRxajn3sI85SPB8Siw0FzqsWJxT9L.1 

(mot de passe : merci de contacter Alexandre TEREFENKO alexandre [*] terefenkoirisa [*] fr )

Résumé:

La sécurité est un sujet de plus en plus important dans notre société actuelle, afin de protéger les ressources critiques contre la divulgation d'informations, le vol ou les dommages. Le modèle informel des arbres d'attaque introduit par Schneier, et largement utilisé dans l'industrie, est recommandé dans le rapport de l'OTAN de 2008 pour gouverner l'évaluation de la menace dans l'analyse des risques. Depuis, les arbres d'attaque ont fait l'objet de nombreux travaux théoriques abordant différentes approches formelles. Ces travaux théoriques considèrent souvent deux généralisations différentes des arbres d'attaque, soit en ajoutant des contre-mesures (arbres d'attaque-défense), soit en considérant un système dynamique au lieu d'un cadre statique.

Nous présentons d'abord un cadre mathématique pour traiter simultanément les deux généralisations des arbres d'attaque : nous équipons les arbres d'attaque-défense (ADT) d'une sémantique de langage (de traces), permettant d'avoir une interprétation dynamique originale des contre-mesures. Fait intéressant, l'expressivité des ADT coïncide avec les langages sans étoile, et les contre-mesures imbriquées impactent l'expressivité des ADT. Avec une notion appropriée de "profondeur des contre-mesures", nous exposons une hiérarchie stricte des langages sans étoile qui ne coïncide pas avec les hiérarchies classiques. De plus, nous définissons les ADT-games, des jeux (similaire aux jeux d'Ehrenfeucht-Fraïssé) capables de déterminer si un langage peut être exprimé par un ADT avec un certain nombre de contre-mesures imbriquées.