苹果发布 corecrypto：用量子安全算法与形式验证保障超 25 亿设备安全！

苹果开启安全变革发布 corecrypto苹果安全工程与架构团队SEAR以及硬件技术形式验证团队撰写相关内容。苹果通过在 iMessage 中引入量子安全加密技术开启重大安全变革旨在保护用户免受未来量子计算机威胁。为大规模部署新一代算法开发了严格的新型形式验证方法以证明实现方案数学上的正确性。随着本周 corecrypto 的发布公布了量子安全的 ML - KEM 和 ML - DSA 算法实现方案及数学证明还公布了形式验证库和工具。后量子加密技术融入苹果系统2024 年后量子加密技术被添加到苹果操作系统基础加密库 corecrypto 中。苹果努力在加密通信等领域开发和部署量子安全加密技术Apple CryptoKit 包含的量子安全 API 让开发者可采用相关技术。corecrypto 为超 25 亿台活跃设备提供加密等功能添加新代码时非常谨慎。纳入 corecrypto 的算法标准苹果仅在新加密算法符合提升安全性、设计安全、高性能、参数精简标准后才会将其纳入 corecrypto。当算法达到标准实现方案需满足安全、优化、正确的要求。评估后确定 ML - KEM 和 ML - DSA 符合标准且最符合苹果要求。算法实现的严格要求与优化因 corecrypto 广泛使用先使用可移植 C 代码编写算法实现。编写代码时避免泄露秘密值防范侧信道攻击和内存损坏漏洞还会评估是否对内部计算随机化。审查参考实现后应用数学优化方法提高性能手动优化有助于防止时序侧信道攻击。形式验证的挑战与要求引入复杂算法实现方案是艰巨任务且 ML - KEM 和 ML - DSA 数学理论较新行业经验少。苹果设定高验证门槛结合传统测试和严格形式验证。形式验证用数学证明系统或对象满足特定属性苹果在芯片开发中进行形式验证超 15 年2019 年开始用于证明经典密码学正确性。corecrypto 形式验证的关键要求形式验证虽能证明子例程输出正确但单独验证不够。苹果确定了 corecrypto 形式验证的关键要求能够验证整个算法实现方案支持用可移植 C 语言和 ARM64 汇编语言编写的算法实现方案支持快速迭代减少保持正确性证明有效的工作量与现有开发工具兼容。corecrypto 的定制方法评估许多验证工具后大多数不符合要求最终设计了定制的形式验证方法。将已有工具与新工具结合进行端到端证明。使用的开源工具包括 Isabelle、软件分析工作台SAW、Cryptol、cryptol - to - Isabelle。通过一系列步骤证明 C 实现方案与算法规范等价最后验证 ARM64 汇编语言编写的子例程。示例C 实现与 Isabelle 规范的差异以一个 C 语言子例程为例展示了其与对应的 Isabelle 规范的差异。C 子例程通过循环相加多项式系数而 Isabelle 规范更抽象使用内置操作处理系数。形式验证的成果与局限性形式验证发现了传统测试无法发现的问题让苹果有信心相信实现方案正确。但形式验证存在局限性如假设编译器行为正确SAW 无法验证 ML - DSA 的所有可能消息大小。不过苹果认为结合形式验证与传统方法严格评估端到端结果能获得最强可靠性保证。成果发布与意义2026 年 5 月 22 日corecrypto 源代码发布苹果分享了形式验证进展、方法细节和工具。相关论文详细阐述技术细节提供评估结果、理解或扩展工具和理论的信息。定制形式验证方法为 ML - KEM 和 ML - DSA 实现方案提供高功能正确性保证支持手动优化代码。那么这种方法未来能否在更多领域发挥更大作用呢