{"id":307,"date":"2016-09-02T15:54:14","date_gmt":"2016-09-02T13:54:14","guid":{"rendered":"http:\/\/members.loria.fr\/MDuflot\/?page_id=307"},"modified":"2016-09-02T15:57:09","modified_gmt":"2016-09-02T13:57:09","slug":"recherche","status":"publish","type":"page","link":"https:\/\/members.loria.fr\/MDuflot\/recherche\/","title":{"rendered":"Recherche"},"content":{"rendered":"<p>Cette page contient une pr\u00e9sentation de mes th\u00e8mes de recherche, un pointeur sur ma liste de publications, la description de certains travaux ainsi que les transparents de certains de mes expos\u00e9s.<\/p>\n<h2 id=\"themes\">Th\u00e8mes de recherche<\/h2>\n<ul>\n<li><strong>V\u00e9rification formelle<\/strong><br \/>\nLa v\u00e9rification formelle, que ce soit d&rsquo;un point de vue th\u00e9orique pour d\u00e9finir de nouvelles m\u00e9thodes, formalismes ou outils ou d&rsquo;un point de vue pratique sur des \u00e9tudes de syst\u00e8mes r\u00e9els, est un th\u00e8me commun \u00e0 tous mes travaux de recherche. Elle se d\u00e9cline dans chacun des points suivants.<\/li>\n<li><strong>Syst\u00e8mes probabilistes<\/strong><br \/>\nTout comme le th\u00e8me pr\u00e9c\u00e9dent, les syst\u00e8mes probabilistes sont pr\u00e9sents dans \u00e0 peu pr\u00e8s tous mes travaux de recherche.J&rsquo;ai commenc\u00e9 \u00e0 m&rsquo;y int\u00e9resser du fait de l&rsquo;importance des syst\u00e8mes probabilistes pour r\u00e9soudre des conflits dans des syst\u00e8mes distribu\u00e9s, principalement pour s&rsquo;assurer que, avec probabilit\u00e9 1, la sym\u00e9trie d&rsquo;un syst\u00e8me sera rompue et les conflits ne se reproduiront pas \u00e0 l&rsquo;infini. Je me suis donc d&rsquo;abord int\u00e9ress\u00e9e \u00e0 v\u00e9rifier des propri\u00e9t\u00e9s qualitatives sur des syst\u00e8mes probabilistes. J&rsquo;ai ensuite abord\u00e9 les propri\u00e9t\u00e9s quantitatives (<em>i.e.<\/em> o\u00f9 la valeur exacte des probabilit\u00e9s est calcul\u00e9e) par le biais de protocoles de communication comme CSMA\/CD ou Bluetooth, d\u00e9taill\u00e9s dans le point suivant. Plus r\u00e9cemment je me suis int\u00e9ress\u00e9e \u00e0 la v\u00e9rification statistique de syst\u00e8mes probabilistes.<\/li>\n<li><strong>Syst\u00e8mes distribu\u00e9s<\/strong>Au cours de ma th\u00e8se, j&rsquo;ai \u00e9tudi\u00e9 des syst\u00e8mes distribu\u00e9s, et plus pr\u00e9cis\u00e9ment je me suis int\u00e9ress\u00e9e \u00e0 prouver la convergence de syst\u00e8mes distribu\u00e9s de taille param\u00e9tr\u00e9e, \u00e0 savoir que, quelle que soit la configuration initiale du syst\u00e8me, quel que soit le chemin suivi (suivant l&rsquo;algorithme), le syst\u00e8me va arriver au bout d&rsquo;un nombre de transitions fini dans l&rsquo;ensemble souhait\u00e9.<br \/>\nJ&rsquo;ai depuis continu\u00e9 \u00e0 m&rsquo;int\u00e9resser \u00e0 de tels syst\u00e8mes, notamment par l&rsquo;\u00e9tude et la v\u00e9rification de protocoles de communication pour lesquels l&rsquo;absence de contr\u00f4le global peut engendrer des conflits (deux entit\u00e9s qui ne parviennent pas \u00e0 communiquer, ou encore deux entit\u00e9s qui envoient des messages simultan\u00e9ment engendrant une collision). Dans la plupart des cas que j&rsquo;ai \u00e9tudi\u00e9s, la solution pour r\u00e9soudre les confilts a \u00e9t\u00e9 la pr\u00e9sence de comportements probabilistes, comme d\u00e9taill\u00e9 dans le point suivant.<\/li>\n<li><strong>V\u00e9rification statistique<\/strong>En ce qui concerne la v\u00e9rification de syst\u00e8mes probabilistes, deux m\u00e9thodes principales existent. La v\u00e9rification num\u00e9rique est bas\u00e9e sur le calcul des valeurs r\u00e9elles des probabilit\u00e9s. Des outils de model-checking comme PRISM existent et permettent de v\u00e9rifier ou d&rsquo;\u00e9valuer les syst\u00e8mes. Cependant, ce caclcul des valeurs exactes a un co\u00fbt en terme de complexit\u00e9 et atteint ses limites sur de trop grands syst\u00e8mes. La v\u00e9rification statistique consiste pour sa part \u00e0 \u00e9chantillonner les ex\u00e9cutions suivant les probabilit\u00e9s d&rsquo;occurence des \u00e9v\u00e9nements, tout en \u00e9valuant le long de chaque ex\u00e9cution une quantit\u00e9. On \u00e9value ensuite une formule sur ces quantit\u00e9s, comme par exemple l&rsquo;esp\u00e9rance, et des th\u00e9or\u00e8mes statistiques nous permettent soit d&rsquo;\u00e9valuer la pr\u00e9cision de notre r\u00e9sultat en fonction du nombre d&rsquo;ex\u00e9cutions test\u00e9es, soit de dire quand on peut arr\u00eater l&rsquo;exp\u00e9rience pour avoir une pr\u00e9cision et un degr\u00e9 de confiance souhait\u00e9s. L&rsquo;avantage principal de la v\u00e9rification statistique est qu&rsquo;elle peut s&rsquo;appliquer sur de tr\u00e8s grands syst\u00e8mes car elle ne n\u00e9cessite pas de calculer l&rsquo;ensemble de l&rsquo;espace des \u00e9tats. Nous avons dans ce cadre pr\u00e9sent\u00e9 un formalisme logique bas\u00e9 sur des automates hybrides lin\u00e9aires permettant d&rsquo;une part une s\u00e9lection tr\u00e8s fine des ex\u00e9cutions et d&rsquo;autre part d&rsquo;\u00e9valuer des quantit\u00e9s bien plus complexes qu&rsquo;une probabilit\u00e9.<\/li>\n<li><strong>Th\u00e9orie des jeux<\/strong>Lors d&rsquo;un travail en collaboration avec Nicolas Markey et Patricia Bouyer, nous nous sommes int\u00e9ress\u00e9s \u00e0 la permissivit\u00e9 dans les jeux finis. L&rsquo;approche classique en terme de strat\u00e9gie consiste \u00e0 choisir, \u00e0 chaque \u00e9tape contr\u00f4l\u00e9e par un joueur fix\u00e9, une transition parmi celles possibles afin d&rsquo;atteindre un objectif. Une multi-strat\u00e9gie consiste pour sa part \u00e0 offrir au joueur la possibilit\u00e9 de choisir parmi un sous-ensemble de transitions possibles. L&rsquo;id\u00e9e de la permissivit\u00e9 est de limiter au minimum les possibilit\u00e9s du joueur tout en l&rsquo;assurant d&rsquo;atteindre son objectif. Ceci est possible en assignant un co\u00fbt au fait de l&#8217;emp\u00eacher de prendre une transition. dans ce cadre nous avons prouv\u00e9 l&rsquo;existence de multi strat\u00e9gies optimales et sans m\u00e9moire. Nous avons \u00e9galement conis\u00e9r\u00e9 le cas \u00ab\u00a0d\u00e9compt\u00e9\u00a0\u00bb o\u00f9 le fait de bloquer une transition plus tard dans une ex\u00e9cution co\u00fbte moins que de bloquer la transition d\u00e8s le d\u00e9part. Dans ce cadre nous avons montr\u00e9 que les strat\u00e9gies optimales peuvent ne pas exister ou n\u00e9cessiter de la m\u00e9moire, mais qu&rsquo;une strat\u00e9gie optimale peut \u00eatre approch\u00e9e en combinant deux strat\u00e9gies sans m\u00e9moire.<\/li>\n<li><strong>S\u00e9curit\u00e9<\/strong><br \/>\nJe me suis int\u00e9ress\u00e9e \u00e0 la s\u00e9curit\u00e9 au travers des deux th\u00e9matiques suivantes :<\/p>\n<ul>\n<li>Fuite d&rsquo;informationLa fuite d&rsquo;information est une question importante dans le domaine de la s\u00e9curit\u00e9 informatique. Il s&rsquo;agit de d\u00e9terminer si un utilisateur de bas niveau (i.e. non autoris\u00e9) peut r\u00e9ussir \u00e0 obtenir des informations (m\u00eame partielles) sur le comportement haut niveau (i.e. confidentiel) du syst\u00e8me.<br \/>\nDans notre \u00e9tude, contrairement \u00e0 l&rsquo;approche classique possibiliste, le fait d&rsquo;obtenir de l&rsquo;information a \u00e9t\u00e9 repr\u00e9sent\u00e9 \u00e0 l&rsquo;aide de probabilit\u00e9s, et d\u00e9fini par rapport \u00e0 une propri\u00e9t\u00e9 portant (entre autres) sur le comportement haut niveau du syst\u00e8me.<br \/>\nDans ce cadre, nous nous sommes int\u00e9ress\u00e9s \u00e0 d\u00e9finir diff\u00e9rentes formes de fuite d&rsquo;information relatives \u00e0 diff\u00e9rentes classes de propri\u00e9t\u00e9s. Nous avons donn\u00e9 des caract\u00e9risations que doit satisfaire un syst\u00e8me pour garantir l&rsquo;absence de fuite d&rsquo;information pour une propri\u00e9t\u00e9, ou pour un ensemble de propri\u00e9t\u00e9s d&rsquo;une classe. Nous avons \u00e9galement montr\u00e9 comment notre formalisme bas\u00e9 sur les propri\u00e9t\u00e9s permettait d&rsquo;exprimer des notions classiques possibilistes de fuite d&rsquo;information. Nous avons \u00e9galement \u00e9tudi\u00e9 des questions de d\u00e9cidabilit\u00e9 (et de complexit\u00e9) de l&rsquo;existence de fuite d&rsquo;information, dans le cas o\u00f9 le syst\u00e8me est une cha\u00eene de Markov et la propri\u00e9t\u00e9 est r\u00e9guli\u00e8re.<\/li>\n<li>Participation \u00e0 l&rsquo;encadrement de la th\u00e8se de Myrto Arapinis sur des probl\u00e8mes de d\u00e9cidabilit\u00e9 de la v\u00e9rification de protocoles cryptographiquesLa v\u00e9rification de protocoles cryptographiques est une t\u00e2che difficile, compliqu\u00e9e par le fait que plusieurs instances d&rsquo;un m\u00eame protocole peuvent \u00eatre ex\u00e9cut\u00e9es en m\u00eame temps et par le fait que la taille des messages n&rsquo;est pas born\u00e9e et donc l&rsquo;espace des messages possibles est infin. Dans nos travaux nous avons introduit une notion de protocoles \u00ab\u00a0bien form\u00e9s\u00a0\u00bb et prouv\u00e9 que, pour ces protocoles, si une attaque existe alors une attaque avec des messages de longueur born\u00e9e (par la taille du plus grand message d&rsquo;une ex\u00e9cution honn\u00eate du protocole) existe aussi. Cela permet ainsi de limiter le branchement dans l&rsquo;espace de recherche des attaques. Nous avons \u00e9galement montr\u00e9 qu&rsquo;un \u00e9tiquetage tr\u00e8s simple permet de rendre un protocole bien form\u00e9 et ainsi soit de supprimer certaines attaques, soit de simplifier sa v\u00e9rification.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<h2 id=\"publis\">Publications<\/h2>\n<p>La liste de mes publications est disponible <a href=\"https:\/\/members.loria.fr\/MDuflot\/files\/publis.html\"> ici<\/a><\/p>\n<p>Je maintiens \u00e9galement une liste de mes co-auteurs qui se trouve <a href=\"http:\/\/www.loria.fr\/%7Emduflotk\/publis.html#coauthors\"> par l\u00e0 <\/a><\/p>\n<h2 id=\"talks\">Quelques expos\u00e9s<\/h2>\n<ul>\n<li>Un expos\u00e9 donn\u00e9 en 2006 pour pr\u00e9senter beamer (ou comment faire des pr\u00e9sentations avec LaTeX) et gastex (ou comment dessiner simplement des automates en LaTeX).Depuis j&rsquo;ai chang\u00e9 pour tikz mais pas encore fait d&rsquo;expos\u00e9 dessus :\n<ul>\n<li>Pr\u00e9sentation de beamer <a href=\"https:\/\/members.loria.fr\/MDuflot\/files\/beamertalk.pdf\">version pdf<\/a> et le fichier source <a href=\"https:\/\/members.loria.fr\/MDuflot\/files\/beamertalk.tex\">.tex<\/a><\/li>\n<li>Pr\u00e9sentation de gastex <a href=\"https:\/\/members.loria.fr\/MDuflot\/files\/gastextalk.pdf\">version pdf<\/a> et le fichier source <a href=\"https:\/\/members.loria.fr\/MDuflot\/files\/gastextalk.tex\">.tex<\/a><\/li>\n<\/ul>\n<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Cette page contient une pr\u00e9sentation de mes th\u00e8mes de recherche, un pointeur sur ma liste de publications, la description de certains travaux ainsi que les transparents de certains de mes expos\u00e9s.<\/p>\n<p>Th\u00e8mes de recherche<\/p>\n<ul>\n<li>V\u00e9rification formelle<br \/>\nLa v\u00e9rification formelle, que ce soit d&rsquo;un point de vue th\u00e9orique pour d\u00e9finir de nouvelles m\u00e9thodes, formalismes ou outils ou d&rsquo;un point de vue pratique sur des \u00e9tudes de syst\u00e8mes r\u00e9els, est un th\u00e8me commun \u00e0 tous mes travaux de recherche. Elle se d\u00e9cline dans chacun des points suivants.<\/li>\n<li>Syst\u00e8mes probabilistes<br \/>\nTout comme le th\u00e8me pr\u00e9c\u00e9dent, les syst\u00e8mes probabilistes sont pr\u00e9sents dans \u00e0 peu pr\u00e8s tous mes travaux de recherche.J&rsquo;ai commenc\u00e9 \u00e0 m&rsquo;y int\u00e9resser du fait de l&rsquo;importance des syst\u00e8mes probabilistes pour r\u00e9soudre des conflits dans des syst\u00e8mes distribu\u00e9s,<\/li>\n<\/ul>\n","protected":false},"author":98,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-307","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/pages\/307","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/users\/98"}],"replies":[{"embeddable":true,"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/comments?post=307"}],"version-history":[{"count":3,"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/pages\/307\/revisions"}],"predecessor-version":[{"id":310,"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/pages\/307\/revisions\/310"}],"wp:attachment":[{"href":"https:\/\/members.loria.fr\/MDuflot\/wp-json\/wp\/v2\/media?parent=307"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}