Thèse Vérification Formelle de la Sûreté des Protocoles de Stablecoins H/F Doctorat.Gouv.Fr

Les protocoles de stablecoins mettent en jeu de nombreux acteurs, rôles et opérations : émission et destruction de tokens (mint/burn), demandes de rachat (redeem), délégation et révocation de privilèges, gel ou suspension d'opérations, évolution des contrats et transferts entre blockchains. Des incidents récents ont notamment montré que la compromission de mécanismes d'autorisation pouvait conduire à la création non autorisée de millions de stablecoins [1].

Cette thèse propose d'étudier la sûreté de ces protocoles par model checking symbolique de systèmes paramétrés, en s'appuyant en particulier sur Cubicle [2,3]. Les mécanismes étudiés pourront concerner la gestion des rôles et des autorisations, les workflows d'émission et de rachat, ainsi que les protocoles cross-chain, pour lesquels la cohérence des opérations doit être préservée malgré la concurrence, le retard, le réordonnancement ou le rejeu de messages.

Une attention particulière pourra également être portée à la traçabilité des stablecoins. Des techniques d'analyse de graphes, de clustering ou d'apprentissage automatique pourront être utilisées pour identifier les différentes adresses contrôlées par un même acteur ou reconstruire des flux, y compris entre plusieurs blockchains [7]. Il s'agira notamment d'étudier comment les informations ainsi obtenues peuvent être combinées avec les méthodes de vérification formelle.

La vérification formelle des smart contracts a déjà fait l'objet de nombreux travaux [4,5], et Cubicle a notamment été utilisé pour vérifier des smart contracts comportant un nombre non borné d'utilisateurs [3]. Certains protocoles de stablecoins, tels que Djed, ont également fait l'objet de vérifications formelles [6]. Le positionnement de cette thèse est d'étudier plus spécifiquement ces protocoles sous l'angle du model checking symbolique et paramétré.

Une question scientifique centrale sera de déterminer quelles composantes de protocoles réels de stablecoins peuvent être paramétrées et quelles abstractions permettent leur vérification automatique. Les difficultés rencontrées pourront conduire à de nouvelles abstractions ainsi qu'à des extensions du langage ou des algorithmes de Cubicle. L'objectif est ainsi de vérifier des protocoles réels tout en développant de nouvelles techniques de model checking symbolique et paramétré.

Références
[1] S. Ling et al. SoK: Stablecoin Designs, Risks, and the Stablecoin LEGO, 2025.
[2] S. Conchon et al. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems. CAV, 2012.
[3] S. Conchon, A. Korneva, F. Zaïdi. Verifying Smart Contracts with Cubicle. FMBC, 2019.
[4] P. Tsankov et al. Securify: Practical Security Analysis of Smart Contracts. CCS, 2018.
[5] A. Permenev et al. VerX: Safety Verification of Smart Contracts. IEEE S&P, 2020.
[6] J. Zahnentferner et al. Djed: A Formally Verified Crypto-Backed Autonomous Stablecoin Protocol. ICBC, 2023.
[7] H. Wu et al. CLTracer: A Cross-Ledger Tracing Framework Based on Address Relationships. Computers & Security, 2022. Les stablecoins occupent une place croissante dans les écosystèmes blockchain et soulèvent d'importantes questions de sûreté concernant notamment les mécanismes d'émission et de rachat, la gestion des autorisations et les opérations cross-chain. Plusieurs incidents récents illustrent les conséquences possibles de défaillances de ces mécanismes. Si la vérification formelle des smart contracts a fait l'objet de nombreux travaux, la vérification de protocoles de stablecoins reste encore relativement peu explorée, en particulier sous l'angle des systèmes paramétrés. La thèse s'inscrit dans la continuité des travaux sur Cubicle et son utilisation pour la vérification de smart contracts comportant un nombre non borné d'utilisateurs. Elle s'appuiera également sur les travaux récents concernant la sécurité des stablecoins et pourra établir des liens avec les recherches sur la traçabilité des transactions blockchain, notamment par analyse de graphes, clustering et apprentissage automatique. L'objectif de la thèse est de développer et d'appliquer des techniques de vérification formelle pour l'analyse de la sûreté des protocoles de stablecoins, en s'appuyant notamment sur le model checking symbolique et paramétré et sur Cubicle. Il s'agira d'identifier les propriétés pertinentes, les abstractions et les formes de paramétrisation permettant leur vérification automatique. Une attention particulière pourra également être portée à la combinaison de ces approches avec des techniques d'analyse de graphes, de clustering ou d'apprentissage automatique pour les questions de traçabilité. Les travaux pourront conduire à de nouvelles méthodes et à des extensions de Cubicle. Les protocoles de stablecoins étudiés seront modélisés sous forme de systèmes de transitions paramétrés, afin de permettre la vérification de propriétés indépendamment du nombre d'acteurs ou d'opérations considérés. La vérification reposera principalement sur des techniques de model checking symbolique, en particulier celles mises en oeuvre dans Cubicle. L'étude de protocoles réels permettra d'identifier les abstractions nécessaires et pourra conduire à des extensions du langage ou des algorithmes de Cubicle. Pour les questions de traçabilité, ces méthodes pourront être combinées à des techniques d'analyse de graphes, de clustering et d'apprentissage automatique appliquées aux données de transactions blockchain.