苹果公司发布了经过形式化验证的corecrypto加密库，包含量子安全的ML-KEM和ML-DSA算法实现。为确保算法正确性，苹果开发了严格的形式化验证方法，并公开了验证工具库和数学证明，供专家独立评估。这是首个大规模部署的量子安全加密实现，符合FIPS 203/204标准。

苹果核心加密库形式化验证蓝图 - 苹果安全研究

由苹果安全工程与架构(SEAR)及硬件技术形式化验证团队联合撰写

随着iMessage量子安全加密技术的推出，苹果开启了重大安全转型，以保护用户免受未来量子计算机的威胁。为确保新一代算法在苹果全平台的安全部署，我们开发了严格的形式化验证方法，通过数学证明确保算法实现的正确性。本次发布的corecrypto库包含量子安全算法ML-KEM和ML-DSA的实现，以及符合FIPS 203和FIPS 204标准的数学证明，供专家独立评审。同时，我们开源了形式化验证工具库，为关键软件验证树立了新标杆。

核心验证技术 corecrypto作为苹果操作系统的基础加密库，为超过25亿台活跃设备提供加密、哈希、随机数生成和数字签名服务。我们采用以下严格标准评估新算法： 1. 安全性提升：必须解决新安全问题或提升现有算法安全性 2. 设计可靠：需具备强大理论安全性，并经受全球密码学界持续验证 3. 高性能：在所有苹果设备上实现低延迟和低功耗 4. 参数精简：密钥和签名大小需优化网络传输和内存占用

实现要求包括： - 安全性：防止信息泄露，抵御时序攻击 - 优化：充分利用苹果芯片指令集 - 正确性：严格符合密码学界验证的标准

形式化验证方法 我们采用数学证明确保算法实现的正确性，远超传统测试的验证强度。验证过程包括： 1. 将C语言实现转化为Cryptol形式化语言 2. 使用SAW工具验证Cryptol模型与实现的一致性 3. 通过定制工具将Cryptol模型转换为Isabelle语言 4. 在Isabelle中完成5万多个证明步骤，建立算法规范与实现的数学等价性 5. 对ARM64汇编优化进行专项验证

验证成果 形式化验证发现了传统测试难以检测的深层问题，包括： - ML-DSA实现中罕见的输入范围越界错误 - 第三方证明中的特定参数错误 我们开源的验证资源包括： - 技术白皮书详细说明验证方法 - Cryptol-to-Isabelle转换工具 - Isabelle理论库和验证框架

这种定制化验证方法为ML-KEM和ML-DSA的大规模生产部署提供了最高级别的正确性保证，同时支持持续优化演进。通过结合形式化验证与传统测试，我们为关键加密软件树立了新的安全保障标准。

（注：原文中关于量子安全算法部署时间线、具体优化技术细节、工具链协作流程等次要内容已做精简，保留核心验证方法论和关键技术成果）

总结评论内容：

1. 关于SAW工具的优势：

• 认为SAW能有效发现ML-DSA中的隐蔽代码缺陷（"rare inputs that pass code review"）
• 相比其他形式化验证工具更易用（"amazingly easy to use compared to other formal methods tools"）

2. 关于编程语言安全性的讨论：

• 批评C++在高安全领域的使用（"C++ is still popular in high assurance spaces...the ability to write safe code is so much worse"）
• 认为C语言在当前更具安全性优势

3. 关于苹果安全措施的批评：

• 指责苹果忽视解析器安全问题（"apple still doesnt take parser security seriously enough"）
• 指出苹果用"锁定模式"替代根本修复（"offer lockdown mode instead of fixing it"）

4. 关于后量子加密的积极评价：

• 肯定苹果2024年就部署后量子加密（"great to see 'crypto' to mean cryptography"）
• 特别提到ML-KEM和ML-DSA标准（"FIPS 203 and FIPS 204"）

注：所有评论均未显示评分（None），故无法评估认可度。不同观点保持平衡呈现，引用保留了中英文关键内容。