Blockstream a franchi une nouvelle étape dans le développement de Bitcoin, en certifiant et en vérifiant une nouvelle fonctionnalité cryptographique pour Bitcoin : safegcd.
Dans un monde où la sécurité et l’efficacité sont essentielles au succès des crypto-monnaies, Blockstream, l’une des entreprises les plus innovantes en matière de technologie blockchain, a fait un pas de géant pour renforcer l’infrastructure Bitcoin. Rappelons que la sécurité du Bitcoin dépend en grande partie d’algorithmes de signature numérique comme l’ECDSA, qui garantissent l’authenticité et l’intégrité des transactions. Cependant, ces algorithmes sont confrontés au défi constant d’équilibrer vitesse et sécurité, en particulier lorsqu’il s’agit d’opérations mathématiques complexes telles que les inverses modulaires.
Blockstream a relevé ce défi avec le développement et la mise en œuvre d'un nouvel algorithme appelé «Safegcd«. Cet algorithme, qui allie rapidité et sécurité, a fait l'objet d'une vérification formelle rigoureuse pour garantir son exactitude. Le résultat est une avancée significative qui non seulement améliore les performances des opérations de signature et de vérification de Bitcoin, mais fournit également une forte garantie mathématique de son bon fonctionnement. Dans cet article, nous explorerons comment Blockstream a franchi cette étape et quelles implications cela a pour l’avenir de Bitcoin.
Un énorme défi pour la sécurité du Bitcoin
Et au cœur des algorithmes de signature numérique et de dérivation de clé se trouve une opération mathématique connue sous le nom de marche arrière modulaire. Cette opération est relativement coûteuse en ressources informatiques, ce qui en fait un goulot d'étranglement pour les performances du Bitcoin. Mais il est également vital pour sa sécurité, ce qui le rend particulièrement important lorsqu’il s’agit d’en assurer une bonne mise en œuvre.
Cela a conduit à deux méthodes principales pour calculer les inverses modulaires : l'utilisation d'une technique appelée « échelle d'exposants » (très lente) et l'algorithme GCD étendu d'Euclide (rapide mais difficile à rendre constant dans le temps). Actuellement, la bibliothèque libsecp256k1, créée et utilisée par Bitcoin Core, opte toujours pour l'échelle des exposants lorsqu'elle est configurée pour être utilisée dans Bitcoin Core. Bien que sécurisée, cette méthode est notoirement lente, ce qui limite les performances du portefeuille.
La solution de Blockstream : Safegcd
Pour résoudre ce problème, Blockstream a décidé de créer une implémentation GCD qui maintiendrait la sécurité de Bitcoin à ce stade, mais lui permettrait également d'améliorer les performances du réseau. C’est ainsi qu’en 2021, Blockstream a implémenté un nouvel algorithme modulaire inverse appelé « safegcd ». Cet algorithme, développé par Daniel J. Bernstein et Bo-Yin Yang, propose une alternative à la fois rapide et constante dans le temps. Safegcd fonctionne en itérant un calcul simple jusqu'à ce qu'une condition de terminaison soit atteinte. Pour garantir que l’algorithme est constant dans le temps, il peut être itéré un nombre fixe de fois, même si la condition de terminaison est atteinte prématurément.
La clé pour rendre safegcd constant dans le temps est de déterminer combien d'itérations sont nécessaires pour toutes les entrées possibles de 256 bits (la taille des entrées dans le cas de secp256k1). Initialement, on estimait que 741 itérations étaient nécessaires, mais Pieter Wuille, ingénieur chez Blockstream, a développé une méthode pour réduire ce nombre à 724 itérations. Plus tard, Wuille et Gregory Maxwell ont découvert une variante de l'algorithme qui ne nécessite que 590 itérations. Cette optimisation améliorerait les performances des signatures ECDSA de 25 % et la vérification des signatures de 15 % par rapport à l'échelle des exposants.
Vérification formelle : garantir l'exactitude
Mais malgré les améliorations de performances, la mise en œuvre d'un nouvel algorithme comme safegcd comporte des risques. S'il y a une erreur dans le calcul des itérations nécessaires, l'algorithme peut ne pas se terminer correctement, ce qui entraîne des valeurs incorrectes et finalement un échec de la vérification de la signature. Cela serait dévastateur pour la sécurité du Bitcoin.
Pour atténuer ce risque, Blockstream Research a effectué une vérification formelle de l'algorithme safegcd à l'aide de l'assistant de test Coq. Coq est un outil basé sur la théorie des types dépendants qui combine un système de déduction mathématique avec un langage de programmation fonctionnel. Cela permet de tester par réflexion, une méthode qui combine l'exécution d'un programme fonctionnel avec la déduction mathématique pour vérifier l'exactitude de l'algorithme.
La vérification formelle a consisté à implémenter l'algorithme de calcul de coque convexe en Coq et à prouver que ce calcul est correct. Le résultat est un théorème qui garantit que l’algorithme safegcd se termine en 590 itérations. Cette vérification a été réalisée en 2,5 jours sur du matériel grand public, démontrant la faisabilité de la technique.
Implémentation dans libseCP256k1
La mise en œuvre de safegcd dans libseCP256k1 était un effort de collaboration. Peter Dettman, le développeur qui a implémenté l'algorithme, a travaillé en étroite collaboration avec l'équipe Blockstream pour intégrer safegcd dans la bibliothèque. Le processus comprenait l'ajout de fonctions ctz (compter les zéros à droite) pour optimiser les opérations sur les bits, la mise en œuvre de l'algorithme safegcd dans des modules séparés, l'ajout de tests approfondis et la refactorisation du code pour préparer la transition vers safegcd.
De plus, des optimisations supplémentaires ont été apportées pour améliorer les performances sur les systèmes 32 et 64 bits. Ces optimisations sont cruciales car Bitcoin fonctionne souvent sur du matériel très faible, comme les appareils mobiles et les systèmes embarqués, où l'efficacité est vitale.
De cette manière, la mise en œuvre et la vérification formelle de l’algorithme safegcd par Blockstream représentent une étape importante dans la sécurité et l’efficacité du Bitcoin. Ce développement améliore non seulement les performances des opérations de signature et de vérification, mais apporte également des garanties mathématiques sur le bon fonctionnement de l'algorithme.
De plus, la vérification formelle de safegcd démontre qu'il est possible de vérifier dans la pratique des logiciels complexes et critiques, ce qui ouvre la porte à la vérification d'autres fonctions implémentées dans libsecp256k1, et pourrait conduire à une plus grande sécurité et fiabilité du réseau Bitcoin.
