Amira Radhouani - Méthodes formelles pour l’extraction d’attaques internes des Systèmes d’Information

10:30
Vendredi
23
Juin
2017
Organisé par : 
Amira Radhouani
Intervenant : 
Amira Radhouani
Équipes : 
Mots clés : 
Information détaillée : 

Membres du jury :

  • Rapporteurs :
    • Yamine Ait Ameur, professeur, Institut National Polytechnique de Toulouse
    • Leila Jemni Ben Ayed, professeure, Ecole Nationale Sup. d’Informatique de Tunis
  • Examinateurs :
    • Jacques Julliand, professeur, Université de Franche-Comté
    • Amel Borgi, maitre de conférences HdR, Université de Tunis al-Manar
    • Amel Mammar, maitre de conférences HdR, Institut Télécom SudParis,      
  • Directeurs de thèse :
    • Akram Idani, maitre de conférences, Grenoble INP
    • Yves Ledru, professeur, Université Grenoble Alpes
    • Narjès Ben Rajeb, professeure, INSAT Tunis
Résumé : 

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale.
Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. 
Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. 
Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description SecureUML des règles de contrôle d’accès basées sur les rôles.
Ces vulnérabilités étant dues à l’évoution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système.
Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes.
Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles.