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.

Abstract

In the ever-evolving landscape of blockchain technology, the emergence of decentralized applications (DApps) has revolutionized how we envision trust, operations, and services in a digital world. The surge in DApp deployment and transaction volume has brought the issue of scalability and privacy to the fore. Ethereum, the leading platform for DApps, has faced challenges in scaling while maintaining decentralization and security. Solutions such as zk-Rollups have been proposed to alleviate these constraints by bundling or rolling up transactions into a single proof. There are also numerous applications of Zero knowledge in protocols providing privacy-preserving transactions on blockchain like Zcash. The security of these technologies hinges on the reliability of the underlying zero-knowledge-proof systems. Given these systems’ complexity and critical nature, formal verification methods are paramount to ensure that the proof systems are correctly implemented and that the circuits within are robust against vulnerabilities. In addition, at the core of this paradigm shift is the need for robust security mechanisms that govern access control and maintain the security of smart contracts. In this context, this research aims to contribute substantially to the blockchain security field. This dissertation ventures into two groundbreaking research domains: the formal verification and abstract interpretation of zero-knowledge proof systems, with a focus on Halo2 circuits, which are one of the most popular implementations of Plonk, and Blockchain-Based Access Control as a Service. The first segment pioneers the formal verification of Halo2 circuits, critical for privacy-preserving protocols and zk-Rollups, using SMT solvers to detect under-constrained circuits and introducing a novel, lightweight formal method for analyzing PLONK-based arithmetization. Significantly, this research produced the first-ever tool for analyzing Halo2 circuits, initially creating a dynamic analyzer that models Halo2’s constraint system for verification with SMT solver, and subsequently refining the design to a fully static version that optimizes SMT solver efficiency. In addition, we propose an improvement for the abstract interpretation of halo2 circuits for detecting unused elements within a circuit which can cause several security issues like under-constrained vulnerability. The second segment introduces an innovative platform that simplifies access control in smart contracts through a Role-Centric Access Control model, blending the simplicity of RBAC with the flexibility of ABAC. This model enhances function-level access control and enables dynamic updates of attribute-based policies, thereby allowing developers to concentrate on core functionalities viii without sacrificing security. This dual-focus exploration not only advances the theoretical framework for blockchain security and zero-knowledge proofs but also delivers practical tools and methodologies for enhancing the reliability and performance of these cutting-edge technologies. Through these two avenues, this research contributes to the critical discussion and development of blockchain security, addressing the pivotal role of zero-knowledge-proof systems in Ethereum’s scalability and the pressing issue of smart contract access control.