后量子密码｜谷歌计划推出经过形式化验证的NIST后量子算法实现

Formal verification

近日，Google的安全研究团队在其博客上表示，作为后量子密码进展的下一阶段，Google正在与Cryspen合作，生产形式化验证的NIST选定后量子算法的实现。

以下为博客原文——

美国国家标准与技术研究院（NIST）官方发布的后量子密码学（PQC）标准标志着在保护互联网和全球组织免受量子计算威胁方面迈出了重要一步。

在量子计算机大规模存在的情况下，目前用于保护设备上的数据或其在网络中传输的数据的经典公钥密码学算法将变得过时。

Google一直处于后量子发展的前沿，早在2016年便开始实验后量子算法，并于2022年为内部通信提供了后量子保护，最近又将保护范围扩展到Chrome桌面浏览器。

作为后量子密码进展的下一阶段，我们正在与Cryspen合作，生产形式化验证的NIST选定后量子算法的实现。

这些高性能的开源实现将提供有关安全性、功能正确性和内存安全的正式保证，并将供Google及其他用户使用。

实施这些新后量子算法并非易事——这些算法依赖复杂的数学结构，形式化验证是确保新算法代码没有关键实现错误的唯一方式。

项目完成后，Rust语言的后量子密码学算法实现将被纳入libcrux开源库。这些实现将进行AVX2优化，经过F*验证并翻译为C语言。实现将是自包含的，便于集成到其他密码学库中。

后量子密码学的到来

量子计算机的时代对现有密码学构成了威胁：Shor算法的整数因式分解将现代密码学的公钥主力——RSA加密系统和Diffie-Hellman密钥交换——置于危险之中。

虽然量子计算机目前尚不能破解这些方案，但对加密数据的存储与未来解密的能力使得保护数据免受量子计算机威胁成为紧迫任务。

幸运的是，NIST自2016年起便开始对PQC算法进行标准化，近期的成果已得到三个批准的方案：ML-KEM、ML-DSA和SL-DSA。这些方案明确推动密码学向PQC过渡。

鉴于历史上过渡期较长的先例，采取主动措施以确保数字基础设施的安全以及从一开始就采用安全且无错误的PQC实现至关重要。

为什么形式化验证很重要？

与传统测试不同，形式化验证提供了对密码学实现正确性的数学证明，适用于所有输入，包括意外和恶意输入。这通过在开发过程中早期发现潜在漏洞，确保了更高的安全性和可靠性。

认识到形式化验证的价值，一些密码学库（如BoringSSL和NSS）已开始集成形式化验证的密码学原语实现，从而实现了更安全、更高效的实现。

形式化验证允许在不担心引入错误的情况下进行优化——每个可能的优化都经过形式化验证，这一安全网的存在使得进一步优化成为可能。

Cryspen与Google的PQC合作始于对ML-KEM的验证。虽然像ML-KEM和ML-DSA这样的基于格的算法可能看起来比传统的非对称密码学更简单，但它们的并行化特性带来了独特的挑战。

这种复杂性使得通过传统测试难以识别潜在错误。在验证过程中，Cryspen发现了ML-KEM参考实现中的一个定时侧信道漏洞，这一漏洞连算法设计者也未曾察觉。

此漏洞及其变体（有时称为KyberSlash）随后在多个Kyber实现中被发现。形式化验证PQC算法将捕捉到这些错误，从而部署高度安全、高度优化的代码。

未来的道路

我们正在积极将最新的ML-KEM和ML-DSA规范更新整合到我们的实现中。一旦验证完成，我们计划将实现发布为Rust crate，并提取C代码，方便集成到其他密码学库中。

接下来，我们将专注于其他NIST规范，最终目标是开发出生产就绪、形式化验证的PQC实现，不仅供Google等组织使用，还能为需要迎接即将到来的PQC过渡的各方提供支持。

组织如何为PQC迁移做好准备？

针对组织如何为PQC迁移做好准备，Google在其另一篇安全博客文章中给出了建议：

以下是一些可以随时实施的加密敏捷性最佳实践：

★加密清单

了解组织在何处以及如何使用加密技术，包括掌握当前使用的加密算法，并确保密钥材料的安全管理。

★密钥轮换

密钥轮换任何新的加密系统都需要能够生成新密钥并将其移至生产环境而不会导致中断。就像测试从备份中恢复一样，定期测试密钥轮换应该是任何良好弹性计划的一部分。

★抽象层

使用像Tink这样的工具（这是Google提供的多语言、跨平台开源库），可以让非专业人士轻松、安全地使用加密技术，并在不需要大量代码重构的情况下在不同的加密算法之间切换。

★端到端测试

后量子密码学算法具有不同的属性。例如，公钥、密文和签名通常更大。确保所有层的堆栈按预期运行非常重要。