Microsoft posílá ověřenou kryptografii z Lean důkazů do SymCryptu

Microsoft ukázal metodiku, ve které Rust implementace v SymCryptu ověřuje proti formálním specifikacím v Lean přes toolchain Aeneas. První veřejná větev obsahuje kód, specifikace, vlastnosti a důkazy pro SHA-3 a ML-KEM, přičemž Microsoft uvádí, že tento kód už používají Windows Insider buildy.

SymCrypt dostává důkazy přímo vedle Rust kódu

SymCrypt je open-source kryptografická knihovna Microsoftu používaná mimo jiné ve Windows a Azure Linuxu. Nový blog popisuje cestu od veřejného standardu k Lean specifikaci, od Rust kódu k Lean modelu a nakonec k důkazu, že implementace odpovídá matematickému popisu.

Podstatný detail je, že Microsoft nechce po produktových týmech přepis do speciálního verifikačního jazyka. Inženýři píšou bezpečný Rust, Aeneas z něj vytvoří model v Lean a proof engineers dokazují vztah mezi modelem a specifikací odvozenou ze standardu.

Formální verifikace se snaží vejít do běžného release procesu

Pro kryptografické týmy je to důležitý posun v provozní ekonomice. Testy a audity pořád zůstávají nutné, ale u algoritmů jako ML-KEM nestačí vědět, že implementace prošla sadou vektorů. Důležité je, jestli pro všechny povolené vstupy dělá přesně to, co říká standard, třeba u NTT transformace nad 256 koeficienty v ML-KEM.

Microsoft navíc řeší nepříjemnou část produkce: optimalizace, intrinsics a více architektur. Popisuje modelování cest pro x86-64 a aarch64, včetně SSE2 a Neon, aby verifikace nekončila u čisté referenční verze, kterou stejně nikdo nenasadí.

Agent píše důkaz, ale Lean drží razítko

Nejzajímavější část není samotné použití AI, ale hranice její pravomoci. Agenti můžou pomáhat s překladem standardů do Lean specifikací a s psaním proof scripts, ale výsledek přijme až Lean kernel. Tím se AI práce mění na návrh, který musí projít deterministickou kontrolou.

Slabé místo zůstává ve specifikacích a předpokladech. Pokud člověk špatně formalizuje standard, nebo schová příliš silný předpoklad do theorem statementu, důkaz bude vypadat zeleně a přesto nemusí chránit to, co tým opravdu potřebuje.

Rozhodne, jestli dashboardy udrží krok s měnícím se kódem

Microsoft slibuje developer-facing dashboardy, které ukážou preconditions, postconditions, pokryté funkce, trusted models a zbývající assumptions. To je prakticky důležitější než efektní demo s proof agentem, protože vývojář potřebuje vidět, co přesně je ověřené po změně kódu.

Další signál bude rozsah. SHA-3 a ML-KEM jsou dobrý začátek, ale skutečný test přijde u AES-GCM, FrodoKEM, ML-DSA a optimalizovaných cest, kde se bezpečnostní důkaz potká s tlakem na výkon a údržbu.

Lilithin verdikt

V kryptografii je to jako dát revizní štítek přímo na součástku, kterou už montuje Windows: méně slibů o bezpečnosti, víc kontrolovatelných důkazů.