VePaSS, vers de nouveaux outils pour analyser les systèmes de sécurité probabilistes
Les outils disponibles pour analyser les protocoles de sécurité des infrastructures numériques ne prennent pas en compte tous les comportements probabilistes, vulnérables à des attaques, par exemple dans les systèmes de vote électronique ou d'authentification à distance. Les équipes de recherche du projet VePaSS ont reçu une bourse du Conseil européen de le recherche (ERC) Synergy. Avec une approche interdisciplinaire, elles ont pour ambition de créer de nouveaux outils pour vérifier la fiabilité des systèmes de sécurité probabilistes.
Que ce soit pour protéger les données personnelles, la confidentialité des communications ou les transactions commerciales, la sécurité est un enjeu majeur pour les systèmes numériques. Confrontés à des attaques de plus en plus complexes, ces systèmes doivent être capables d'assurer la sécurité de fonctions telles que l'authentification, la confidentialité, la transparence... Pour se prémunir contre les attaques, des protocoles de sécurité ont été mis en place. Des méthodes permettant de vérifier leur validité ont été développées et ont donné naissance à des outils d'analyse automatique des protocoles de sécurité. Toutefois, ces méthodes d'analyse ont une limite : la plupart ne prennent en compte qu'une partie des comportements probabilistes, notamment ceux pour générer de manière aléatoire des clés de chiffrement. Or, les protocoles de sécurité utilisent d'autres sources de comportement aléatoires, par exemple dans les systèmes d'ouverture de porte de voiture sans contact, lors de l'accès à un site web ou dans le vote électronique, lorsque l'authentification de l'utilisateur passe par l'échange d'un code court qui peut être capté ou deviné par un attaquant.
Le projet ERC Synergy VePaSS (Verification of probabilistic security systems) a pour objectif de combler ces lacunes. Il réunit quatre scientifiques1, Vincent Cheval, maître de conférences à l'Université d'Oxford et chargé de cours à Balliol College, Véronique Cortier, directrice de recherche CNRS au Laboratoire lorrain de recherche en informatique et ses applications (Loria - CNRS/Université de Lorraine), Mahsa Shirmohammadi, chargée de recherche CNRS à l'Institut de recherche en informatique fondamentale (IRIF - CNRS/Université Paris Cité) et Sébastien Tavenas, chargé de recherche CNRS au Laboratoire de mathématiques (LAMA - CNRS/Université de Savoie Mont Blanc), dont les expertises sont complémentaires. Ils ont l’ambition, en combinant leurs approches, de créer de nouveaux outils incluant les comportements probabilistes dans l’analyse des protocoles de sécurité. « Un premier objectif du projet est de formuler un modèle unifié qui prendra en compte les perspectives de la sécurité numérique et de la théorie des jeux, qui jusqu'ici étaient étudiées dans des communautés de recherche qui se parlaient peu », indique Véronique Cortier.
Un jeu stochastique peut être vu comme une partie de poker qui se déroule sur plusieurs manches, la distribution des cartes introduisant une composante probabiliste. Chaque joueur élabore une stratégie en vue de maximiser ses chances de gagner. Les récents progrès de la théorie des jeux stochastiques rendent désormais possible l’analyse de la complexité de stratégies déployées. D’après Mahsa Shirmohammadi, « ces méthodes d'analyse, transposées dans le domaine de la sécurité numérique, permettront d’identifier les attaques possibles et de déterminer les paramètres optimaux pour la conception de nouveaux protocoles de sécurité ».
Une autre grande question abordée par VePaSS concerne la complexité des calculs, par exemple le calcul de la probabilité qu’un attaquant réussisse, qui implique la manipulation de grands systèmes d’équations polynomiales. C’est là que la recherche sur le calcul symbolique et la complexité algébrique joue un rôle essentiel, faisant progresser à la fois la théorie des jeux stochastiques et la vérification des systèmes de sécurité probabilistes.
Les nouveaux modèles et algorithmes issus du projet seront évalués sur des exemples réels de sécurité numérique, en particulier sur les cas complexes du vote électronique et de l'authentification à distance. « Ces tests, utilisés de manière itérative, permettront aussi de soulever de nouvelles questions théoriques », précise Sébastien Tavenas.
Ces développements, au-delà de leurs applications directes à la sécurité de systèmes probabilistes, feront aussi progresser la recherche fondamentale en théorie des jeux et en calcul symbolique. Enfin, les résultats de VePaSS permettront d'enrichir les outils utilisés actuellement pour analyser des protocoles cryptographiques, afin de permettre l’analyse de protocoles de sécurité probabilistes.
En savoir plus
Les partenaires du projet ERC VePaSS :
- Vincent Cheval, associate professor à l'Université d'Oxford et chargé de cours à Balliol College, s’intéresse particulièrement au développement d’outils de vérification automatique, corrects, efficaces et permettant de traiter de nombreux protocoles.
- Véronique Cortier, directrice de recherche CNRS au Loria, se consacre à la mise au point des techniques pour analyser les protocoles de sécurité, en particulier les protocoles de vote électronique.
- Mahsa Shirmohammadi, chargée de recherche CNRS à l'IRIF, mène des recherches axées sur la vérification de systèmes probabilistes et les jeux stochastiques.
- Sébastien Tavenas, chargé de recherche CNRS au LAMA, travaille sur la complexité algorithmique des problèmes algébriques. Ses travaux visent à caractériser le temps et l’espace nécessaire à un ordinateur pour trouver des solutions à des questions algébriques.