Aurélien Pepin : Optimisation par colonies de fourmis pour la recherche d'attaques

De Ensiwiki
Aller à : navigation, rechercher

Certaines attaques informatiques, dites « attaques d'initié », sont réalisées par des individus possédant déjà un accès au système d'information. Ce travail évalue une façon de détecter ces attaques : l'optimisation par colonies de fourmis.

Cornues.png
Titre du projet Optimisation par colonies de fourmis pour la recherche d'attaques
Cadre IRL

Labo Laboratoire d'informatique de Grenoble (LIG)
Équipe VASCO
Encadrants Akram Idani


Dans le cadre de l'introduction à la recherche en laboratoire, cette page récapitule les résultats obtenus.

  • Étudiant : Aurélien Pepin (étudiant à l'Ensimag, filière ISI)
  • Encadrant : Akram Idani (maître de conférences à l'Ensimag)


Introduction

Attaques d'initié

La sécurité des systèmes d’information est un thème de recherche actif. Des impératifs comme la protection des données personnelles et la confidentialité motivent le développement d’outils pour vérifier qu’une application informatique est sécurisée. L’objectif est de se prémunir des attaques contre les systèmes d’information.

Ces attaques peuvent être de deux types : externes ou internes. Elles sont dites externes quand l’attaquant cherche à nuire au système d’information depuis l’extérieur : injection de code, déni de service, etc. Moins étudiées, les attaques internes, dites « attaques d’initié » sont réalisées par des individus qui possèdent déjà un accès au système d’information. Pourtant, les attaques d’initié peuvent causer des dommages importants. Elles consistent pour l’attaquant à abuser des permissions qui lui sont données pour en acquérir de nouvelles. Détecter ces attaques est difficile car l’attaquant est le plus souvent une personne de confiance avec une bonne compréhension du système d’information et de ses failles.

Exemple introductif

Nous prenons l'exemple d'un système d'information (simplifié) d'une banque. Le modèle fonctionnel en UML ci-dessous décrit le lien entre un client (Customer) et un compte bancaire (Account). Un client possède au moins un compte bancaire. Un compte bancaire appartient au plus à un client.


Modèle fonctionnel en UML, développé par l'équipe VASCO.


Ce modèle fonctionnel définit des opérations sur les comptes (comme transferFunds pour un virement bancaire). En revanche, il n'est pas suffisant pour spécifier la politique de sécurité du système d'information. Pour cela, SecureUML, une extension d'UML, permet de compléter le modèle fonctionnel selon les règles du modèle RBAC (« Role-based access control »). Le modèle RBAC définit la politique de sécurité d'un système d'information comme la donnée de rôles et de permissions.

Un rôle est l'équivalent dans le S.I. d'une fonction dans l'organisation. Pour cet exemple, deux exemples de rôles sont celui du client et du conseiller bancaire. Une permission est un accès à certaines opérations du S.I. Donner l'autorisation de changer l'adresse d'un client ou donner l'autorisation de créditer un compte sont des exemples de permissions.

Le modèle ainsi complété avec la politique de sécurité est le suivant :


Modèle de sécurité associé au modèle fonctionnel, en SecureUML.


Ce modèle définit deux rôles : CustomerUser (client) et AccountManager (conseiller bancaire). Les permissions traduisent le fait que le client peut lire ses données et effectuer des opérations financières. Elles traduisent aussi le fait que le conseiller bancaire a tous les droits sur l’entité Customer mais qu’il ne peut que créer ou alimenter des comptes.

Considérons l'attaque d'initié suivante : un conseiller bancaire veut transférer de l'argent depuis le compte d'un client. D'après le modèle statique de sécurité ci-dessus, ce scénario est impossible. La contrainte d'autorisation (encadré bleu) impose à l'utilisateur qui veut débiter un compte d'en être le propriétaire.

De la spécification à la vérification formelle

Existe-t-il une suite d'opérations autorisées qui permet de transgresser le modèle statique de sécurité ? Pour le savoir, il faut un moyen dynamique d'animer le modèle de sécurité. L'équipe VASCO a développé à cet effet la plateforme B4MSecure. Elle permet de transformer des spécifications (SecureUML, RBAC) en machines abstraites de la méthode B.

La méthode B est une méthode formelle qui permet de modéliser les états d'exécution du système d'information. Les états forment un graphe orienté dont les arcs sont appelés « transitions ». Dans notre exemple, les transitions sont des opérations du système : changer l'adresse d'un client, connecter un utilisateur, effectuer un virement, etc.

La recherche d'une attaque d'initié est donc équivalente à la recherche d'un état critique de la machine abstraite.
Représentation simplifiée du graphe de transition d'états, avec l'état initial et un état critique.
L'image ci-contre est une représentation simplifiée du graphe de transition d'états.


Un état contient des données appelées variables. Ces variables changent d'un état à l'autre en fonction des transitions. Elles permettent de représenter ce que contient le système. Dans l'exemple ci-contre, nous souhaitons savoir si un conseiller bancaire peut usurper le compte d'un client. Nous nous intéressons donc aux variables suivantes : la liste des utilisateurs (Customer), la liste des comptes (Account) et à qui appartient chaque compte (AccountOwner).

Cela permet de représenter l'attaque d'initié comme un prédicat.

Un état initial permet de donner des valeurs aux variables. La suite des transitions à choisir pour aller de l'état initial à l'état critique correspond à la suite des opérations qui permet de transgresser la politique de sécurité.

Optimisation par colonies de fourmis

Un model-checker pour B comme ProB propose une recherche exhaustive de l'état critique. Toutes les transitions sont explorées dans un parcours mixte profondeur/largeur. Cette méthode est coûteuse en temps et inefficace puisqu'elle inclut des transitions qui n'ont aucune chance de mener à l'état critique (par exemple, changer l'adresse d'un client).

L'idée pour éviter cette explosion combinatoire est d'effectuer un parcours intelligent de l'espace de recherche. Pour ce faire, nous nous intéressons à l'optimisation par colonies de fourmis. Les algorithmes de colonies de fourmis désignent une famille d’algorithmes de recherche heuristique. Ils s’inspirent des stratégies et des schémas naturels mis en place par les fourmis pour des objectifs comme la recherche de nourriture. Développés à partir des années 1990, leur intérêt s’est vite manifesté dans des domaines tels que l’optimisation combinatoire où une recherche exhaustive se révèle souvent très coûteuse.

Les algorithmes de colonies de fourmis opèrent généralement à deux niveaux :

  • au niveau local, des fourmis artificielles explorent un espace de recherche de proche en proche pour se rapprocher de sites jugés intéressants ;
  • au niveau global, la colonie de fourmis collecte les informations des fourmis pour faire émerger une solution globale intéressante.

Dans ce travail, l’algorithme employé est API, fondé sur l’espèce Pachycondyla apicalis.

Algorithme Pachycondyla apicalis (API)

Les fourmis explorent les alentours du nid. C'est un découpage de l'espace de recherche. Source.
La colonie envoie n fourmis (dites fourrageuses) autour du nid. Chaque fourmi crée puis garde en mémoire p sites de chasse. En parallèle des autres fourmis, la fourmi choisit aléatoirement un de ses sites de chasse noté S, et commence une exploration locale. Si l’exploration est fructueuse, elle remplace S par son nouveau site de chasse S'.

Sinon, elle compte un échec supplémentaire pour le site S. Si le nombre d’échecs de S dépasse un seuil appelé patience locale, il est oublié et remplacé par un nouveau site aléatoire. La patience permet de creuser une piste pendant quelques tours plutôt que de l’abandonner tout de suite.

La colonie rappelle régulièrement ses fourrageuses et regarde leurs résultats.

Si un site de chasse d’une fourmi est meilleur que ceux des autres fourmis et que la position actuelle du nid, tout le nid se déplace et la mémoire de toutes les fourmis repart de zéro. La procédure recommence alors : les fourmis sont de nouveau disséminées autour du nid.

Implémentation de l'algorithme

L'algorithme API s'applique à n'importe quel espace de recherche, discret ou continu. À tout moment de l'exécution, il fournit une solution valide dans l'espace de recherche. C'est le domaine d'application qui motive certains choix d'implémentation :

  • L'heuristique d'exploration : comment se déplacer dans l'espace de recherche ?
  • L'évaluation d'un site de chasse d'une fourmi : qu'est-ce qu'une exploration fructueuse ?
  • Le critère d'arrêt de l'algorithme.
  • Les paramètres (nombre de fourmis, taille de la mémoire d'une fourmi, seuil de patience, etc.).

Exploration de l'espace de recherche

Dans ce travail, l'espace de recherche est l'espace d'états généré par la machine abstraite de la méthode B. Chaque état est un site de chasse potentiel. Explorer cet espace de recherche consiste à choisir les transitions pour passer d'un état à un autre.

L'heuristique proposée pour l'exploration locale consiste à choisir aléatoirement une transition parmi celles qui quittent l'état courant ou le retour en arrière. Le retour en arrière permet aux fourmis de ne pas rester bloquées dans un sous-espace de recherche.


À gauche, les états explorés par les fourmis pour cet exemple sont en rouge.
À droite, les transitions de retour enregistrées après cette exploration sont en rouge. Les états qui deviennent accessibles grâce aux retours en arrière sont en bleu.


Le retour en arrière est implémenté en gardant une trace de l'origine de chaque transition. Cela revient à construire un arbre couvrant des états visités. Sur la figure ci-dessus, le graphe de gauche montre quelques états (en rouge) explorés par des fourmis. Le graphe de droite montre les transitions de retour en arrière enregistrées par cette exploration. Les états en bleu sont ceux qui deviennent accessibles grâce au retour en arrière.

Évaluation d'un état

Le but de l'algorithme API est d'exclure les états qui ne permettent pas de reproduire l'attaque d'initié. Il faut donc savoir si une exploration locale a été fructueuse, c'est-à-dire si l'état courant permet de se rapprocher de l'état critique.

Dans l'algorithme, ceci est le rôle de la fonction d'évaluation des états. C'est une fonction objectif à valeurs dans [0; 1] que l'on souhaite minimiser. Si un état est évalué à 0, alors c'est un état critique. L'idée est donc de mesurer la ressemblance entre deux états par rapport au prédicat choisi (ensemble de variables et leurs valuations). Plus deux états sont semblables, plus il est probable qu'il faudra peu de transitions pour passer de l'un à l'autre.


L'état critique semble plus proche de l'état E1 que de l'état E2.


L'exemple ci-dessus reprend les conventions du graphe de la section Vérification formelle.
Dans cet exemple, l'état critique semble plus proche de l'état E1 que de l'état E2, d'où f(E1) < f(E2).

La fonction objectif est une moyenne des mesures de ressemblances entre les valeurs des variables de l'état courant et de l'état critique. Seules les variables du prédicat (ici, Customer, Account et AccountOwner) sont prises en compte. Dans le rapport, ces mesures de ressemblances sont définies pour plusieurs types de variables : des ensembles, des entiers voire des booléens.

Résultats

L'implémentation de l'algorithme utilise l'API en Java du model-checker ProB.
Le critère de performance est le nombre d'états visités. Il faut au minimum 11 états visités pour parvenir à l'état critique.

La recherche exhaustive (déterministe) a besoin de 36 000 états visités.
Pour 20 exécutions de l'algorithme API :

  • L'algorithme trouve l'état critique dans 95% des cas ;
  • Il a besoin de 247 états visités en moyenne.

Sur cet exemple, l'algorithme API est donc beaucoup plus efficace qu'une recherche exhaustive. Il parvient à éliminer la majorité des états inintéressants et à guider rapidement les fourmis vers l'état critique. Il faut toutefois noter que les chemins critiques repérés par API contiennent des transitions inutiles (dues à la patience locale des fourmis). L'algorithme pourra être testé sur des exemples de scénarios plus compliqués.

Conclusion

Je souhaite remercier Akram Idani, encadrant de cette introduction à la recherche en laboratoire, pour son suivi régulier et son implication.

Ce sujet m’a donné une première vue d’ensemble de la recherche académique. Mon travail a été l’occasion d’approfondir ou de découvrir des domaines variés comme les algorithmes de colonies de fourmis, les méthodes formelles avec la méthode B ainsi que le model checking dans ses aspects pratiques.

Ressources

Rapport : accéder au rapport (PDF)
Soutenance : accéder à la présentation (PDF)
Implémentation : via GitHub