Securing Ethereum's Ecosystem: Formal Verification and Abstract Interpretation of Halo2 Circuits and Innovative Access Control of Smart Contracts

Dans le paysage en constante évolution de la technologie blockchain, l’émergence des applications décentralisées (DApps) a révolutionné notre vision de la confiance, des opérations et des services dans un monde numérique. L’augmentation du déploiement des DApps et du volume des transactions a mis en lumière le problème de l’scalabilité. Ethereum, la plateforme principale pour les DApps, a rencontré des défis pour évoluer tout en maintenant la décentralisation et la sécurité. Des solutions telles que les zk-Rollups ont été proposées pour atténuer ces contraintes en regroupant ou en roulant plusieurs transactions en une seule preuve. Il existe également de nombreuses applications de la preuve à divulgation nulle de connaissance (Zero Knowledge) dans les protocoles offrant des transactions préservant la vie privée sur la blockchain comme Zcash. La sécurité de ces technologies repose sur la fiabilité des systèmes de preuve à connaissance zéro sous-jacents. Étant donné la complexité et la nature critique de ces systèmes, les méthodes de vérification formelle sont primordiales pour garantir que les systèmes de preuve sont correctement implémentés et que les circuits internes sont robustes face aux vulnérabilités. En outre, coeur de ce changement de paradigme se trouve le besoin de mécanismes de sécurité robustes régissant le contrôle d’accès et maintenant la sécurité des contrats intelligents. Dans ce contexte, cette recherche vise à contribuer de manière substantielle au domaine de la sécurité de la blockchain. Cette dissertation se lance dans deux domaines de recherche révolutionnaires : la vérification formelle et interprétation abstraite des systèmes de preuve à connaissance zéro, avec un focus sur les circuits Halo2 et le Contrôle d’Accès Basé sur Blockchain en tant que Service. Le premier segment est pionnier dans la vérification formelle des circuits Halo2, essentiels pour les protocoles préservant la vie privée et les zk-Rollups, utilisant des solveurs SMT pour détecter les circuits sous-contraints et introduisant une nouvelle méthode formelle légère pour analyser l’arithmétisation basée sur PLONK. Significativement, cette recherche a produit le premier outil jamais créé pour analyser les circuits Halo2, en créant initialement un analyseur dynamique qui modélise le système de contraintes de Halo2 pour une vérification avec SMT solver, et par la suite en affinant la conception vers une version entièrement statique qui optimise l’efficacité du solveur SMT. Cette exploration non seulement avance le cadre théorique pour la sécurité de la blockchain et les preuves à connaissance zéro mais fournit également des outils pratiques et des méthodologies pour améliorer la fiabilité et la performance de ces techvi nologies de pointe. De plus, nous proposons une amélioration de l’interprétation abstraite des circuits halo2 pour détecter les éléments inutilisés dans un circuit qui peuvent causer plusieurs problèmes de sécurité comme une vulnérabilité sous-contrainte. Le second segment introduit une plateforme innovante simplifiant le contrôle d’accès dans les contrats intelligents à travers un modèle de Contrôle d’Accès Centré sur les Rôles, combinant la simplicité du Contrôle d’Accès Basé sur les Rôles (CABR) avec la flexibilité du Contrôle d’Accès Basé sur les Attributs (CABA). Ce modèle améliore le contrôle d’accès au niveau des fonctions et permet des mises à jour dynamiques des politiques basées sur les attributs, permettant ainsi aux développeurs de se concentrer sur les fonctionnalités essentielles sans sacrifier la sécurité. Par ces deux voies, cette recherche contribue à la discussion critique et au développement de la sécurité de la blockchain, en abordant le rôle central des systèmes sans connaissance dans l’évolutivité d’Ethereum et la question urgente du contrôle d’accès aux contrats intelligents.