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

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提供的多语言、跨平台开源库），可以让非专业人士轻松、安全地使用加密技术，并在不需要大量代码重构的情况下在不同的加密算法之间切换。

★端到端测试

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

（博客原文🔗：https://bughunters.google.com/blog/6038863069184000/formally-verified-post-quantum-algorithms） 

(文章来源：公钥密码开放社区)