Apple称，此前常规测试未能排查出新型抗量子计算机攻击加密方案内存在的缺陷。因此在大范围推行该代码前，Apple借助数学证明方式核验代码运行的可靠性。

5月22日发布的最新研究论文及源代码，详述了Apple对部分后量子密码体系的核验过程。该研究提出，传统软件测试固然可行，但已无法为超25亿台在用设备所搭载的加密系统提供足够安全保障。

本次研究工作围绕corecrypto开展，是Apple底层密码函数库，应用于iPhone、iPad、Mac等全品类设备。由于未来量子计算机或将破解当下多数公钥加密体系，Apple启动了此项研发工作。

各大科技企业都在争相更替老旧加密方式，防止量子计算机实现实用化后遭到破解。

Apple自研一套形式化验证体系，对照美国国家标准与技术研究院（NIST）官方规范，核验自家后量子加密程序。依托数学证明，证实Apple编写的ML-KEM、ML-DSA代码符合对应算法行业标准。

iMessage现已搭载后量子防护技术。Apple还计划将该技术拓展至虚拟专用网络、TLS网络传输以及面向开发者的CryptoKit应用程序接口。

抗量子加密技术正逐步成为Apple安全架构的核心基础组件。安全框架、CryptoKit、CommonCrypto均依托corecrypto，这也让该函数库在Apple全系设备以及开发者工具中占据关键地位。

形式化验证工作发现了开发阶段常规测试未能察觉的缺陷。研发人员在早期ML-DSA程序中发现一处步骤缺失问题，该问题在极少数情形下会致使加密运算结果出错。

本次研究还排查并修复了项目中引用的第三方验证程序存在的一处错误。

该步骤缺失问题会在无任何提示的情况下篡改加密运算数据，现有测试程序无法察觉。加密程序漏洞往往不会造成闪退、弹窗报错等直观故障，却会削弱加密防护能力。

corecrypto支撑苹果全平台的加密运算、哈希算法、数字签名、随机数生成等功能。一旦该函数库出现高危漏洞，几乎所有依托Apple安全框架的应用与服务都会受到牵连。

相较于传统公钥加密体系，后量子加密在程序编写环节存在特殊风险。ML-KEM与ML-DSA算法依托海量多项式运算以及多层复杂数学运算，极易产生细微的进位、借位运算差错。

论文提及，行业对于新式后量子算法的实操经验，远少于成熟的椭圆曲线加密算法。早年椭圆曲线加密落地时，也曾因细微编写缺陷衍生出可被利用的安全漏洞。

Apple并未局限于简易学术模型，而是对适配Apple芯片的正式优化代码开展核验。形式化证明覆盖通用C语言版本代码，以及为提升运行效率、规避时序信息泄露而人工优化的ARM64汇编程序。

Apple通过形式化证明，证实通用C语言与ARM64汇编编写的ML-KEM、ML-DSA抗量子代码均契合官方规范。

后量子加密大幅提升了代码编写复杂度，高度精简的运算流程也扩大了受攻击范围。Apple同步运用Apple芯片内置安全机制，包含数据独立时序防护(DIT)、指针认证(PAC)，以此降低相关安全隐患。

DIT能够规避时序侧信道信息泄露，PAC可抵御特定内存破坏类攻击。研发人员还重写关键加密程序，精准管控加密运算过程中的处理器运行行为。

Apple整合Isabelle、SAW、Cryptol多款工具，并与安全企业Galois合作研发全新Cryptol转Isabelle翻译程序，打造专属验证工作链路。该验证流程会将程序代码转化为严谨的数学模型。

整套核验工作累计完成五万余步独立数学证明。Apple随同论文一并对外发布更新后的corecrypto源代码以及多款形式化验证工具。

公开资料包含Isabelle程序库、验证架构、ARM64运算模型，以及研发阶段所用的Cryptol转Isabelle转换工具。

形式化验证并非能够彻底解决全部加密安全隐患。苹果坦言，整套核验工作建立在编译器无误的前提之上，受工具局限，部分ML-DSA环节依旧沿用传统测试方式核验。

随着后量子加密技术在全球商用体系普及，数学核验愈发关键。Apple选择借助形式化数学证明完成后量子加密技术校验，再逐步推广至旗下各类设备。