Microsoft: formalna verifikacija Rust kriptografije u SymCryptu uz pomoć AI agenata i Leana

Dva sloja garancije umjesto jednog

Formalna verifikacija je matematički dokaz da se kod ponaša točno prema specifikaciji — ne samo za testirane slučajeve, nego za svaki mogući ulaz. Microsoft je u SymCrypt, svoju temeljnu kriptografsku biblioteku koja podržava Windows, Azure i druge proizvode, ugradio dvostruku zaštitu: Rust jezik eliminira cijelu klasu grešaka vezanih uz upravljanje memorijom (memory-safety bugovi), dok Lean dokazni asistent potvrđuje funkcionalnu korektnost — da algoritam radi upravo onako kako standard zahtijeva.

Lean je alat koji provjerava matematičke dokaze kroz vlastiti pouzdani kernel. Za razliku od unit testova koji pokrivaju odabrane scenarije, Lean dokaz pokriva apsolutno sve moguće ulaze. Kombinacija ta dva sloja čini verificirani kod znatno robusnijim od konvencionalnog pristupa.

Što je već verificirano?

Microsoft je objavio verificirani kod za SHA-3, široko korišteni algoritam za hashiranje, i za ML-KEM — post-kvantni algoritam za razmjenu ključeva koji je NIST standardizirao 2024. godine. ML-KEM je posebno važan jer je dizajniran da izdrži napade kvantnih računala, koja bi mogla razbiti RSA i ECDH koji danas štite veliku većinu internetskog prometa.

Na planu su i AES-GCM (simetrična enkripcija), FrodoKEM i ML-DSA — još dva post-kvantna algoritma. Zajednički nazivnik svih tih algoritama je njihova složenost i visoka cijena greške: implementacijski propust u kriptografiji tipično ne uzrokuje pad programa, nego tihu ranjivost koja se može eksploatirati.

AI agenti ubrzavaju pisanje dokaza

Pisanje Lean dokaza za kriptografski kod je sporo i zahtjevno. Microsoft koristi AI agente kako bi ubrzao taj proces: agenti predlažu dokaze koji se zatim neovisno provjeravaju kroz Leanov trusted kernel. Ključna razlika u odnosu na obično generiranje koda jest to da AI izlaz mora proći matematičku provjeru — nije dovoljno da izgleda ispravno. To znači da greške AI agenata ne mogu proći neopaženo.

Integracija u SymCrypt čini taj pristup praktički relevantnim već danas, a ne samo akademskim eksperimentom. Toolchain koji Microsoft koristi — Aeneas — prevodi Rust kod u oblik koji Lean može analizirati, čime se premošćuje jaz između produkcijskog koda i formalnih metoda.