Doctorant en Vérification de protocoles avec opérateurs AC à l'aide de PROVERIF (H/F)

Sujet de thèse

La vérification formelle repose sur des techniques de raisonnement mathématique pour établir des propriétés de systèmes distribués complexes. Dans les cadres de vérification symbolique, les comportements du système et les manipulations de données sont représentés sous forme de termes algébriques et analysés à l’aide de procédures de déduction automatisées. Une difficulté centrale dans ce contexte réside dans le traitement des structures algébriques satisfaisant des propriétés équationnelles non triviales, en particulier l’associativité et la commutativité. La prise en charge de telles théories augmente considérablement la complexité des procédures de raisonnement automatisé et soulève des questions fondamentales concernant la correction, la complétude et la terminaison. ProVerif est un outil de raisonnement automatisé largement utilisé, basé sur une traduction des problèmes de vérification en clauses de Horn, ainsi que sur une procédure de résolution dont la correction est prouvée. Bien que la correction soit garantie, la terminaison n’est pas assurée en général, bien qu’elle soit souvent observée en pratique. Plusieurs extensions ont été étudiées afin d’intégrer les théories associatives-commutatives (AC) dans ce cadre, y compris les théories liées au XOR, aux groupes abéliens et à l’exponentiation de Diffie‑Hellman, principalement par le biais de techniques de prétraitement. Cependant, ces approches présentent des limites importantes et n’ont pas été intégrées dans l’outil principal. Récemment, nous avons étendu ProVerif pour prendre en charge le XOR dans l’analyse des propriétés d’accessibilité. En nous appuyant sur ce travail, l’objectif de ce projet de thèse est de développer de nouvelles techniques de résolution capables de gérer des classes plus riches de théories équationnelles associatives-commutatives dans le même cadre de raisonnement automatisé.

Objectifs du projet de thèse

Le premier objectif du projet de thèse sera d’acquérir une compréhension approfondie du moteur de résolution de ProVerif et de ses fondements théoriques.

L’objectif scientifique principal consistera ensuite à étendre cette procédure de résolution pour prendre en charge des théories équationnelles associatives-commutatives supplémentaires, telles que les groupes abéliens (AG), l’exponentiation de Diffie‑Hellman ou les appariements bilinéaires. L’accent sera d’abord mis sur les propriétés d’accessibilité.

• Concevoir une nouvelle procédure de résolution en adaptant le cadre existant pour prendre en charge des théories associatives-commutatives plus riches.
• Établir les propriétés de correction et, dans la mesure du possible, de complétude de la procédure proposée.
• Implémenter la nouvelle procédure dans le code source de ProVerif et évaluer son comportement pratique, en prêtant une attention particulière aux performances.

Conditions particulières d'exercice

Le Centre national de la recherche scientifique est l’une des plus importantes institutions publiques au monde, avec 34 000 femmes et hommes, plus de 1 000 laboratoires et 200 métiers, en partenariat avec les universités et les grandes écoles. Depuis plus de 80 ans, des recherches pluridisciplinaires sont développées sur tout le territoire national, en Europe et à l’international. Le lien étroit que le CNRS tisse entre ses missions de recherche et le transfert vers la société fait de lui un acteur clé de l’innovation en France et dans le monde. Le partenariat qui le lie avec les entreprises est le socle de sa politique de valorisation, et les start‑ups issues de ses laboratoires témoignent du potentiel économique de ses travaux de recherche.

Le Centre national de la recherche scientifique est un organisme public de recherche pluridisciplinaire placé sous la tutelle du ministère de l’Enseignement supérieur et de la Recherche. Créé en 1939 et dirigé par des scientifiques, il a pour mission de faire progresser la connaissance et d’être utile à la société dans le respect des règles d’éthique, de déontologie et d’intégrité scientifique.