Apple ha lanzado un código criptográfico resistente a los cuánticos y las herramientas de verificación matemática que desarrolló para demostrar la exactitud del código, poniéndolos a disposición del público para su revisión independiente y su uso más amplio en toda la industria.

la liberación Incluye implementaciones de dos algoritmos de seguridad cuántica, ML-KEM y ML-DSA, junto con las bibliotecas y herramientas de verificación formal que Apple creó para validar su precisión. La compañía también publicó documentación detallada de su metodología de verificación, que describe como el logro de los resultados de corrección más sólidos conocidos para cualquier implementación de producción ampliamente implementada de estos algoritmos.

Los algoritmos de seguridad cuántica están integrados en núcleocriptola biblioteca criptográfica de Apple utilizada en todos sus sistemas operativos. La biblioteca maneja cifrado, descifrado, hash y firmas digitales en más de 2.500 millones de dispositivos activos. Apple comenzó a implementar cifrado resistente a los cuánticos en iMessage en 2024 y ha ampliado la tecnología a servicios VPN y protocolos de red TLS.

Una de las herramientas lanzadas es el traductor Cryptol-to-Isabelle de la compañía, que convierte modelos criptográficos entre lenguajes formales, junto con las bibliotecas de soporte necesarias para reproducir los resultados. La verificación formal utiliza pruebas matemáticas para demostrar que el código funciona correctamente para todas las entradas posibles. Apple tradujo su código al criptolun lenguaje formal desarrollado por Galois, luego en Isabelasistente de pruebas de la Universidad de Cambridge y de la Universidad Técnica de Munich, para demostrar que ambas cumplían con los estándares oficiales. Apple ha utilizado Isabelle anteriormente para verificar componentes criptográficos de hardware.

El proceso de verificación descubrió errores que las pruebas convencionales habrían pasado por alto. Los investigadores encontraron un paso computacional faltante en el código ML-DSA que habría roto silenciosamente las firmas digitales. Si este error hubiera llegado a producción, los mensajes en iMessage podrían haber aparecido autenticados cuando en realidad no lo estaban, dejando a los usuarios sin saber que sus comunicaciones carecían de la seguridad adecuada.

Incluso con estas herramientas, Apple reconoció que todavía depende de las pruebas criptográficas convencionales y que se necesita una evaluación para garantizarlo. La verificación formal puede detectar errores que las pruebas tradicionales simplemente no pueden encontrar. Las pruebas funcionan probando muchos escenarios, pero con un código criptográfico complejo, hay demasiadas entradas posibles para realizar pruebas exhaustivas. Los errores sutiles pueden ocultarse en los espacios entre los casos de prueba y nunca generar una advertencia. La verificación formal, por el contrario, utiliza las matemáticas para demostrar la corrección de todas las entradas posibles a la vez.

Sin embargo, el equipo de Apple escribe que no pudo verificar formalmente cada aspecto de su código con las herramientas disponibles, por lo que combinaron enfoques: verificación formal de la corrección matemática básica, pruebas convencionales para aspectos que los métodos formales no podían cubrir y evaluación cuidadosa de cómo funcionan todas las piezas juntas. Apple sostiene que este enfoque híbrido proporciona la seguridad más sólida para el software criptográfico crítico.

«Basándonos en nuestro trabajo hasta la fecha, creemos que la mayor garantía posible proviene de combinar la verificación formal con métodos convencionales y evaluar críticamente los resultados de un extremo a otro», se lee en la publicación del blog.

Además, el blog afirma que Apple seleccionó ML-KEM y ML-DSA entre varios algoritmos estandarizados resistentes a lo cuántico porque cumplían mejor con los requisitos de seguridad, rendimiento y parámetros compactos de la empresa. Los algoritmos abordan la amenaza que plantean las futuras computadoras cuánticas, que podrían potencialmente romper los métodos de cifrado que actualmente protegen las comunicaciones digitales.

Se puede encontrar más información en corecrypto de Apple. página de GitHub.