Le livre blanc de Bitcoin a été publié le 31 octobre 2008, par Satoshi Nakamoto sur le site P2P foundation, présentant le livre blanc de Bitcoin (Bitcoin : un système de monnaie électronique pair-à-pair), célébrant aujourd'hui son 16e anniversaire.
Le prix initial du Bitcoin était de 0,0008 dollars, et aujourd'hui, il a augmenté de plus de 90 millions de fois.
Il est bien connu que Bitcoin a redéfini la façon dont les gens font confiance au transfert de valeur. Dans un réseau décentralisé, la confiance est remplacée par la technologie, chaque transaction étant vérifiée par le réseau lui-même. Cependant, avec la montée de la finance décentralisée (DeFi) et des contrats intelligents, comment introduire en toute sécurité des calculs plus complexes dans le réseau Bitcoin et construire un contenu plus riche est devenu un nouveau défi.
Qu'est-ce que BitVM ?
En décembre 2023, le responsable du projet ZeroSync, Robin Linus, a publié un livre blanc intitulé (BitVM : Compute Anything On Bitcoin), suscitant des réflexions sur l'amélioration de la programmabilité de Bitcoin.
L'émergence de BitVM a donné à Bitcoin la capacité d'exécuter des calculs complexes hors chaîne, tout en vérifiant les résultats sur chaîne, élargissant considérablement ses fonctionnalités. Plus simplement, BitVM est une solution qui permet d'exécuter des calculs complexes et des contrats intelligents sur le réseau Bitcoin. C'est une solution qui peut réaliser la complétude de Turing sans changer le consensus du réseau Bitcoin. En devenant Turing-complet, la blockchain Bitcoin pourrait théoriquement être utilisée pour étendre les fonctionnalités de Bitcoin, bien au-delà de la vision initiale du « système de monnaie électronique pair-à-pair » proposée dans le livre blanc de Bitcoin. Elle permet aux utilisateurs de créer des applications au-dessus de Bitcoin - semblables aux fonctionnalités déjà mises en œuvre sur d'autres plateformes comme Ethereum, tout en maintenant la sécurité et la décentralisation bien connues de Bitcoin.
En résumé, BitVM permet à l'écosystème Bitcoin non seulement de répondre aux besoins de transaction, mais aussi de créer des DApps plus complexes au niveau BTC. En même temps, cela conserve la sécurité et les caractéristiques de décentralisation de Bitcoin.
Cependant, la complexité s'accompagne souvent de risques, et garantir la sécurité de ces calculs complexes est devenu un problème urgent à résoudre.
Actuellement, de nombreuses équipes se consacrent à la recherche et au développement de BitVM, notamment : ZeroSync, fondé par le créateur de BitVM Robin, le projet natif du Bitcoin Nubit fondé par le Prof. Yu Feng de l'Université de Californie à Santa Barbara, Alpen Labs, qui se consacre à l'extension ZK de Bitcoin, Chainway Labs, qui se concentre sur les Rollups ZK de Bitcoin, Citrea, et Fiamma, ainsi que la Layer 1 Foundation où se trouve le créateur de BRC20, Domo.
Actuellement, Nubit, en collaboration avec ZeroSync, Alpen Labs, Chainway Labs et la Layer 1 Foundation dirigée par Domo, a publié le 31 octobre un article (Vérification par bouton-poussoir pour les mises en œuvre de BitVM), complétant et lançant l'outil de vérification formelle de BitVM. Dans cet article, Nubit, par le biais de la vérification formelle, fournit une preuve mathématique automatisée pour garantir davantage la sécurité des applications BitVM, permettant aux développeurs et aux utilisateurs de construire et d'utiliser des applications en toute confiance.
Qu'est-ce que la vérification formelle ? Comment aide-t-elle à garantir la sécurité de BitVM ?
Dans l'article de Robin, BitVM introduit un système qui permet à n'importe quel calcul d'être vérifié sur la blockchain de Bitcoin, sans compromettre sa sécurité ou modifier le réseau. Cependant, le développement du système et la construction d'applications basées sur celui-ci nécessitent souvent une révision du code par des experts. Dans un écosystème comme Bitcoin, où la sécurité est primordiale, la révision manuelle est à la fois chronophage et sujette à erreurs. La vérification formelle, par des calculs mathématiques purs, peut automatiquement valider si la logique du programme correspond aux attentes, fournissant ainsi une garantie de sécurité pour l'ensemble du système BitVM.
Imaginez que vous déployez un contrat intelligent impliquant plusieurs transactions sur Bitcoin. Pour s'assurer que le contrat s'exécute correctement dans toutes les situations, les méthodes traditionnelles pourraient nécessiter de tester chaque possibilité de manière répétée. Mais avec l'outil de vérification formelle, la preuve mathématique vérifiera automatiquement la validité du contrat, augmentant considérablement les propriétés de sécurité du système.
Les défis particuliers de BitVM : complexité des contrats intelligents et limites du script Bitcoin
Contrairement aux blockchains comme Ethereum qui possèdent la complétude de Turing, le langage de script Bitcoin est limité par des considérations de sécurité et ne peut pas exécuter directement des calculs complexes. BitVM réalise les fonctionnalités de base des contrats intelligents Bitcoin par un modèle d'exécution hors chaîne et de vérification sur chaîne. En d'autres termes, tous les calculs complexes sont effectués hors chaîne, seul le résultat est vérifié sur chaîne, allégeant considérablement la charge de la chaîne Bitcoin. Cependant, cette innovation a apporté des difficultés significatives à sa mise en œuvre.
Tout d'abord, la conception de BitVM comprend de nombreuses opérations sur la pile et des calculs sur les registres, qui doivent être réalisés et vérifiés efficacement dans le script non Turing-complet de Bitcoin. Par exemple, pour s'assurer que les valeurs sont correctement jugées positives ou négatives lors de l'exécution du contrat, une fonction courante est is_positive, qui vérifie le bit le plus significatif pour déterminer le signe. Cependant, dans une version antérieure, la fonction is_positive a erronément jugé 0 comme un nombre positif en raison d'un biais de calcul, cette petite erreur pourrait entraîner de graves écarts dans l'exécution des contrats, voire provoquer des pertes économiques potentielles.
Source de l'image : (Vérification par bouton-poussoir pour les mises en œuvre de BitVM)
Grâce à la vérification formelle, l'outil de Nubit peut automatiquement vérifier des logiques de calcul similaires avant le déploiement du code, garantissant que tous les chemins d'exécution correspondent aux attentes. Ici, l'équipe Nubit a conçu un DSL (langage spécifique au domaine) basé sur les registres, transformant les opérations complexes sur la pile du script Bitcoin en opérations sur les registres plus faciles à vérifier, simplifiant ainsi le processus de développement et de vérification. De plus, pour des calculs répétitifs, ce DSL introduit des « invariants de boucle » pour réduire efficacement les calculs redondants dans le code et diminuer la difficulté de vérification.
Source de l'image : (Vérification par bouton-poussoir pour les mises en œuvre de BitVM)
Efficacité de la vérification : efficacité de la vérification formelle automatisée
D'après l'article, l'outil de vérification formelle de Nubit a été largement testé sur 98 benchmarks de vérificateurs SNARK de BitVM, avec un taux de réussite de vérification allant jusqu'à 94%, et la plupart des tâches de vérification peuvent être complétées en quelques secondes. Par rapport à la révision manuelle traditionnelle, cet outil non seulement accélère le processus de vérification, mais évite également la possibilité d'erreurs humaines, garantissant ainsi une exécution fiable des contrats intelligents BitVM sur Bitcoin.
Ce résultat prouve que la vérification formelle possède une valeur pratique extrêmement élevée dans les applications complexes de Bitcoin, en particulier dans les applications BTCFi qui exigent une sécurité maximale, elle peut réduire efficacement les risques.
BitVM et l'écosystème Bitcoin : étendre le potentiel des contrats intelligents Bitcoin
Grâce à la vérification formelle, la sécurité de BitVM a été considérablement améliorée, aidant les développeurs à construire des contrats et des applications plus complexes sur Bitcoin, tout en permettant aux utilisateurs de bénéficier de la haute sécurité de l'écosystème Bitcoin dans la finance décentralisée et les applications inter-chaînes. En tant qu'outil d'innovation pour l'écosystème Bitcoin, BitVM jette les bases de l'expansion de Bitcoin dans des applications complexes.
Bitcoin n'a jamais été conçu comme une plateforme de calcul complexe, mais s'est concentré sur la fiabilité du stockage et du transfert de valeur. Cependant, avec le lancement de BitVM, l'écosystème Bitcoin avance vers des contrats intelligents et des applications DeFi. Pour le développement d'applications décentralisées, la réalisation de la vérification formelle de BitVM n'est pas seulement une avancée technique, mais représente également une étape importante pour Bitcoin dans la finance décentralisée et les contrats intelligents.
BitVM ouvre l'écosystème futur de Bitcoin
Dans le processus de développement de BitVM, Nubit a travaillé en étroite collaboration avec des équipes telles que ZeroSync, Alpen Labs, Chainway Labs et Layer 1 Foundation, et sa vérification formelle de BitVM a introduit de nouvelles normes de sécurité et techniques dans l'écosystème Bitcoin. De plus, Nubit continuera à promouvoir le développement de calculs natifs Bitcoin sécurisés et vérifiables avec le soutien de Starkware et Fractal Bitcoin.
Tout commence difficilement, l'écosystème Bitcoin apporté par BitVM est encore en gestation, mais la collaboration et l'innovation profondes entre les projets précoces fourniront non seulement une garantie solide pour la sécurité des calculs complexes, mais ouvriront également des possibilités infinies pour l'avenir de Bitcoin. Une nouvelle ère de Bitcoin, où chacun peut faire confiance et participer, est en train d'émerger.
Cet article provient d'une soumission et ne représente pas l'avis de BlockBeats
