Microsoft：借助AI智能体和Lean，对SymCrypt中的Rust密码学进行形式化验证

双层保障而非单层

形式化验证是对代码行为完全符合规范的数学证明——不仅仅针对测试的情况，而是针对每一个可能的输入。Microsoft在SymCrypt——支持Windows、Azure和其他产品的基础密码学库——中内置了双重保护：Rust语言消除了整个类别的内存管理相关错误（内存安全漏洞），而Lean证明助手则确认功能正确性——算法完全按照标准要求运行。

Lean是一个通过其可信内核验证数学证明的工具。与覆盖所选场景的单元测试不同，Lean证明涵盖绝对所有可能的输入。这两层的结合使经过验证的代码比传统方法更加强大。

已经验证了什么？

Microsoft发布了SHA-3（广泛使用的哈希算法）和ML-KEM（NIST于2024年标准化的后量子密钥交换算法）的经过验证的代码。ML-KEM尤其重要，因为它被设计为能够抵御量子计算机的攻击，而量子计算机可能会破解目前保护大部分互联网流量的RSA和ECDH。

计划中还有AES-GCM（对称加密）、FrodoKEM和ML-DSA——另外两个后量子算法。所有这些算法的共同点是它们的复杂性和错误的高代价：密码学中的实现缺陷通常不会导致程序崩溃，而是造成可被利用的隐性漏洞。

AI智能体加速证明编写

为密码学代码编写Lean证明既缓慢又费力。Microsoft使用AI智能体来加速这一过程：智能体提出证明建议，然后通过Lean的可信内核独立验证。与普通代码生成的关键区别是AI输出必须通过数学检查——看起来正确是不够的。这意味着AI智能体的错误无法未被发现地通过。

与SymCrypt的集成使这种方法在当今具有实际相关性，而不仅仅是学术实验。Microsoft使用的工具链——Aeneas——将Rust代码转换为Lean可以分析的形式，从而弥合了生产代码和形式化方法之间的差距。