Apple has released quantum-resistant cryptographic code and the mathematical verification tools it developed to prove the code’s correctness, making them publicly available for independent review and broader use across the industry.
The release includes implementations of two quantum-secure algorithms, ML-KEM and ML-DSA, along with the formal verification libraries and tools Apple created to validate their accuracy. The company also published detailed documentation of its verification methodology, which it describes as achieving the strongest known correctness results for any widely deployed production implementation of these algorithms.
The quantum-secure algorithms are integrated into corecrypto, Apple’s cryptographic library used across its operating systems. The library handles encryption, decryption, hashing, and digital signatures on over 2.5 billion active devices. Apple began deploying quantum-resistant encryption in iMessage in 2024 and has expanded the technology to VPN services and TLS networking protocols.
One of the tools released is the company’s Cryptol-to-Isabelle translator, which converts cryptographic models between formal languages, along with supporting libraries needed to reproduce the results. Formal verification uses mathematical proofs to show that code works correctly for all possible inputs. Apple translated its code into Cryptol, a formal language developed by Galois, then into Isabelle, a proof assistant from the University of Cambridge and The Technical University of Munich, to prove both matched the official standards. Apple has used Isabelle previously to verify hardware cryptographic components.
The verification process uncovered errors that conventional testing would have missed. Researchers found a missing computational step in the ML-DSA code that would have silently broken digital signatures. If this bug had reached production, messages in iMessage may have appeared authenticated when they actually weren’t, leaving users unaware their communications lacked proper security.
Even with these tools, Apple acknowledged that it still depends on conventional cryptographic testing and evaluation is needed for assurance. Formal verification can catch errors that traditional testing simply cannot find. Testing works by trying many scenarios, but with complex cryptographic code, there are too many possible inputs to test exhaustively. Subtle bugs can hide in the gaps between test cases and never trigger a warning. Formal verification, by contrast, uses mathematics to prove correctness across all possible inputs at once.
However, Apple’s team writes that it couldn’t formally verify every single aspect of their code with the tools available, so they combined approaches: formal verification for core mathematical correctness, conventional testing for aspects formal methods couldn’t cover, and careful evaluation of how all the pieces work together. Apple argues this hybrid approach provides the most robust security for critical cryptographic software.
“Based on our work to date, we believe that the strongest assurance possible comes from combining formal verification with conventional methods and critically evaluating the end-to-end results,” the blog post reads.
Furthermore, the blog states that Apple selected ML-KEM and ML-DSA from among several standardized quantum-resistant algorithms because they best matched the company’s requirements for security, performance, and compact parameters. The algorithms address the threat posed by future quantum computers, which could potentially break the encryption methods currently protecting digital communications.
More information can be found on Apple’s corecrypto GitHub page.
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。