A Microsoft abriu o código-fonte de um branch de sua biblioteca criptográfica SymCrypt contendo especificações formais e provas para as implementações em Rust de ML-KEM e SHA-3. Este lançamento demonstra uma metodologia onde algoritmos de produção são escritos em Rust seguro e verificados contra modelos Lean derivados de padrões usando a toolchain Aeneas.
- A abordagem usa o Aeneas para traduzir a representação de nível médio do Rust em modelos Lean puros, aproveitando as regras de propriedade do Rust para simplificar o raciocínio sobre segurança de memória.
- As especificações formais são projetadas para espelhar de perto padrões públicos como NIST ou RFCs da IETF, permitindo testes executáveis contra vetores oficiais e revisão humana linha por linha.
- O branch aberto inclui provas completas para o código de ML-KEM e SHA-3 atualmente usado em builds insider do Windows, com planos para estender este fluxo de trabalho para AES-GCM, FrodoKEM e ML-DSA.
Esta metodologia fornece duas camadas de garantia ao combinar as garantias de segurança de memória do Rust com provas Lean de correção funcional, visando escalar a verificação formal para algoritmos criptográficos de produção.