科技媒体 9to5Mac 于5月22日发布独家报道，披露苹果公司已在 GitHub 平台正式开源其核心加密库 corecrypto 的代码仓库，并同步发布深度技术解析文章，全面揭秘了后量子密码学技术是如何深度集成到 iPhone、Mac 等全系苹果设备中的。
这一举措标志着苹果在2024年公布的后量子密码学战略路线图上迈出了关键一步。为应对未来量子计算机可能带来的严峻安全挑战，苹果此前已在 iOS 17.4 系统中为 iMessage 引入了全新的 PQ3 加密协议，该协议在会话建立及后续的周期性密钥更新过程中，均提供了符合后量子安全标准的强大保护。
本次开源的核心是位于 GitHub 的 corecrypto 项目。作为苹果设备加密体系的基石，这个底层加密库为 Security framework、CryptoKit 以及 CommonCrypto 等高级框架提供关键支撑，负责执行加密解密、哈希运算、安全随机数生成以及数字签名等核心密码学功能。
开源仓库内容极为详实，不仅包含了完整的核心源代码，还提供了苹果官方选定的两种后量子密码算法（PQC）的具体实现：ML-KEM（模块化格密钥封装机制）和 ML-DSA（模块化格数字签名算法）。此外，相关的完整测试套件、性能基准分析工具以及多平台构建目标也全部公开。尤为引人注目的是，苹果专门设立了一个用于形式化验证的独立目录。
该验证目录中存放了严谨的数学证明材料和配套自动化工具，旨在严格验证苹果的算法实现是否完全符合美国国家标准与技术研究院（NIST）的 FIPS 203 与 FIPS 204 标准。具体而言，FIPS 203 标准对应 ML-KEM 算法，主要用于实现安全的密钥协商与封装；而 FIPS 204 标准对应 ML-DSA 算法，则专用于生成抗量子攻击的数字签名。
苹果在技术文章中强调，这套先进的形式化验证流程并非用于取代传统的软件测试方法，而是作为一种强有力的增强与补充。通过将常规测试、硬件模拟、独立第三方安全审计与数学形式化验证多层叠加，苹果构建起一道更为纵深和坚固的终端安全防御体系。
除了核心代码库，苹果还开源了配套的完整技术文档，包括题为《Formal verification for Apple corecrypto》的学术论文、用于将 Cryptol 规范转换为 Isabelle 理论的专用工具链，以及源码包中附带的 Isabelle 理论文件。这些资源为全球密码学和安全研究社区提供了宝贵的学习与参考材料。
相关资源
- The corecrypto (cc) project
- A blueprint for formal verification of Apple corecrypto
