-
El programa admite secuencias de comando Elements.
-
B’SST utiliza el Z3, un probador de teoremas de lógica de primer orden.
Un nuevo programa permite realizar análisis del código fuente de Bitcoin. El desarrollador Dmitriy Petukhov divulgó, a través de la lista de correos de desarrolladores, el repositorio de Bitcoin Script Symbolic Tracer (B’SST), una herramienta capaz de ejecutar códigos de operaciones y detectar potenciales errores.
B’SST es capaz de analizar los scripts de Bitcoin “ejecutando simbólicamente todas las rutas de ejecución posibles y rastreando las restricciones que los códigos de operación imponen a los valores en los que operan”, indica Petukhov. Luego, el programa genera un informe basado en este análisis.
El programa utiliza la biblioteca de código abierto Elements, diseñada por Google para el lenguaje de programación Python. También utiliza el probador de teoremas de primer orden Z3, diseñado por Microsoft Research, uno de los componentes más poderosos para detectar problemas de los scripts (o conjunto de instrucciones escritas en lenguaje de programación). Según el repositorio de B’SST, esta función permite un análisis minucioso. Sin embargo, se puede ejecutar el programa sin Z3 para ciertos análisis “donde la velocidad de verificación es más importante que la minuciosidad”.
Este programa debe usarse como una capa adicional de defensa en la lucha por detectar defectos y comportamientos inesperados en los scripts, al igual que otras cosas como pruebas o auditorías de código se usan para este propósito, simplemente reduciendo la probabilidad de que los defectos no se detecten. También se puede utilizar como herramienta para comprender mejor el comportamiento de los scripts analizados.
Dmitry Petukhov, repositorio de Bitcoin Script Symbolic Tracer.
Para ejecutar este programa se necesita Python 3.10 o posterior. Además, requiere el uso de la biblioteca secp256k1, diseñada específicamente para Bitcoin, para verificar la validez de las llaves públicas. Este último es un requerimiento opcional, al igual que el uso del probador Z3.
En cuanto a su licencia de uso, B’SST es de código abierto: se registró como Prosperity Public License 3.0.0., que es gratis para uso no comercial. Esta licencia otorga 30 días gratis si el programa se utiliza con fines comerciales. Las instituciones educativas y de investigación están exentas.
B’SST también contiene partes del código de Bitcoin: el código de la clase CSHA256 de licencia MIT, escrito por varios desarrolladores de Bitcoin Core y la función ripmd160, también de licencia MIT, escrito por el desarrollador Pieter Wuille.
Entre las funciones de B’SST se encuentra la capacidad de informar sobre fallos de secuencias de comando detectados, con el código que pudo haber causado el error; detectar rutas válidas para la ejecución de los scripts; hacer una lista de restricciones que deben cumplirse para completar exitosamente un script; y analiza posibles valores para distintas variables: por ejemplo, testigos, resultados del script o campos de transacción.
Sin embargo, como advierte Pethukov, el programa “no puede garantizar que no haya problemas, inconsistencias, errores, vulnerabilidades, etc. en el script analizado”. En este sentido, sugerimos leer cuidadosamente la descripción del proyecto en GitHub, que contempla una serie más detallada de factores que pueden derivar en un análisis exitoso y las posibles limitaciones del programa.
Petukhov indica que este tipo de desarrollos no había sido objeto de trabajo de los programadores de Bitcoin en mucho tiempo: “Solo conozco un proyecto que tuvo como objetivo realizar este tipo de análisis anteriormente: el ‘SCRIPT Analyser’, pero no tuvo actualizaciones en su repositorio de GitHub durante 5 años”.
La detección de errores es una parte vital del proceso de mejora de Bitcoin. A través de los años se han encontrado y corregido numerosos errores. Por ejemplo, en 2018, los desarrolladores de Bitcoin Core corrigieron una vulnerabilidad que pudo haber afectado la política monetaria de bitcoin, como reportó CriptoNoticias.
