Apple ha publicado sus implementaciones de criptografía postcuántica en corecrypto, junto con pruebas matemáticas y herramientas de verificación para la evaluación independiente por parte de expertos, lo que permite a investigadores externos revisar el trabajo y reproducir el análisis de la compañía.
La criptografía postcuántica está diseñada para proteger los datos cifrados de los futuros ordenadores cuánticos que podrían romper los algoritmos de cifrado de clave pública ampliamente utilizados.
Un plan para la verificación formal de Apple corecrypto
Apple ha publicado en la plataforma GitHub el código fuente de su biblioteca de criptografía de bajo nivel corecrypto, lo que permite a los desarrolladores vislumbrar cómo están combatiendo las amenazas que plantea la computación cuántica futura.
En 2024, os comenté cómo el servicio iMessage contó con el cifrado post-cuántico con el protocolo PQ3. Ahora, la compañía californiana ofrece sus herramientas de seguridad más potentes para un análisis detallado.
El archivo publicado contiene el código fuente utilizado en todas las plataformas de Apple. Con el lanzamiento de corecrypto esta semana, Apple comenta sus implementaciones de los algoritmos ML-KEM y ML-DSA cuánticamente seguros, junto con las pruebas matemáticas que crearon para asegurar su fidelidad a las especificaciones FIPS 203 y FIPS 204, para su evaluación independiente por parte de expertos. Además, para seguir avanzando en el estado del arte en la garantía de software crítico, también publicó Apple las bibliotecas y herramientas de verificación formal que creamos para lograr los resultados de corrección más sólidos conocidos para cualquier implementación de producción ampliamente desplegada de los algoritmos relevantes.
Apple pone estas herramientas a disposición del público para su uso generalizado y un control independiente y riguroso. Una protección de alta calidad contra las potentes máquinas cuánticas exige una impecabilidad absoluta. Por lo tanto, los materiales publicados incluyen un componente especial dedicado a la denominada verificación formal.
Cómo funciona el sistema de verificación
La verificación formal utiliza métodos matemáticos para demostrar que el software se comporta según lo previsto en condiciones definidas.
ML-KEM y ML-DSA, algoritmos post-cuánticos estandarizados por el NIST, fueron seleccionados por su seguridad, rendimiento, tamaño compacto de claves y textos cifrados, y corrección funcional. Las implementaciones se validaron mediante pruebas convencionales, simulación, revisión independiente y verificación formal.
Tras evaluar las herramientas de verificación existentes y las implementaciones verificadas, Apple creó un sistema personalizado que admite múltiples lenguajes de programación, bases de código y flujos de trabajo de desarrolladores existentes.
El marco combina herramientas existentes y de reciente desarrollo para verificar las implementaciones conforme a los estándares oficiales FIPS. Galois, una empresa de investigación e ingeniería especializada en verificación formal, colaboró con Apple para desarrollar una herramienta que genera teorías de Isabelle a partir de modelos Cryptol y conecta C portable con Cryptol. Apple también desarrolló bibliotecas de Isabelle y optimizó manualmente subrutinas de ensamblador ARM64.
Según Apple, con la publicación del código fuente de corecrypto el 22 de mayo de 2026, quieren compartir los avances significativos en verificación formal aplicada con la comunidad criptográfica global, incluyendo los detalles de nuestro enfoque y las herramientas que usan. Su publicación abierta busca fomentar una mayor adopción, respaldar la revisión crítica de nuestro trabajo y contribuir al avance de las técnicas para garantizar la seguridad del software crítico
