近日，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）已开始集成形式化验证的密码学原语实现，从而实现了更安全、更高效的实现。