Tras años de secreto, Apple hace pública su criptografía: por qué importa
Así es la preparación de un ataque que aún no existe.
Apple decidió someter una de las partes más cerradas de su protección a revisión pública. La compañía publicó el código de criptografía resistente a la cuántica y las herramientas con las que verificó su corrección matemática. Esta medida debería ayudar no solo a Apple, sino también a otros actores de la industria que se preparan para la era de potentes ordenadores cuánticos.
En acceso abierto se publicaron las implementaciones de dos algoritmos, ML-KEM y ML-DSA, así como bibliotecas y herramientas de verificación formal. Apple afirma que logró uno de los métodos más fiables para confirmar la corrección de implementaciones operativas de tales algoritmos.
Los algoritmos ya están integrados en corecrypto, la biblioteca criptográfica de Apple, que funciona en los sistemas operativos de la compañía y atiende a más de 2,5 mil millones de dispositivos activos. Apple comenzó a implementar la protección resistente a la cuántica en iMessage en 2024, y luego amplió el uso de la tecnología a servicios VPN y al protocolo de red TLS.
Entre las herramientas publicadas hay un traductor Cryptol-a-Isabelle. Traduce modelos criptográficos entre lenguajes formales y ayuda a verificar si el código cumple los estándares oficiales. Para esa verificación Apple utilizó Cryptol, desarrollado por Galois, e Isabelle, creado con la participación de la Universidad de Cambridge y la Universidad Técnica de Múnich.
La verificación formal ya ayudó a encontrar un error que las pruebas habituales podrían no haber detectado. En el código de ML-DSA, los especialistas de Apple encontraron un paso de cálculo omitido. Ese error podría haber alterado silenciosamente el funcionamiento de las firmas digitales, de modo que los mensajes en iMessage parecerían auténticos aunque la protección funcionara de forma incorrecta.
Apple reconoce que las pruebas matemáticas por sí solas no son suficientes. Parte del código aún necesita ser probada por métodos convencionales y verificada en el contexto del sistema completo. La compañía considera que el enfoque más fiable es mixto, cuando la verificación formal confirma los cálculos principales y las pruebas convencionales reducen los demás riesgos.
ML-KEM y ML-DSA fueron elegidos de entre los algoritmos estandarizados resistentes a la cuántica por su equilibrio entre seguridad, velocidad y compacidad de parámetros. Estos algoritmos deben proteger los datos frente a futuros ordenadores cuánticos, que pueden romper muchos esquemas modernos de cifrado.