Apple（苹果公司）于2026年5月22日正式开源其corecrypto密码库中的后量子密码算法实现，包括美国国家标准与技术研究院（NIST）选定的两套标准化算法ML-KEM（FIPS 203）和ML-DSA（FIPS 204）的落地代码，以及整套形式化验证工具链和Isabelle理论库。本次开源不仅落地NIST标准化后量子密码成果，还完整公开了一套从底层汇编代码到国标规范闭环核验的数学验证工程方案，尽管形式化验证和结论有效性受限于规约的正确性、可信计算基、随机数生成器等验证范围完整性，以及组合安全性、长期证明维护的可持续性等问题，但仍不失在后量子密码安全验证领域具备重要参考价值。

本期简报整合苹果公司官方发布资料与其他公开信息的分析内容，从项目落地背景、算法选型逻辑、形式化验证技术架构、实际落地成效与开源行业价值等维度梳理相关信息，为后量子密码落地实现提供参考。

一、苹果公司corecrypto后量子密码集成总体布局

为应对未来量子计算机带来的加密破解威胁，苹果公司启动了系统性的安全转型工作，在全平台部署量子安全密码体系，全方位保护用户隐私通信安全。2024年，苹果公司正式将后量子加密能力集成至系统底层基础密码库corecrypto，优先在iMessage、TLS网络传输等加密通信场景落地应用。

作为苹果公司全操作系统通用的基础密码组件，corecrypto承载着设备加解密、哈希运算、随机数生成、数字签名等密码功能，覆盖超25亿台全球活跃设备。由于库内代码漏洞会连锁影响所有依赖该组件的应用与服务安全性，苹果公司对corecrypto新增代码秉持极高的审慎性，针对后量子密码新代码投入了大量资源开展全方位测试校验。

二、corecrypto库的密码算法入选标准

新密码算法只有在经过以下标准的全面评估后才会被纳入corecrypto：

1. 增强安全性：算法必须解决新问题或改进现有算法的安全性。

2. 安全设计：算法必须具备强大的理论安全性，并且经受了全球研究社区严格、持续的密码分析。在实践中，必须能够以安全的方式实现该算法以满足预期用途。

3. 高性能：在所有苹果设备上的执行必须高效——包括延迟和功耗两个方面。

4. 紧凑参数：密钥大小、签名和密文必须最小化对网络延迟的影响，并适应设备内存限制。

当算法达到纳入corecrypto的高标准后，开发实现还必须满足以下要求：

1. 安全：代码必须满足严格的安全标准，不能泄露信息。这既需要正确性，也需要加固措施，例如防止泄露攻击者可用来提取应用密钥的时序信号。

2. 优化：实现应最大限度利用所运行硅片的指令集和架构优势。

3. 正确：包括所有相关优化在内的代码必须忠实实现密码学社区分析过的标准中定义的算法，必须产生正确的输出。

三、ML-KEM与ML-DSA算法选型及工程优化实践

在评估纳入corecrypto的量子安全算法时，苹果公司聚焦于两个满足标准的算法，即被NIST选定并标准化为ML-KEM和ML-DSA的算法（分别为FIPS 203和FIPS 204）。选择这两个算法的关键原因在于它们在安全性、性能和紧凑参数方面最能匹配苹果公司的严格要求。

在审查ML-KEM和ML-DSA设计的参考实现后，苹果公司应用数学优化，在不改变底层算法的情况下提高性能，并重写对性能和安全性最敏感的子程序。这些手工优化的路径能够精确控制处理器行为，帮助防止可能向攻击者暴露秘密的时序侧信道。

苹果公司的首要任务是确保新算法实现在功能上正确且安全。为实现这一目标，苹果公司设定了极高的合格门槛，包括深入的常规测试、仿真和独立审查，并将其与严格的形式化验证相结合。

（一）形式化验证需求

