Steve Kremer, ERC Consolidator Grant 2014

Originaire du Luxembourg, Steve Kremer fait ses études à Bruxelles où il termine sa thèse en informatique en 2003. Déjà à l’époque il s’intéresse à l’utilisation de méthodes formelles pour vérifier et analyser des protocoles de sécurité. Au cours de son post-doctorat à l’Université de Birmingham, il travaille sur le vote électronique, et en particulier sur la modélisation de certaines particularités de l’anonymat. Steve Kremer est recruté chez Inria en 2004 comme chargé de recherche au Laboratoire Spécification et Vérification (LSV, CNRS/ENS Cachan), avant de rejoindre le LORIA en 2011.

Steve Kremer mène des recherches sur le vote électronique afin de modéliser certaines propriétés fortes comme la résistance à la coercition (le fait de ne pas pouvoir vendre son vote à un tiers) ou la vérifiabilité (la possibilité de vérifier la sincérité du scrutin). Il travaille également sur la vérification de modules de hardware sécurisés qui permettent de faire des opérations cryptographiques, qui sont par exemple utilisés dans les transactions bancaires pour des opérations sensibles. Un autre aspect de ses recherches, la composition de protocoles, consiste à déterminer si deux protocoles de sécurité assurent encore une protection lorsqu’ils fonctionnent ensemble. Par exemple, il est fréquent qu’un utilisateur choisisse le même mot de passe pour différentes applications. Bien que chacune des applications puisse être sûre séparément, le fait de les utiliser simultanément avec le même mot de passe peut compromettre leur sécurité.

Steve Kremer s’intéresse enfin à la conception d’outils de vérification de ces protocoles. Il faut concevoir des algorithmes de vérification automatique capable d’analyser la sécurité des protocoles. Ces algorithmes se basent généralement sur des techniques empruntées aux assistants de preuve et au model checking.

Dans le cadre de la bourse ERC Consolidator, Steve Kremer souhaite dans un premier temps concevoir des outils de vérification de protocoles pour les propriétés de type anonymat. Auparavant on s’intéressait principalement à la vérification de l’authentification et du secret (la confidentialité de certaines données), des propriétés pour lesquelles des outils de vérification existent. Aujourd’hui l’anonymat prend de l’importance, et exige dans certains contextes que l’on ne puisse pas relier une personne à une action, ou deux actions effectuées par la même personne (unlikability), soit la non-traçabilité. Pour le vote électronique, c’est le fait de ne pas pouvoir faire le lien entre l’identité d’un votant et son vote. Cet aspect se modélise par des propriétés d’équivalence, qui garantissent qu’un adversaire ne peut pas distinguer deux situations différentes lorsqu’elles se présentent.

Un autre aspect de l’ERC Consolidator va consister à étudier des techniques permettant d’exécuter des protocoles de sécurité sur des plateformes non sûres. Précédemment, on considérait en général que les ordinateurs étaient des plateformes sûres, et que les attaques étaient extérieures. Mais on trouve de plus en plus de logiciels malveillants et il n’est plus possible de faire l’hypothèse que les ordinateurs constituent un milieu parfaitement fiable. Le projet va étudier deux familles de techniques pour remédier à ce problème. La première est d’utiliser du hardware dédié pour manipuler des données sensibles, comme des clés cryptographiques, afin d’assurer que les programmes de l’ordinateur n’y ont pas accès. Les puces TPM représentent un exemple d’un tel hardware. La seconde solution est d’utiliser des méthodes multi-facteurs, comme lorsque l’on reçoit un code de confirmation par téléphone pour réaliser un achat par carte bleue. On utilise ici un objet extérieur et déconnecté de l’ordinateur pour confirmer l’authentification. Mais cela pose des problèmes en termes de sécurité, notamment parce que les codes à reproduire doivent être assez courts pour être recopiés facilement par un humain. On doit alors modéliser que ces codes peuvent être attaqués par force brute. Un des buts de l’ERC est alors de concevoir des outils pour étudier les protocoles utilisant ces techniques.

Le troisième volet de l’ERC consiste à utiliser toutes les techniques évoquées pour les appliquer au vote électronique. Bien qu’il existe des protocoles qui assurent la vérifiabilité et l’anonymat, voir même certaines formes de résistance à la coercition, il faut souvent faire l’hypothèse que le matériel du votant est sûr. Un programme malveillant peut pourtant dévoiler l’identité des votants, ou changer le vote des participants sans qu’il soit possible de s’en rendre compte si cela se produit avant l’étape de chiffrement du vote. Il faut alors faire appel à d’autres techniques comme l’utilisation de hardware externe, afin de ne pas avoir à faire confiance à la machine et d’avoir des garanties fortes même si l’ordinateur est infecté. Vérifier formellement ce type de protocole est un vrai défi qui demande de combiner les techniques de vérification discutées ci-dessus.