Microsoft telah membuka sumber sebuah cabang dari pustaka kriptografi SymCrypt-nya yang berisi spesifikasi formal dan bukti untuk implementasi Rust dari ML-KEM dan SHA-3. Rilis ini mendemonstrasikan metodologi di mana algoritma produksi ditulis dalam Rust yang aman dan diverifikasi terhadap model Lean yang berasal dari standar menggunakan toolchain Aeneas.
- Pendekatan ini menggunakan Aeneas untuk menerjemahkan representasi tingkat menengah Rust menjadi model Lean murni, memanfaatkan aturan kepemilikan Rust untuk menyederhanakan penalaran tentang keamanan memori.
- Spesifikasi formal dirancang untuk sangat mencerminkan standar publik seperti NIST atau RFC IETF, memungkinkan pengujian yang dapat dieksekusi terhadap vektor resmi dan tinjauan manusia per baris.
- Cabang yang dibuka sumbernya mencakup bukti lengkap untuk kode ML-KEM dan SHA-3 yang saat ini digunakan dalam build Insider Windows, dengan rencana untuk memperluas alur kerja ini ke AES-GCM, FrodoKEM, dan ML-DSA.
Metodologi ini memberikan dua lapisan jaminan dengan menggabungkan jaminan keamanan memori Rust dengan bukti Lean akan kebenaran fungsional, bertujuan untuk menskalakan verifikasi formal untuk algoritma kriptografi produksi.