La seguridad de Bitcoin y otras blockchains, como Liquid, depende de algoritmos de firma digital como ECDSA y firmas de Schnorr. Una biblioteca C llamada libsecp256k1 proporciona estos algoritmos y es utilizada tanto por Bitcoin Core como por Liquid. Estos algoritmos utilizan un cálculo llamado inversa modular, que es una parte costosa del proceso.
En “Cálculo rápido de gcd en tiempo constante e inversión modular,” Daniel J. Bernstein y Bo-Yin Yang crearon un nuevo algoritmo de inversión modular llamado “safegcd.” Este algoritmo fue implementado para libsecp256k1 por Peter Dettman en 2021. Blockstream Research verificó formalmente el diseño del algoritmo utilizando el asistente de pruebas Coq, demostrando que calcula correctamente la inversa modular para entradas de 256 bits.
Sin embargo, implementar el algoritmo safegcd requirió adaptar la descripción matemática para ajustarse al lenguaje de programación C, que solo admite enteros de hasta 64 bits de forma nativa. Se agregaron varias optimizaciones para hacer que la implementación sea rápida, lo que resultó en cuatro implementaciones separadas del algoritmo safegcd en libsecp256k1.
Para asegurar que el código C implemente correctamente el algoritmo safegcd, se utilizó Verifiable C, parte de la Verified Software Toolchain, junto con el probador de teoremas Coq. Esto implicó especificar precondiciones y poscondiciones para cada función que se somete a verificación utilizando lógica de separación. El proceso de verificación comenzó entonces desde la precondición de la función y estableció un nuevo invariante después de cada declaración en el cuerpo de la función, hasta que se alcanzó la poscondición al final del cuerpo de la función o en las declaraciones de retorno.
La mayor parte del esfuerzo de formalización se dedicó a traducir las operaciones en bruto de cada expresión C en declaraciones de nivel superior sobre lo que representan matemáticamente las estructuras de datos que se manipulan. La verificación resultó en una prueba formal, verificada por el asistente de pruebas Coq, de que la implementación de tiempo variable de 64 bits del algoritmo de inversa modular safegcd de libsecp256k1 es funcionalmente correcta.
Sin embargo, hay algunas limitaciones en la prueba de corrección funcional. La lógica de separación utilizada en Verifiable C solo prueba la corrección parcial, lo que significa que solo muestra que el código C devuelve el resultado correcto si retorna, pero no prueba la terminación en sí. Para abordar esto, se utilizó una prueba previa de Coq de los límites en el algoritmo safegcd para probar que el valor del contador del bucle principal nunca excede 11 iteraciones.
Otra limitación es que el propio lenguaje C no tiene una especificación formal. En cambio, el proyecto Verifiable C utiliza el proyecto del compilador CompCert para proporcionar una especificación formal del lenguaje C. Esto garantiza que cuando un programa C verificado se compila con el compilador CompCert, el código ensamblador resultante cumplirá con su especificación, pero no garantiza que el código generado por otros compiladores funcionará necesariamente.
Además, Verifiable C no admite pasar, devolver o asignar estructuras. En libsecp256k1, las estructuras siempre se pasan por puntero, lo cual está permitido en Verifiable C, pero hay algunas ocasiones en las que se utiliza la asignación de estructuras. En resumen, Blockstream Research ha verificado formalmente la corrección de la función de inversa modular de libsecp256k1, proporcionando más evidencia de que la verificación del código C es posible en la práctica.
Este trabajo también destaca que el resto de las funciones implementadas en libsecp256k1 podrían ser verificadas también, permitiendo que la biblioteca logre las mayores garantías posibles de corrección de software.
Fuente
<p>¡La publicación Cómo las Firmas Digitales Hacen Seguro a Bitcoin! apareció primero en CoinBuzzFeed.</p>
