Resumen Técnico: GCD: Garbled, Corrected, Demonstrandum

Planteamiento del Problema

El artículo aborda la corrección y verificación de la implementación del Algoritmo de Euclides Extendido (GCD Extendido) dentro de la biblioteca estándar de Go (crypto/internal/fips140/bigmod). Esta implementación es crítica para la generación de pares de claves RSA, un componente fundamental para TLS, SSH y PGP. La implementación de Go fue introducida en Go 1.24 para soportar nativamente el cumplimiento con FIPS 140-3, reemplazando la dependencia de BoringSSL.

Los autores identificaron una discrepancia crítica: aunque se afirmaba que el código de Go era un port directo de la implementación de BoringSSL (la cual está formalmente verificada mediante el asistente de pruebas Rocq vía Fiat Cryptography), la versión de Go contenía desviaciones sutiles. Estas desviaciones no fueron detectadas por tres revisiones de código separadas. Las desviaciones rompieron los invariantes matemáticos del algoritmo, comprometiendo potencialmente la corrección del cálculo del inverso modular requerido para las claves privadas RSA. Además, la implementación de Go permitía un dominio de entrada más grande que la versión probada de BoringSSL, invalidando los supuestos de la prueba existente.

Metodología

Los autores emplearon un enfoque de verificación deductiva de programas utilizando Gobra, un verificador basado en lógica de separación para Go. La metodología consistió en:

1. Especificación Formal: Los autores formalizaron las especaciones en lenguaje natural de las funciones de Go (extendedGCD, InverseVarTime, GCDVarTime) en especificaciones de Gobra, incluyendo precondiciones, postcondiciones e invariantes de bucle.
2. Análisis de Desviaciones: Al intentar verificar el código de Go existente contra las especificaciones derivadas de la prueba de BoringSSL, los autores identificaron dos clases principales de desviaciones:
   • Restas Desincronizadas: La implementación de Go actualizaba los coeficientes de Bézout ($A, B, C, D$) de forma independiente basándose en condiciones locales, mientras que la implementación de referencia requería reducciones sincronizadas para mantener los invariantes del bucle.
   • Expansión del Dominio de Entrada: La implementación de Go permitía entradas donde $a \ge n$, violando la precondición $a < n$ requerida por la prueba original.
3. Construcción de la Prueba:
   • Corrección de Código: Los autores propusieron una corrección para las restas desincronizadas para alinear la lógica de Go con los invariantes matemáticos.
   • Adaptación de la Prueba: Portaron la prueba existente de BoringSSL de Rocq a Gobra. Para la desviación del dominio de entrada, relajaron los invariantes y las postcondiciones para cubrir el caso donde $a \ge n$, demostrando que el valor del GCD permanece correcto incluso si la propiedad del inverso modular no se cumple en ese caso específico.
   • Verificación Híbrida: Para los lemas de aritmética no lineal que el solver SMT Z3 (utilizado por Gobra) no podía manejar, los autores utilizaron el asistente de pruebas Lean para demostrar lemas clave e importaron estos a Gobra como lemas trusted (de confianza).
4. Verificación Asistida por IA: Los autores utilizaron un agente de IA (Claude Code de Anthropic) para refinar iterativamente los invariantes y lemas basados en los mensajes de error de Gobra, reduciendo significamente el esfuerzo manual en el proceso de construcción de la prueba.

Contribuciones Clave

• Descubrimiento de Errores (Bugs): El artículo descubre dos desviaciones sutiles pero críticas en la implementación de Extended GCD de Go que rompen los invariantes algorítmicos. Estos errores estaban presentes en un código que había pasado por múltiples revisiones y que se afirmaba era un port directo de una implementación verificada.
• Optimización de Rendimiento: La corrección propuesta para la desviación de la resta desincronizada no solo restaura la corrección, sino que también resulta en una aceleración promedio del 24% (media geométrica) al eliminar asignaciones de memoria innecesarias y operaciones redundantes en el cuerpo del bucle.
• Verificación Formal de Go Crypto: Los autores verifican con éxito la implementación corregida de Go, su terminación y su corrección frente a especificaciones formales utilizando Gobra. Esta es la primera verificación formal de este componente específico en la biblioteca estándar de Go.
• Portabilidad y Generalización de Pruebas: Lograron portar con éxito una prueba de Rocq (Fiat Cryptography) a Gobra y generalizarla para cubrir el dominio de entrada más amplio permitido por la implementación de Go.
• IA en la Verificación: El trabajo demuestra la eficacia de los agentes de IA para facilitar la verificación formal mediante la iteración autónoma sobre especificaciones e identificación de las causas raíz de los fallos de la prueba (por ejemplo, sugiriendo que la reducción independiente de coeficientes era el problema).

Resultados

• Corrección: La implementación corregida se verificó con éxito en 16.9 segundos en una computadora portátil estándar. La verificación cubre la función extendedGCD y sus clientes InverseVarTime y GCDVarTime.
• Rendimiento: Los benchmarks a través de varios tamaños de limb (de 64 a 8192 bits) mostraron que la implementación verificada es consistentemente más rápida que la original. La aceleración promedio fue del 23.98%, con mejoras que oscilan entre el 15.6% y el 36% dependiendo del tamaño de la entrada. La aceleración se atribuye a las actualizaciones in-place y a la eliminación de las asignaciones de buffers intermedios.
• Divulgación e Impacto: Los autores divulgaron las desviaciones a los mantenedores de criptografía de Go. Los mantenedores confirmaron que, si bien las desviaciones podrían teóricamente conducir a inversos modulares incorrectos, las comprobaciones defensivas en el código de generación de claves RSA capturarían estos errores y devolverían un error en lugar de una clave incorrecta, limitando el impacto a la disponibilidad en lugar de un compromiso de seguridad. Las correcciones están bajo revisión para su inclusión en la biblioteca estándar de Go.
• Integración Continua: Debido al rápido tiempo de verificación, la prueba se ha integrado en el flujo de trabajo de Integración Continua (CI) del proyecto para verificar automáticamente futuras desviaciones.

Significado y Reivindicaciones

El artículo afirma que su trabajo destaca tres ideas primordiales:

1. Errores Sutiles en Código Revisado: Incluso el código bien revisado, especialmente cuando se afirma que es un port directo de una implementación verificada, puede contener errores sutiles que rompen los invariantes.
2. El Poder de la Verificación Formal: La verificación formal es una herramienta poderosa para descubrir este tipo de errores que las pruebas y la revisión manual podrían pasar por alto.
3. El Rol de los Agentes de IA: Los agentes de IA pueden facilitar eficazmente la verificación mediante la iteración de invariantes y lemas basada en la retroalimentación del verificador, aunque la supervisión humana sigue siendo necesaria para la limpieza final y la comprensión estructural.

Los autores enfatizan que su trabajo cierra la brecha entre la implementación y su prueba. Al verificar el código de Go directamente, en lugar de confiar en la existencia de una prueba para una implementación diferente (BoringSSL), aseguran que el código específico que se ejecuta en producción es matemáticamente sólido. También señalan que, aunque dependen de funciones trusted para operaciones de bits de bajo nivel, el argumento de corrección general se desglosa en componentes pequeños y revisables, aumentando la confianza en la fiabilidad del sistema.