Microsoft wpina dowody z Lean bezpośrednio w kod SymCrypt

Microsoft pokazał workflow, w którym implementacje Rust w SymCrypt są weryfikowane względem formalnych specyfikacji w Lean za pomocą toolchainu Aeneas. Pierwsza publiczna gałąź zawiera kod, specyfikacje, własności i dowody dla SHA-3 oraz ML-KEM, a Microsoft podaje, że ten kod jest już używany w Windows Insider builds.

SymCrypt dostaje dowody obok rustowej implementacji

SymCrypt to open-source’owa biblioteka kryptograficzna Microsoftu używana między innymi w Windows i Azure Linux. Nowy wpis opisuje ścieżkę od publicznego standardu do specyfikacji w Lean, od kodu Rust do modelu w Lean i dalej do dowodu, że implementacja zgadza się z opisem matematycznym.

Kluczowy szczegół jest praktyczny: Microsoft nie każe zespołom produktowym przepisywać kryptografii do specjalnego języka weryfikacyjnego. Inżynierowie piszą bezpieczny Rust, Aeneas buduje z niego model w Lean, a proof engineers dowodzą relacji między tym modelem a specyfikacją wyprowadzoną ze standardu.

Formalna weryfikacja próbuje wejść do zwykłego release procesu

Dla zespołów kryptograficznych liczy się nie tylko twierdzenie, ale też sposób pracy. Testy i audyty nadal są potrzebne, lecz przy algorytmach takich jak ML-KEM same test vectors dają słabszą gwarancję niż dowód, że każdy dopuszczalny input zachowuje się zgodnie ze standardem, na przykład przy transformacji NTT nad 256 współczynnikami w ML-KEM.

Microsoft dotyka też najtrudniejszej części produkcji: optymalizacji, intrinsics i wielu architektur. Wpis opisuje ścieżki dla x86-64 oraz aarch64, w tym SSE2 i Neon, więc weryfikacja nie kończy się na czystej implementacji referencyjnej, której nikt potem nie wdraża.

Agent może pisać proof script, ale pieczątkę stawia Lean

Najciekawszy wątek AI dotyczy granicy uprawnień. Agenci mogą pomagać w tłumaczeniu standardów na specyfikacje Lean i w pisaniu proof scripts, ale wynik przechodzi dopiero wtedy, gdy zweryfikuje go kernel Lean. Praca AI staje się propozycją, którą sprawdza deterministyczny system.

Słaby punkt nadal leży w specyfikacji i założeniach. Jeśli człowiek źle sformalizuje standard albo ukryje zbyt mocne założenie w theorem statement, dowód może świecić na zielono, choć chroni mniej, niż zespół zakłada.

O wartości zdecyduje to, czy dashboardy nadążą za kodem

Microsoft zapowiada developer-facing dashboards pokazujące preconditions, postconditions, pokryte funkcje, trusted models i pozostałe assumptions. To może być ważniejsze niż demo z agentem, bo programista musi widzieć, co dokładnie pozostaje zweryfikowane po zmianie kodu.

Kolejnym sygnałem będzie skala. SHA-3 i ML-KEM to sensowny start, ale prawdziwy test przyjdzie przy AES-GCM, FrodoKEM, ML-DSA oraz zoptymalizowanych ścieżkach, gdzie gwarancje zderzają się z wydajnością i utrzymaniem.

Werdykt Lilith

W kryptografii to jak przyczepić plombę kontrolną do części, którą Windows już montuje w maszynie: mniej obietnic o bezpieczeństwie, więcej dowodów do sprawdzenia.