在SymCrypt中验证Rust密码学: 从标准到代码

摘要

微软在SymCrypt中采用Rust、Lean和Aeneas，并借助AI代理，对生产级密码算法进行正式验证。他们证明代码安全正确地实现了标准算法，尤其针对后量子密码。最初发布SHA-3和ML-KEM的验证代码、规范、属性和证明。Aeneas支持验证大部分Rust代码，并在Lean中提供高效自动化；AI代理通过编写可独立验证的证明来扩展自动化。这种方法结合了Rust对内存安全的保证和Lean证明对功能正确性的机器检查，以弥补测试和审计的不足。