Blockstream ha alcanzado un nuevo hito dentro del desarrollo de Bitcoin, certificando y verificando una nueva función criptográfica para Bitcoin: la safegcd.
En un mundo donde la seguridad y la eficiencia son cruciales para el éxito de las criptomonedas, Blockstream, una de las empresas más innovadoras en tecnología blockchain, ha dado un paso gigantesco para fortalecer la infraestructura de Bitcoin. Recordemos que la seguridad de Bitcoin depende en gran medida de algoritmos de firma digital como ECDSA, que garantizan la autenticidad y la integridad de las transacciones. Sin embargo, estos algoritmos enfrentan el desafío constante de equilibrar la velocidad y la seguridad, especialmente cuando se trata de operaciones matemáticas complejas como las inversas modulares.
Blockstream ha abordado este desafío con el desarrollo y la implementación de un nuevo algoritmo llamado «safegcd«. Este algoritmo, que combina velocidad y seguridad, ha sido sometido a una rigurosa verificación formal para garantizar su correctitud. El resultado es un avance significativo que no solo mejora el rendimiento de las operaciones de firma y verificación de Bitcoin, sino que también proporciona una sólida garantía matemática de su funcionamiento correcto. En este artículo, exploraremos cómo Blockstream ha logrado este hito y qué implicaciones tiene para el futuro de Bitcoin.
Un enorme desafío para la seguridad de Bitcoin
Y es que en el corazón de los algoritmos de firma digital y derivación de claves, se encuentra una operación matemática conocida como la inversa modular. Esta operación es relativamente costosa en términos de recursos computacionales, lo que la convierte en un cuello de botella para el rendimiento de Bitcoin. Pero también es vital para la seguridad del mismo, lo que le hace especialmente importante a la hora de tener una buena implementación de la misma.
Esto ha llevado a que existan dos métodos principales para calcular inversas modulares: el uso de una técnica llamada “ladder de exponentes” (muy lenta) y el algoritmo de GCD extendido de Euclides (rápido pero difícil de hacer constante en tiempo). Actualmente, la biblioteca libsecp256k1, creada y utilizada por Bitcoin Core, siempre opta por el ladder de exponentes cuando se configura para su uso en Bitcoin Core. Aunque es seguro, este método es notablemente lento, algo que limita el rendimiento del monedero.
La solución de Blockstream: Safegcd
Para resolver esto, Blockstream se propuso crear una implementación GCD que permitiera mantener la seguridad de Bitcoin en este punto, pero también le permitiera mejorar el rendimiento de la red. Fue así como en 2021, Blockstream implementó un nuevo algoritmo de inversa modular llamado «safegcd». Este algoritmo, desarrollado por Daniel J. Bernstein y Bo-Yin Yang, ofrece una alternativa que es tanto rápida como constante en tiempo. Safegcd funciona iterando un cálculo simple hasta que se alcanza una condición de terminación. Para garantizar que el algoritmo sea constante en tiempo, se puede iterar un número fijo de veces, incluso si la condición de terminación se alcanza antes.
La clave para hacer que safegcd sea constante en tiempo es determinar cuántas iteraciones son necesarias para todos los posibles inputs de 256 bits (el tamaño de los inputs en el caso de secp256k1). Inicialmente, se estimó que se necesitaban 741 iteraciones, pero Pieter Wuille, un ingeniero de Blockstream, desarrolló un método para reducir este número a 724 iteraciones. Posteriormente, Wuille y Gregory Maxwell descubrieron una variante del algoritmo que solo requiere 590 iteraciones. Esta optimización mejoraría el rendimiento de las firmas ECDSA en un 25% y la verificación de firmas en un 15% en comparación con el ladder de exponentes.
Verificación formal: garantizando la correctitud
Pero a pesar de las mejoras en rendimiento, implementar un algoritmo novel como safegcd conlleva riesgos. Si hay un error en el cálculo de las iteraciones necesarias, el algoritmo podría no terminar correctamente, lo que resultaría en valores incorrectos y, en última instancia, en fallos en la verificación de firmas. Esto sería devastador para la seguridad de Bitcoin.
Para mitigar este riesgo, Blockstream Research realizó una verificación formal del algoritmo safegcd utilizando el asistente de pruebas Coq. Coq es una herramienta basada en teoría de tipos dependientes que combina un sistema de deducción matemática con un lenguaje de programación funcional. Esto permite realizar pruebas por reflexión, un método que combina la ejecución de un programa funcional con la deducción matemática para verificar la corrección del algoritmo.
La verificación formal consistió en implementar el algoritmo de cálculo de convex hull en Coq y probar que este cálculo es correcto. El resultado es un teorema que garantiza que el algoritmo safegcd termina en 590 iteraciones. Esta verificación se realizó en 2,5 días en hardware de consumo, lo que demuestra la viabilidad de la técnica.
Implementación en libsecp256k1
La implementación de safegcd en libsecp256k1 fue un esfuerzo colaborativo. Peter Dettman, el desarrollador que implementó el algoritmo, trabajó en estrecha colaboración con el equipo de Blockstream para integrar safegcd en la biblioteca. El proceso incluyó la adición de funciones de ctz (count trailing zeros) para optimizar las operaciones de bit, la implementación del algoritmo safegcd en módulos separados, la adición de pruebas extensivas, y la refactorización del código para preparar la transición a safegcd.
Además, se realizaron optimizaciones adicionales para mejorar el rendimiento en sistemas de 32 y 64 bits. Estas optimizaciones son cruciales porque Bitcoin a menudo se ejecuta en hardware muy débil, como dispositivos móviles y sistemas embebidos, donde la eficiencia es vital.
De esta forma, la implementación y verificación formal del algoritmo safegcd por parte de Blockstream representan un hito significativo en la seguridad y eficiencia de Bitcoin. Este desarrollo no solo mejora el rendimiento de las operaciones de firma y verificación, sino que también proporciona garantías matemáticas de que el algoritmo funciona correctamente.
Además, la verificación formal de safegcd demuestra que es posible verificar software complejo y crítico en la práctica, lo que abre la puerta a la verificación de otras funciones implementadas en libsecp256k1, y podría llevar a una mayor seguridad y confiabilidad en la red Bitcoin.