形式化验证使用数学证明来展示一个系统或对象满足苹果公司定义的特定属性。对于corecrypto，苹果公司使用数学证明来展示算法实现的正确性，其保障程度远超传统软件测试所能达到的水平。测试通过尝试大量场景来工作，但对于复杂的密码代码，可能的输入组合太多，无法穷尽测试。构造精妙的漏洞可能隐藏在测试用例之间的间隙中而从不触发警告。相比之下，形式化验证使用数学一次性证明所有可能输入的正确性。

通过分析如何将ML-KEM和ML-DSA的形式化验证与苹果公司现有工程流程最佳结合，苹果公司制定了corecrypto形式化验证的关键要求：

1. 能够验证整个算法实现，包括高级数学公式，证明每个子程序和整个序列的正确性。

2. 支持可移植C语言和ARM64汇编两种实现语言。

3. 支持快速演进，最小化保持证明有效的工作量，兼容现有开发者工具。

（二）定制化验证方案

为满足独特需求（多语言支持、快速代码演进和现有开发者工具兼容），苹果公司设计了一套定制化的形式化验证方法，将已使用的工具与新的工具结合，执行从最终实现回溯到FIPS规范的端到端证明。

关键开源工具包括：

• Isabelle：形式化语言和证明助手，可验证复杂数学证明。苹果公司已用于验证硬件PKA。

• Software Analysis Workbench（SAW）：由Galois开发，对照Cryptol规范验证软件程序属性。

• Cryptol：与SAW配合的形式化语言，也由Galois开发。

• cryptol-to-isabelle：Galois按苹果公司公司规范构建的翻译器，将Cryptol模型转为Isabelle公式（注：这是此次公开发布的关键工具之一，连同支持库一起公开，使外部研究人员能够重现苹果公司公司的验证结果）。

（三）验证成果

整套验证体系搭建了Cryptol-SAW-cryptol/to/isabelle-Isabelle四段式核验流程，依托超50000步数学证明，建立了从手写ARM64汇编到FIPS规范的完整正确性链条。在验证落地过程中，这套数学化验证方案捕捉到传统功能测试难以排查的隐性代码缺陷，包括：

1.ML-DSA早期实现中发现了一个缺失的计算步骤，在极少数情况下可能导致输入超出预期范围并产生错误输出。如果此漏洞进入生产环境，iMessage中的消息可能表面上显示已认证，但实际上并未经过正确的安全保护，用户将无法察觉其通信缺乏适当的安全性。

2.发现并独立修复了一个第三方证明中的错误。形式化验证是一个不断发展的领域，所选方法在所覆盖的属性和假设方面有自然的权衡和限制。

结合本次工程实践，苹果官方明确技术观点：现阶段密码软件实现高安全等级防护最强有力的保障来自于形式化验证与常规方法的结合，以及对端到端结果的严格评估。

四、开源发布与社区影响

苹果公司发布的corecrypto源代码包含以下可公开获取的资源：

• 《corecrypto形式化验证》技术论文（GitHub）

• Cryptol-to-Isabelle翻译器（Galois SAW v1.5.1）

• Isabelle理论库——包括ARM64模型、精化框架、SProp分离代数库、背景引理和FIPS形式化

• 部分理论以受限评估许可发布，其他以更宽松许可发布供公共使用。

本次开源具备行业里程碑意义。从技术层面，该定制化验证方案实现了当前量产级ML-KEM、ML-DSA算法的最高等级正确性保障，可适配人工优化代码迭代升级，大幅降低后续算法优化的验证成本。从行业层面，苹果公司不仅公开了生产级后量子密码实现代码，更完整开放了可复现、可落地的全链路形式化验证工程体系。当前，形式化验证结合传统测试的混合核验模式，已逐步成为密码软件安全审计、合规落地的全新行业范式，为全球科技企业推进后量子密码规模化安全部署提供了参考范例。

编译：祝媛

审核：原浩 朱莉欣 方婷

完

作者编译观点仅代表个人

不代表密码法治实践创新基地

为方便排版，已略去脚注

声明：本文来自苏州信息安全法学所，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。