Apple corecrypto 形式化验证蓝图

iMessage 中量子安全加密技术的引入标志着重大安全转型的开始，以保​​护 Apple 用户免受未来量子计算机带来的威胁。在所有 Apple 平台上大规模部署新一代算法需要高度保证，因此我们开发了严格的新形式验证方法来证明我们实现的数学正确性。随着本周 corecrypto 的发布，我们将发布量子安全 ML-KEM 和 ML-DSA 算法的实现，以及我们构建的数学证明，以确保它们忠实于 FIPS 203 和 FIPS 204 规范，以供专家进行独立评估。为了进一步推进确保关键软件的最先进技术，我们还发布了我们创建的形式验证库和工具，以便为相关算法的任何广泛部署的生产实现实现最强的已知正确性结果。 2024 年，我们将后量子加密添加到了 corecrypto（Apple 操作系统中的基础加密库）中。为了解决来自未来量子计算机的明显威胁，我们一直致力于首先在可能获得最大利益的领域开发和部署强大的量子安全加密技术：涉及加密通信和其他敏感信息的应用程序，包括 iMessage、VPN 和 TLS 网络。此外，我们去年秋天发布的 Apple CryptoKit 中包含的量子安全 API 使开发人员能够在自己的应用程序中采用量子安全加密和身份验证。 corecrypto 在我们的产品中持续使用，为超过 25 亿台活跃设备提供加密和解密、散列、随机数生成和数字签名。 corecrypto 中的严重错误可能会损害依赖于它的每个应用程序和功能的安全性和可靠性，因此我们在向库添加新代码时很保守，并付出了巨大的努力以全面地进行测试。仅在根据以下标准进行彻底评估后，我们才会在 corecrypto 中包含新的加密算法： 提高安全性。该算法必须解决新问题或提高现有算法的安全性。安全设计。该算法必须具有强大的理论安全性，并且必须能够经受住全球研究界严格、持续的密码分析。实际上，为了我们的预期用途，以安全的方式实现该算法必须是可行的。高性能。执行必须非常高效（无论是在延迟还是功耗方面），就像在每台 Apple 设备上实现的那样。参数紧凑。密钥大小、签名和密文必须最大限度地减少对网络延迟的影响，并符合设备内存限制。当算法满足我们纳入 corecrypto 的高标准时，我们开发的实现必须是：安全。代码必须满足严格的安全标准，并且不得泄露信息。这需要正确性和强化，例如防止泄露定时信号，对手可以利用这些信号来提取应用程序机密。优化了。该实现应最大限度地利用其运行所在芯片的指令和架构。正确的 。代码（包括所有相关优化）必须忠实地实现密码社区分析的标准中定义的算法。它必须产生正确的输出。当我们评估要包含在 corecrypto 中的量子安全算法时，我们很快就找到了两个符合我们标准的算法，这两个算法后来被 NIST 选择并标准化为 ML-KEM 和 ML-DSA（分别为 FIPS 203 和 FIPS 204）。虽然 NIST 还标准化了其他签名方案，但 ML-KEM 和 ML-DSA 最符合我们的要求。加密社区的重要工作已经为 ML-KEM 和 ML-DSA 提供了参考实现，根据我们自己的评估，这些参考实现显示了坚实的安全性和性能基础。由于 corecrypto 广泛用于 Apple 产品（包括具有不同微架构的专用芯片），因此我们首先使用可移植的 C 代码编写算法实现。为了确保在部署 corecrypto 的地方正确、安全地运行实现，我们的指导方针非常严格：我们编写此代码是为了避免通过执行计时泄露秘密值，防止编译器无意中削弱这些保护，并利用 Apple 处理器上的数据独立计时 (DIT) 和指针身份验证 (PAC) 等硬件功能，这些功能分别防范一系列微架构侧通道并针对内存损坏漏洞进行强化。此外，我们还根据特定用途的威胁模型评估随机化内部计算的必要性。在审查了 ML-KEM 和 ML-DSA 设计附带的参考实现后，我们确定了 si