Vérification formelle de la sûreté des protocoles de stablecoins

Les stablecoins constituent aujourd'hui une interface majeure entre les monnaies traditionnelles et les systèmes blockchain. En maintenant une parité avec une monnaie de référence, principalement le dollar et, dans une moindre mesure, l'euro, ils permettent de représenter et de transférer sur blockchain une valeur exprimée dans une monnaie traditionnelle. Leur capitalisation mondiale se chiffre désormais en centaines de milliards de dollars et leur importance croissante s'accompagne de nouveaux enjeux de sécurité, comme l'illustrent les nombreux incidents recensés dans la littérature récente [1]. 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. École doctorale : Sciences et Technologies de l'Information et de la Communication Direction : Sylvain CONCHON Financement : Financement d'un fond ou d'une agence de développement (BPI-FUI (Fond Unique Interminstériel), Agences départementales...)