报道指出苹果在 GitHub 发布了 corecrypto 底层加密库与配套技术文档，公开了其后量子密码学实现（包括 ML-KEM 与 ML-DSA）以及测试、性能工具、构建目标和专门的形式化验证目录。该验证目录含证明材料与工具（如 Cryptol-to-Isabelle 转换器与 Isabelle 理论文件），用于检验实现对 FIPS 203（KEM）和 FIPS 204（DSA）要求的符合性。此举延续苹果在 2024 年推动的后量子路线，旨在将后量子保护逐步落地到 iPhone、Mac 等产品（例如 iOS 17.4 在 iMessage 中引入的 PQ3 协议）。
5 月 23 日消息，科技媒体 9to5Mac 昨日（5 月 22 日）发布博文，报道称苹果公司在 GitHub 公布 corecrypto 代码仓库，并配套发布技术长文，集中说明其后量子密码学工作如何落地到 iPhone、Mac 等产品。
本次更新延续苹果公司在 2024 年公开推进的后量子密码学路线。在 iOS 17.4 系统中，苹果为应对未来量子计算机可能带来的破解风险，在 iMessage 上线 PQ3 协议，开始在会话建立和后续密钥刷新阶段加入后量子保护。
Apple 后量子密码方案示意图
在本次更新中，苹果在 GitHub 上发布 corecrypto 代码仓库，该项目是个底层加密库，供 Security framework、CryptoKit 和 CommonCrypto 调用，负责加密、哈希、随机数生成和数字签名等能力。
仓库中除了源代码，还包含 ML-KEM 和 ML-DSA，两者是苹果公司为 corecrypto 选用的后量子算法。同时，苹果还放出了测试、性能工具、构建目标，以及专门的形式化验证目录。
这个验证目录包含证明材料和配套工具，用来检查其实现是否符合 FIPS 203 与 FIPS 204 标准。前者对应 ML-KEM，主要用于安全建立加密密钥；后者对应 ML-DSA，主要用于数字签名。
苹果强调，这套流程不是普通测试的替代品，而是把常规测试、模拟、独立审查和形式化验证叠加使用。
除了代码库外，相关支持材料还包括《Formal verification for Apple corecrypto》论文、Cryptol-to-Isabelle 转换工具，以及源码包中的 Isabelle 理论文件。
IT之家附上参考地址
- The corecrypto (cc) project
- A blueprint for formal verification of Apple corecrypto