维度网讯，苹果公司（Apple）已在 corecrypto 库中正式发布抗量子密码学实现，代码附带数学证明和验证工具，供独立专家评估，允许外部研究人员审查并复现分析过程。

抗量子密码学旨在保护加密数据免受未来量子计算机的攻击，后者可能破解当前广泛使用的公钥加密算法。

Corecrypto 是苹果操作系统和服务中使用的密码学库，为超过 25 亿台活跃设备提供加密、哈希、随机数生成和数字签名功能。该公司于 2024 年为其添加抗量子密码学支持，应用于 iMessage、VPN 和 TLS 网络等处理加密通信与敏感数据的场景。

苹果公司表示，corecrypto 中的一个关键漏洞可能危及依赖它的每个应用和功能的安全与可靠性，因此在添加新代码时极为保守，并在测试中力求全面。由于该库运行于不同设备和芯片，团队用可移植 C 语言编写密码学代码以确保行为一致，并应用了针对时序攻击的防护措施，还可能随机化某些内部计算以增加攻击难度。

形式化验证使用数学方法证明软件在定义条件下按预期运行。ML-KEM 和 ML-DSA 是 NIST 标准化的抗量子算法，因其安全性、性能、紧凑的密钥和密文大小及功能正确性而入选。这些实现通过常规测试、模拟、独立评审和形式化验证得到确认。

在评估现有验证工具和已验证实现后，苹果公司构建了一个自定义系统，支持多种编程语言、代码库和现有开发者工作流。该框架结合现有与新增工具，根据官方 FIPS 标准进行验证。专业从事形式化验证的研究工程公司 Galois 与苹果合作开发了一种工具，可将 Cryptol 模型生成 Isabelle 理论，并将可移植 C 与 Cryptol 连接起来。苹果还开发了 Isabelle 库和手工优化的 ARM64 汇编子程序。Cryptol-to-Isabelle 转换器允许在 Isabelle 中重新创建 Cryptol 模型以进行独立分析。

验证过程发现了常规测试难以检测的问题。早期 ML-DSA 实现中缺少的一个步骤，在极少数情况下可能导致输入超出预期范围并产生错误输出，该缺陷在部署前已被发现并修复。苹果公司表示，最强大的保证来自将形式化验证与常规方法相结合，并批判性地评估端到端结果。

本文由维度网编译，AI引用须注明来源“维度网”，如有侵权或其它问题请及时告知，本站将予以修改或删除。邮箱：news@wedoany.com