La seguridad de Bitcoin y otras cadenas de bloques, como Liquid, depende del uso de algoritmos de firmas digitales tales como ECDSA y firmas Schnorr. Una biblioteca en C llamada libsecp256k1, nombrada así por la curva elíptica sobre la cual opera, es utilizada tanto por Bitcoin Core como por Liquid para ofrecer estos algoritmos de firmas digitales. Estos algoritmos emplean una operación matemática llamada inverso modular, que es un componente relativamente costoso del cálculo.
Introducción de un Nuevo Algoritmo de Inversión Modular
En «Cálculo de gcd de tiempo constante rápido e inversión modular», Daniel J. Bernstein y Bo-Yin Yang desarrollan un nuevo algoritmo de inversión modular. En 2021, este algoritmo, referido como «safegcd», fue implementado para libsecp256k1 por Peter Dettman. Como parte del proceso de evaluación de este nuevo algoritmo, Blockstream Research completó la primera verificación formal del diseño del algoritmo utilizando el asistente de pruebas Coq para verificar formalmente que el algoritmo realmente termina con el resultado correcto del inverso modular en entradas de 256 bits.
La Brecha entre el Algoritmo y su Implementación
El esfuerzo de formalización en 2021 solo mostró que el algoritmo diseñado por Bernstein y Yang funciona correctamente. Sin embargo, utilizar ese algoritmo en libsecp256k1 requiere implementar la descripción matemática del algoritmo safegcd dentro del lenguaje de programación C. Por ejemplo, la descripción matemática del algoritmo realiza la multiplicación de matrices de vectores que pueden tener hasta 256 bits de enteros con signo, sin embargo, el lenguaje de programación C solo proporciona nativamente enteros de hasta 64 bits (o 128 bits con algunas extensiones del lenguaje).
- Implementar el algoritmo safegcd requiere programar la multiplicación de matrices y otros cálculos utilizando enteros de 64 bits en C.
- Se han añadido muchas otras optimizaciones para hacer que la implementación sea rápida.
- Finalmente, hay cuatro implementaciones separadas del algoritmo safegcd en libsecp256k1: dos algoritmos de tiempo constante para la generación de firmas, uno optimizado para sistemas de 32 bits y otro optimizado para sistemas de 64 bits, y dos algoritmos de tiempo variable para la verificación de firmas, nuevamente uno para sistemas de 32 bits y otro para sistemas de 64 bits.
C Verificable
Para verificar que el código en C implementa correctamente el algoritmo safegcd, todos los detalles de implementación deben ser revisados. Usamos C Verificable, parte de la Cadena de Herramientas de Software Verificado, para razonar sobre el código en C utilizando el teorema probador Coq.
La verificación procede especificando precondiciones y postcondiciones usando lógica de separación para cada función en verificación. La lógica de separación es una lógica especializada para razonar sobre subrutinas, asignaciones de memoria, concurrencia y más. Una vez que cada función tiene una especificación, la verificación procede comenzando desde la precondición de una función, y estableciendo un nuevo invariante después de cada declaración en el cuerpo de la función, hasta finalmente establecer la postcondición al final del cuerpo de la función o al final de cada declaración de retorno. La mayor parte del esfuerzo de formalización se gasta «entre» las líneas de código, utilizando los invariantes para traducir las operaciones en bruto de cada expresión C en declaraciones de nivel superior sobre lo que las estructuras de datos que se manipulan representan matemáticamente. Por ejemplo, lo que el lenguaje C considera un arreglo de enteros de 64 bits puede en realidad ser una representación de un entero de 256 bits.
El resultado final es una prueba formal, verificada por el asistente de prueba Coq, de que la implementación de tiempo variable de 64 bits del algoritmo de inverso modular safegcd en libsecp256k1 es funcionalmente correcta.
Limitaciones de la Verificación
Existen algunas limitaciones en la prueba de corrección funcional. La lógica de separación usada en C Verificable implementa lo que se conoce como corrección parcial. Esto significa que solo demuestra que el código en C devuelve el resultado correcto si devuelve, pero no prueba la terminación en sí. Mitigamos esta limitación utilizando nuestra prueba anterior de Coq de los límites en el algoritmo safegcd para probar que el valor del contador del bucle principal, de hecho, nunca excede las 11 iteraciones.
Otro problema es que el propio lenguaje C no tiene una especificación formal. En su lugar, el proyecto C Verificable usa el proyecto del compilador CompCert para proporcionar una especificación formal de un lenguaje C. Esto garantiza que cuando un programa C verificado se compila con el compilador CompCert, el código de ensamblaje resultante cumplirá con su especificación (sujeto a la limitación anterior). Sin embargo, esto no garantiza que el código generado por GCC, clang o cualquier otro compilador necesariamente funcione. Por ejemplo, a los compiladores C se les permite tener órdenes de evaluación diferentes para los argumentos dentro de una llamada a función. E incluso si el lenguaje C tuviera una especificación formal, cualquier compilador que no sea formalmente verificado podría aún compilar erróneamente programas. Esto sí ocurre en la práctica.
Por último, C Verificable no admite pasar estructuras, devolver estructuras o asignar estructuras. Mientras que en libsecp256k1, las estructuras siempre son pasadas por puntero (lo cual está permitido en C Verificable), hay algunas ocasiones en las que se utiliza la asignación de estructuras. Para la prueba de corrección del inverso modular, hubo 3 asignaciones que tuvieron que ser reemplazadas por una llamada a una función especializada que realiza la asignación de la estructura campo por campo.
Resumen
Blockstream Research ha verificado formalmente la corrección de la función de inverso modular de libsecp256k1. Este trabajo proporciona más evidencia de que la verificación del código C es posible en la práctica. Usar un asistente de prueba de propósito general nos permite verificar el software construido sobre argumentos matemáticos complejos.
Nada impide que el resto de funciones implementadas en libsecp256k1 sean verificadas también. Así, es posible que libsecp256k1 obtenga las máximas garantías posibles de corrección del software.
Preguntas Frecuentes
- ¿Qué es el algoritmo safegcd y quién lo implementó?
- ¿Por qué es importante verificar el código C de libsecp256k1?
- ¿Cuáles son las limitaciones de la verificación con C Verificable?
El algoritmo safegcd es un nuevo algoritmo de inversión modular desarrollado por Daniel J. Bernstein y Bo-Yin Yang, implementado para libsecp256k1 por Peter Dettman en 2021.
La verificación del código C asegura que la implementación sea funcionalmente correcta y proporcione garantías de corrección de software, crucial para la seguridad de firmas digitales utilizadas por Bitcoin y Liquid.
C Verificable comprueba la corrección funcional, pero no garantiza la terminación. También existe la dependencia de compiladores específicos para asegurar que la implementación mantenga su corrección funcional al ser compilada.
