KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
Este artículo presenta una prueba totalmente mecanizada en el probador Rocq de que el compilador Jasmin preserva tanto la corrección funcional como la seguridad KEM-IND-CCA para la implementación altamente optimizada de ML-KEM utilizada en Signal, lograda a través de un nuevo marco de seguridad basado en juegos, semántica de árbol de interacción que soporta computaciones probabilísticas y una lógica de Hoare relacional.
Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo
En el mundo de alto riesgo de la seguridad digital, la criptografía actúa como la cerradura invisible que protege todo, desde los mensajes privados hasta las transacciones financieras. Durante décadas, los expertos han dependido de pruebas matemáticas para asegurar que estas cerraduras sean inquebrantables, pero ha persistido una brecha crítica entre la elegante matemática en el papel y la desordenada realidad del código informático que las ejecuta. Incluso cuando un esquema criptográfico es probado como seguro en teoría, el proceso de traducir esa teoría a las instrucciones específicas que entiende un procesador de computadora puede introducir errores sutiles. Estos errores, introducidos a menudo por los compiladores que realizan la traducción, pueden crear vulnerabilidades que los atacantes explotan. Mientras el mundo se prepara para la transición hacia nuevos estándares de cifrado resistentes al computo cuántico para protegerse contra amenazas futuras, asegurar que estos nuevos sistemas permanan seguros en todo el camino hasta el código de máquina ya no es solo una preocupación teórica; es una necesidad para la seguridad de las redes de comunicación globales.
Un equipo de investigadores ha cerrado ahora esta brecha para uno de los nuevos estándares de cifrado más importantes, conocido como ML-KEM, que ya se está utilizando en aplicaciones de mensajería segura populares como Signal. Su trabajo demuestra que la herramienta de software específica utilizada para traducir el código de seguridad de alto nivel en instrucciones de máquina no rompe accidentalmente las garantías de seguridad. En esencia, han demostrado que las propiedades de seguridad establecidas para el código original, legible por humanos, se preservan perfectamente en el código ensamblador optimizado y final que la computadora realmente ejecuta. Este logro es significativo porque elimina la necesidad de confiar en el compilador como una "caja negra" que podría contener errores ocultos; en su lugar, el propio compilador ha sido verificado matemáticamente como un puente seguro entre las pruebas de seguridad abstractas y el hardware físico.
El desafío que enfrentaron los investigadores fue único debido a la naturaleza de la criptografía moderna. El algoritmo específico que estudiaron, ML-KEM, depende de una técnica llamada muestreo de rechazo (rejection sampling), donde la computadora intenta repetidamente números aleatorios hasta encontrar uno que encaje con un patrón específico. Este proceso significa que el programa no siempre se ejecuta durante un tiempo fijo; podría terminar rápidamente, o podría tomar muchos más intentos de los esperados. Los métodos anteriores para la verificación de compiladores fueron diseñados para programas que se ejecutan en una secuencia de pasos predecible y fija. Tenían dificultades para manejar este tipo de comportamiento probabilístico, donde el camino que toma el código depende del azar. Si una herramienta de verificación de compiladores no puede dar cuenta de estos bucles aleatorios, no puede garantizar que el código de máquina final se comporte de la misma manera que el diseño original, dejando un posible hueco en la cadena de seguridad.
Para resolver esto, los investigadores construyeron un nuevo marco para comprender cómo se comportan estos programas. Trataron la ejecución del código no como una simple lista de instrucciones, sino como un árbol de posibles interacciones, donde cada elección aleatoria y cada interacción con el mundo exterior es una rama en el árbol. Este enfoque les permitió modelar la terminación "casi segura" del programa, lo que significa que eventualmente terminará con una probabilidad de uno, incluso si el tiempo exacto es impredecible. Al utilizar este nuevo modelo, pudieron definir qué significa que un compilador sea correcto en un entorno probabilístico. Demostraron que para cada posible camino que el código original podría tomar, el código compilado toma un camino coincidente, preservando la misma distribución exacta de resultados.
El equipo aplicó este marco al compilador Jasmin, una herramienta diseñada específicamente para escribir código criptográfico de alta seguridad. Se centraron en la implementación de ML-KEM utilizada en Signal, una aplicación de mensajería con millones de usuarios. Utilizando un asistente de pruebas potente, una herramienta de software que verifica argumentos matemáticos con absoluta rigurosidad, verificaron que el compilador traduce correctamente el código fuente al lenguaje ensamblador sin alterar las propiedades de seguridad. Su prueba cubre todo el proceso de compilación, desde la descripción inicial de alto nivel hasta las instrucciones de máquina finales. El resultado es una garantía de que la seguridad del cifrado, que anteriormente solo se había probado para el código fuente, ahora es válida para el código real que se ejecuta en el dispositivo del usuario.
Este trabajo es parte de un esfuerzo mayor para aportar los niveles más altos de aseguramiento a la transición post-cuántica, un cambio global hacia métodos de cifrado que puedan resistir ataques de futuras computadoras cuánticas. Si bien los investigadores aún no han extendido su prueba para cubrir ataques de canal lateral (side-channel attacks) —donde un atacante podría aprender secretos observando cuánto tiempo tarda una computación o cuánta energía utiliza—, han sentado la base necesaria para dicho trabajo futuro. Al establecer que el compilador preserva el juego de seguridad central, han creado una base sólida sobre la cual se pueden construir garantías de seguridad más complejas. La verificación está totalmente mecanizada, lo que significa que cada paso de la prueba ha sido revisado por una computadora, sin dejar lugar al error humano en la lógica misma.
Las implicaciones de este trabajo se extienden más allá de un solo algoritmo. El marco que los investigadores desarrollaron es lo suficientemente general como para aplicarse a otros esquemas criptográficos y propiedades de seguridad. Han demostrado que es posible razonar sobre la seguridad basada en juegos, una forma estándar de definir la fuerza criptográfica, a través de la lente de la corrección del compilador. Esto significa que, a medida que se desarrollan e implementan nuevos estándares de cifrado, estos pueden ser sometidos al mismo proceso de verificación rigurosa. Los investigadores han hecho que sus herramientas y pruebas sean de código abierto, permitiendo que otros expertos inspeccionen, verifiquen y construyan sobre su trabajo. Esta transparencia es crucial para mantener la confianza en la infraestructura digital que sustenta la sociedad moderna.
Al final, este trabajo representa un paso significativo hacia un futuro en el que podemos estar seguros de que las cerraduras digitales que protegen nuestros datos son exactamente tan fuertes como los matemáticos que las diseñaron prometieron. Al cerrar la brecha entre las pruebas de seguridad abstractas y la realidad concreta del código de máquina, los investigadores han eliminado una fuente importante de incertidumbre de la cadena de suministro criptográfica. Su trabajo asegura que, cuando un usuario envía un mensaje seguro, las garantías de seguridad en las que confía no son solo ideales teóricos, sino propiedades que se preservan matemáticamente en todo el camino hasta los chips de silicio en sus dispositivos. Este nivel de aseguramiento es lo que nos permite confiar en la tecnología que nos conecta, incluso mientras enfrentamos amenazas nuevas y en evolución en la era digital.
¿Ahogado en artículos de tu campo?
Recibe resúmenes diarios de los artículos más novedosos que coincidan con tus palabras clave de investigación — con resúmenes técnicos, en tu idioma.