Faits marquants:
Le programme prend en charge les scripts Elements.
B’SST utilise le Z3, un prouveur de théorème logique du premier ordre.
Un nouveau programme permet d’analyser le code source du Bitcoin. Le développeur Dmitriy Petukhov a divulgué, via la liste de diffusion des développeurs, le référentiel Bitcoin Script Symbolic Tracer (B’SST), un outil capable d’exécuter des codes de trading et de détecter des erreurs potentielles.
B’SST est capable d’analyser les scripts Bitcoin « en exécutant symboliquement tous les chemins d’exécution possibles et en suivant les restrictions que les opcodes imposent sur les valeurs sur lesquelles ils opèrent », explique Petukhov. Le programme génère ensuite un rapport basé sur cette analyse.
Le programme utilise la bibliothèque open source Elements, conçue par Google pour le langage de programmation Python. Il utilise également le prouveur de théorème du premier ordre Z3, conçu par Microsoft Research, l’un des composants les plus puissants pour détecter les problèmes de script (ou ensemble d’instructions écrites en langage de programmation). Selon le référentiel B’SST, cette fonctionnalité permet une analyse approfondie. Cependant, vous pouvez exécuter le programme sans Z3 pour certaines analyses « où la rapidité de vérification est plus importante que la rigueur ».
Ce programme doit être utilisé comme couche de défense supplémentaire dans la lutte pour détecter les défauts et les comportements inattendus dans les scripts, tout comme d’autres éléments tels que les tests ou les audits de code sont utilisés à cette fin, réduisant simplement la probabilité que les défauts ne soient pas détectés. détecter. Il peut également être utilisé comme outil pour mieux comprendre le comportement des scripts analysés.
Dmitry Petukhov, référentiel Bitcoin Script Symbolic Tracer.
Pour exécuter ce programme Python 3.10 ou version ultérieure est requis. De plus, cela nécessite l’utilisation de la bibliothèque secp256k1, conçue spécifiquement pour Bitcoin, pour vérifier la validité des clés publiques. Cette dernière est une exigence facultative, tout comme l’utilisation du testeur Z3.
Concernant sa licence d’utilisation, B’SST est open source : il a été enregistré sous le nom de Prosperity Public License 3.0.0., qui est gratuit pour une utilisation non commerciale. Cette licence accorde 30 jours gratuits si le programme est utilisé à des fins commerciales. Les établissements d’enseignement et de recherche sont exonérés.
B’SST contient également des parties du code Bitcoin : le code de classe CSHA256 sous licence MIT, écrit par plusieurs développeurs Bitcoin Core, et la fonction ripmd160, également sous licence MIT, écrite par le développeur Pieter Wuille.
Parmi les fonctions de B’SST se trouve la possibilité de signaler les échecs de script détectés, avec le code qui a pu provoquer l’erreur ; détecter les chemins valides pour l’exécution du script ; dresser une liste des contraintes à respecter pour mener à bien un script ; et analyse les valeurs possibles pour différentes variables : par exemple, les jetons, les résultats de script ou les champs de transaction.
Cependant, comme le prévient Pethukov, le programme « ne peut garantir qu’il n’y a pas de problèmes, d’incohérences, d’erreurs, de vulnérabilités, etc. dans le script analysé ». En ce sens, nous vous suggérons de lire attentivement la description du projet sur GitHub, qui envisage une série plus détaillée de facteurs pouvant conduire à une analyse réussie et aux éventuelles limites du programme.
Petukhov indique que ces types de développements n’avaient pas fait l’objet de travaux de la part des programmeurs Bitcoin depuis longtemps : « Je ne connais qu’un seul projet qui visait auparavant à réaliser ce type d’analyse : le ‘SCRIPT Analyzer’, mais il n’a pas eu de mises à jour. à son référentiel GitHub pendant 5 ans.
La détection des bogues est un élément essentiel du processus d’amélioration du Bitcoin. De nombreux bugs ont été trouvés et corrigés au fil des années. Par exemple, en 2018, les développeurs de Bitcoin Core ont corrigé une vulnérabilité qui aurait pu affecter la politique monétaire de Bitcoin, comme l’a rapporté CriptoNoticias.