Activités de recherche

Cette page contient une présentation de mes thèmes de recherche, un pointeur sur ma liste de publications, la description de certains travaux ainsi que les transparents de certains de mes exposés.

Thèmes de recherche

• Vérification formelle
  La vérification formelle, que ce soit d'un point de vue théorique pour définir de nouvelles méthodes, formalismes ou outils ou d'un point de vue pratique sur des études de systèmes réels, est un thème commun à tous mes travaux de recherche. Elle se décline dans chacun des points suivants.
• Systèmes probabilistes
  Tout comme le thème précédent, les systèmes probabilistes sont présents dans à peu près tous mes travaux de recherche.

  J'ai commencé à m'y intéresser du fait de l'importance des systèmes probabilistes pour résoudre des conflits dans des systèmes distribués, principalement pour s'assurer que, avec probabilité 1, la symétrie d'un système sera rompue et les conflits ne se reproduiront pas à l'infini. Je me suis donc d'abord intéressée à vérifier des propriétés qualitatives sur des systèmes probabilistes. J'ai ensuite abordé les propriétés quantitatives (i.e. où la valeur exacte des probabilités est calculée) par le biais de protocoles de communication comme CSMA/CD ou Bluetooth, détaillés dans le point suivant. Plus récemment je me suis intéressée à la vérification statistique de systèmes probabilistes.

• Systèmes distribués

  Au cours de ma thèse, j'ai étudié des systèmes distribués, et plus précisément je me suis intéressée à prouver la convergence de systèmes distribués de taille paramétrée, à savoir que, quelle que soit la configuration initiale du système, quel que soit le chemin suivi (suivant l'algorithme), le système va arriver au bout d'un nombre de transitions fini dans l'ensemble souhaité.
  J'ai depuis continué à m'intéresser à de tels systèmes, notamment par l'étude et la vérification de protocoles de communication pour lesquels l'absence de contrôle global peut engendrer des conflits (deux entités qui ne parviennent pas à communiquer, ou encore deux entités qui envoient des messages simultanément engendrant une collision). Dans la plupart des cas que j'ai étudiés, la solution pour résoudre les confilts a été la présence de comportements probabilistes, comme détaillé dans le point suivant.

• Vérification statistique

  En ce qui concerne la vérification de systèmes probabilistes, deux méthodes principales existent. La vérification numérique est basée sur le calcul des valeurs réelles des probabilités. Des outils de model-checking comme PRISM existent et permettent de vérifier ou d'évaluer les systèmes. Cependant, ce caclcul des valeurs exactes a un coût en terme de complexité et atteint ses limites sur de trop grands systèmes. La vérification statistique consiste pour sa part à échantillonner les exécutions suivant les probabilités d'occurence des événements, tout en évaluant le long de chaque exécution une quantité. On évalue ensuite une formule sur ces quantités, comme par exemple l'espérance, et des théorèmes statistiques nous permettent soit d'évaluer la précision de notre résultat en fonction du nombre d'exécutions testées, soit de dire quand on peut arrêter l'expérience pour avoir une précision et un degré de confiance souhaités. L'avantage principal de la vérification statistique est qu'elle peut s'appliquer sur de très grands systèmes car elle ne nécessite pas de calculer l'ensemble de l'espace des états. Nous avons dans ce cadre présenté un formalisme logique basé sur des automates hybrides linéaires permettant d'une part une sélection très fine des exécutions et d'autre part d'évaluer des quantités bien plus complexes qu'une probabilité.

• Théorie des jeux

  Lors d'un travail en collaboration avec Nicolas Markey et Patricia Bouyer, nous nous sommes intéressés à la permissivité dans les jeux finis. L'approche classique en terme de stratégie consiste à choisir, à chaque étape contrôlée par un joueur fixé, une transition parmi celles possibles afin d'atteindre un objectif. Une multi-stratégie consiste pour sa part à offrir au joueur la possibilité de choisir parmi un sous-ensemble de transitions possibles. L'idée de la permissivité est de limiter au minimum les possibilités du joueur tout en l'assurant d'atteindre son objectif. Ceci est possible en assignant un coût au fait de l'empêcher de prendre une transition. dans ce cadre nous avons prouvé l'existence de multi stratégies optimales et sans mémoire. Nous avons également coniséré le cas "décompté" où le fait de bloquer une transition plus tard dans une exécution coûte moins que de bloquer la transition dès le départ. Dans ce cadre nous avons montré que les stratégies optimales peuvent ne pas exister ou nécessiter de la mémoire, mais qu'une stratégie optimale peut être approchée en combinant deux stratégies sans mémoire.

• Sécurité
  Je me suis intéressée à la sécurité au travers des deux thématiques suivantes :
  • Fuite d'information

    La fuite d'information est une question importante dans le domaine de la sécurité informatique. Il s'agit de déterminer si un utilisateur de bas niveau (i.e. non autorisé) peut réussir à obtenir des informations (même partielles) sur le comportement haut niveau (i.e. confidentiel) du système.
    Dans notre étude, contrairement à l'approche classique possibiliste, le fait d'obtenir de l'information a été représenté à l'aide de probabilités, et défini par rapport à une propriété portant (entre autres) sur le comportement haut niveau du système.
    Dans ce cadre, nous nous sommes intéressés à définir différentes formes de fuite d'information relatives à différentes classes de propriétés. Nous avons donné des caractérisations que doit satisfaire un système pour garantir l'absence de fuite d'information pour une propriété, ou pour un ensemble de propriétés d'une classe. Nous avons également montré comment notre formalisme basé sur les propriétés permettait d'exprimer des notions classiques possibilistes de fuite d'information. Nous avons également étudié des questions de décidabilité (et de complexité) de l'existence de fuite d'information, dans le cas où le système est une chaîne de Markov et la propriété est régulière.

  • Participation à l'encadrement de la thèse de Myrto Arapinis sur des problèmes de décidabilité de la vérification de protocoles cryptographiques

    La vérification de protocoles cryptographiques est une tâche difficile, compliquée par le fait que plusieurs instances d'un même protocole peuvent être exécutées en même temps et par le fait que la taille des messages n'est pas bornée et donc l'espace des messages possibles est infin. Dans nos travaux nous avons introduit une notion de protocoles ``bien formés'' et prouvé que, pour ces protocoles, si une attaque existe alors une attaque avec des messages de longueur bornée (par la taille du plus grand message d'une exécution honnête du protocole) existe aussi. Cela permet ainsi de limiter le branchement dans l'espace de recherche des attaques. Nous avons également montré qu'un étiquetage très simple permet de rendre un protocole bien formé et ainsi soit de supprimer certaines attaques, soit de simplifier sa vérification.

Publications

La liste de mes publications est disponible ici

Je maintiens également une liste de mes co-auteurs qui se trouve par là

Quelques exposés

• Un exposé donné en 2006 pour présenter beamer (ou comment faire des présentations avec LaTeX) et gastex (ou comment dessiner simplement des automates en LaTeX).Depuis j'ai changé pour tikz mais pas encore fait d'exposé dessus :
  • Présentation de beamer version pdf et le fichier source .tex
  • Présentation de gastex version pdf et le fichier source .tex