Introducción
La seguridad de Bitcoin y otras cadenas de bloques, como Liquid, depende del uso de algoritmos de firmas digitales como las firmas ECDSA y Schnorr. La biblioteca AC llamada libsecp256k1, que lleva el nombre de la curva elíptica en la que opera la biblioteca, es utilizada tanto por Bitcoin Core como por Liquid para proporcionar estos algoritmos de firma digital. Estos algoritmos hacen uso de un cálculo matemático llamado inversa modularque es un componente relativamente costoso del cálculo.
En “Cálculo rápido del mcd en tiempo constante e inversión modular”, Daniel J. Bernstein y Bo-Yin Yang desarrollan un nuevo algoritmo de inversión modular. En 2021, Peter Dettman implementó este algoritmo, denominado “safegcd”, para libsecp256k1. Como parte del proceso de investigación de este novedoso algoritmo, Blockstream Research fue el primero en completar una verificación formal del diseño del algoritmo utilizando el asistente de prueba Coq para verificar formalmente que el algoritmo efectivamente termina con el resultado inverso modular correcto en 256 bits. entradas.
La brecha entre algoritmo e implementación
El esfuerzo de formalización de 2021 sólo demostró que el algoritmo diseñado por Bernstein y Yang funciona correctamente. Sin embargo, usar 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 matricial de vectores que pueden tener un ancho de hasta enteros con signo de 256 bits; sin embargo, el lenguaje de programación C solo proporcionará de forma nativa números enteros de hasta 64 bits (o 128 bits con algunas extensiones de lenguaje).
La implementación del algoritmo safegcd requiere programar la multiplicación de matrices y otros cálculos utilizando enteros de 64 bits de C. Además, se han agregado muchas otras optimizaciones para agilizar la implementación. Al final, 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 verificación de firmas, nuevamente. uno para sistemas de 32 bits y otro para sistemas de 64 bits.
Verificable C
Para verificar que el código C implemente correctamente el algoritmo safegcd, se deben verificar todos los detalles de implementación. Usamos Verifiable C, parte de Verified Software Toolchain para razonar sobre el código C usando el demostrador del teorema de Coq.
La verificación procede especificando condiciones previas y posteriores utilizando una lógica de separación para cada función sometida a verificación. La lógica de separación es una lógica especializada en razonar sobre subrutinas, asignaciones de memoria, concurrencia y más.
Una vez que se le da una especificación a cada función, la verificación continúa comenzando desde la condición previa 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 condición posterior al final del cuerpo de la función o al final de cada declaración de devolución. La mayor parte del esfuerzo de formalización se gasta “entre” las líneas de código, utilizando los invariantes para traducir las operaciones sin procesar de cada expresión C en declaraciones de nivel superior sobre lo que representan matemáticamente las estructuras de datos que se manipulan. Por ejemplo, lo que el lenguaje C considera una matriz de enteros de 64 bits puede ser en realidad 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 de libsecp256k1 del algoritmo inverso modular safegcd es funcionalmente correcta.
Limitaciones de la verificación
Existen algunas limitaciones para la prueba de corrección funcional. La lógica de separación utilizada en Verifiable C implementa lo que se conoce como corrección parcial. Eso significa que solo prueba que el código C regresa con el resultado correcto. si regresa, pero no prueba la terminación en sí. Mitigamos esta limitación utilizando nuestra prueba Coq anterior de los límites del algoritmo safegcd para demostrar que el valor del contador del bucle principal, de hecho, nunca excede las 11 iteraciones.
Otro problema es que el lenguaje C en sí no tiene una especificación formal. En cambio, el proyecto Verifiable C utiliza el proyecto del compilador CompCert para proporcionar una especificación formal de un lenguaje C. Esto garantiza que cuando se compila un programa C verificado con el compilador CompCert, el código ensamblador 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 funcione necesariamente. Por ejemplo, a los compiladores de C se les permite tener diferentes órdenes de evaluación para los argumentos dentro de una llamada de función. E incluso si el lenguaje C tuviera una especificación formal, cualquier compilador que no esté formalmente verificado aún podría compilar mal los programas. Esto ocurre en la práctica.
Por último, Verifiable C no admite estructuras de paso, estructuras de retorno o estructuras de asignación. Mientras que en libsecp256k1 las estructuras siempre se pasan por puntero (lo cual está permitido en Verifiable C), hay algunas ocasiones en las que se utiliza la asignación de estructuras. Para la prueba de corrección inversa modular, hubo 3 asignaciones que tuvieron que ser reemplazadas por una llamada de función especializada que realiza la asignación de estructura campo por campo.
Resumen
Blockstream Research ha verificado formalmente la exactitud de la función inversa modular de libsecp256k1. Este trabajo proporciona evidencia adicional de que la verificación del código C es posible en la práctica. El uso de un asistente de prueba de propósito general nos permite verificar software basado en argumentos matemáticos complejos.
Nada impide que también se verifiquen el resto de funciones implementadas en libsecp256k1. Por lo tanto, es posible que libsecp256k1 obtenga las mayores garantías posibles de corrección del software.
Esta es una publicación invitada de Russell O’Connor y Andrew Poelstra. Las opiniones expresadas son enteramente propias y no reflejan necesariamente las de BTC Inc o Bitcoin Magazine.
