Apple has published its post-quantum cryptography implementations in corecrypto, together with mathematical proofs and verification tools for independent expert evaluation, allowing external researchers to review the work and reproduce the company’s analysis.

Post-quantum cryptography is designed to protect encrypted data from future quantum computers that could break widely used public-key encryption algorithms.

A new approach to formal verification of Apple corecrypto (Source: Apple)

Corecrypto, the cryptography library used throughout Apple operating systems and services, provides encryption, hashing, random number generation, and digital signatures on more than 2.5 billion active devices. The company added post-quantum cryptography support to the library in 2024 for applications that handle encrypted communications and sensitive data, including iMessage, VPNs, and TLS networking.

“A critical bug in corecrypto has the potential to compromise the security and reliability of every app and feature that depends on it, so we are conservative when adding new code to the library and make exceptional efforts to be comprehensive in our testing,” Apple said.

Because the library runs on different Apple devices and chips, Apple writes its cryptographic code in portable C to ensure consistent behavior on all platforms. The company said it applies protections against timing attacks and may randomize some internal computations to make attacks harder.

How the verification system works

Formal verification uses mathematical methods to prove that software behaves as intended under defined conditions.

ML-KEM and ML-DSA, post-quantum algorithms standardized by NIST, were selected for their security, performance, compact key and ciphertext sizes, and functional correctness. The implementations were validated through conventional testing, simulation, independent review, and formal verification.

After evaluating existing verification tools and verified implementations, Apple built a custom system that supports multiple programming languages, codebases, and existing developer workflows.

The framework combines existing and newly developed tools to verify the implementations against official FIPS standards. Galois, a research and engineering company specializing in formal verification, collaborated with Apple to develop a tool that generates Isabelle theories from Cryptol models and connects portable C with Cryptol. Apple also developed Isabelle libraries and hand-optimized ARM64 assembly subroutines.

The Cryptol-to-Isabelle translator allows Cryptol models to be recreated in Isabelle for independent analysis.

The verification process identified issues that conventional testing would likely not have detected. One issue involved a missing step in an early ML-DSA implementation that, in rare cases, could cause inputs to exceed the expected range and produce incorrect output. The flaw was identified and fixed before deployment.

“We believe that the strongest assurance possible comes from combining formal verification with conventional methods and critically evaluating the end-to-end results,” the company added.