A Microsoft formálisan ellenőrzi a Rustban írt kriptográfiai kódot
A Microsoft Research nyilvánosságra hozta a SymCrypt kriptográfiai könyvtár Rustban írt algoritmusainak formális ellenőrzéséhez használt specifikációkat és bizonyításokat. Az első kiadás az SHA-3 és az ML-KEM teljes bizonyítását tartalmazza.
- A Microsoft Research a SymCrypt Rust-kódját Lean és Aeneas segítségével ellenőrzi.
- Az első nyilvános kiadás SHA-3 és ML-KEM teljes bizonyításait tartalmazza.
- A formalizált specifikációk a szabványok szerkezetét követik és tesztvektorokkal futtathatók.
- A folyamatot AES-GCM-re, FrodoKEM-re és ML-DSA-ra is kiterjesztik.
- AI-ügynökök írhatnak bizonyításokat, amelyeket determinisztikus eszközök ellenőriznek.
Géppel ellenőrzött bizonyítás a kriptográfiai kód mögött
A Microsoft Research 2026. július 13-án ismertette, hogyan használja a Rust, a Lean, az Aeneas és az AI-ügynökök kombinációját a gyártásban használt kriptográfiai algoritmusok formális ellenőrzésének kiterjesztésére. A cél annak bizonyítása, hogy a kód biztonságosan és helyesen valósítja meg a szabványokban leírt algoritmusokat, különös tekintettel a kvantum utáni kriptográfiára.
A kriptográfiai kód operációs rendszerek, felhőszolgáltatások, firmware-ek, üzenetküldő rendszerek és kommunikációs protokollok alapvető része. Egyetlen számtani hiba, hiányzó határellenőrzés vagy hibás állapotváltás is veszélyeztetheti egy egyébként megfelelően megtervezett rendszer biztonságát. A tesztelés és a kódátvizsgálás továbbra is fontos, de a Microsoft szerint önmagában egyik módszer sem elegendő.
A formális ellenőrzés géppel vizsgálható bizonyításokat használ. Ezek nem csak azt ellenőrzik, hogy a program a tesztekben szereplő esetekben megfelelően működik, hanem egy matematikai specifikáció alapján minden, előfeltételeknek megfelelő bemenetre bizonyítják a helyes működést.
A Rust kódot Lean-modellhez kapcsolják
A SymCrypt a Microsoft nyílt forráskódú kriptográfiai könyvtára, amelyet többek között a Windows és az Azure termékei és szolgáltatásai használnak. A Microsoft korábbi bejelentése alapján az új algoritmusokat biztonságos Rustban írják, majd az Aeneas eszközlánccal Lean-formális modellekké alakítják, hogy a Lean bizonyítási keretrendszerben ellenőrizhessék őket.
Ebben a folyamatban a Rust memóriatulajdonlási és kölcsönzési szabályai több, mutatóaliasolással, élettartammal és módosítással kapcsolatos feladatot eleve kezelnek. Az Aeneas a Rust köztes reprezentációját tisztán funkcionális Lean-modellre fordítja. Egy helyben módosított tömbből például olyan függvény lesz, amely bemenetként átveszi, majd eredményként visszaadja a tömböt.
A fejlesztők így továbbra is idiomatikus, teljesítményre optimalizált Rust kódot írhatnak. A bizonyítási mérnökök a létrehozott Lean-modelleken dolgoznak, és tételekkel igazolják, hogy a megvalósítás megfelel a szabványból származó specifikációnak. A Rust-kód és a bizonyítások egymás mellett maradnak, miközben a bizonyítási folyamatnak nem kell természetellenes formára alakítania a programot.
SHA-3 és ML-KEM a nyilvános kiadásban
A Microsoft megnyitotta a SymCrypt egy olyan ágát, amely a Rust-algoritmusok mellett a formális specifikációkat és a bizonyításokat is tartalmazza. A vállalat szerint ez nem önálló kutatási prototípus, hanem a Windows és az Azure által is használt könyvtárhoz kapcsolódó munka.
Az első kiadásban a Windows bennfentes tesztverzióiban már használt Rust-alapú ML-KEM és SHA-3 kód teljes bizonyítása szerepel. A specifikációkat úgy alakították ki, hogy a lehető legközelebb maradjanak a nyilvános szabványokhoz, például a NIST előírásaihoz vagy az IETF RFC-ihez. Ez megkönnyíti az összevetést, miközben a Lean-modellek futtathatók, és hivatalos tesztvektorokkal is ellenőrizhetők.
Az ML-KEM egyik példája a számelméleti transzformáció, az NTT. A Lean-változat a szabványban szereplő ciklusokat, a zétaérték kiválasztását és a koefficiensek frissítését is követi. Így a modell egyszerre vizsgálható soronként, tesztelhető ismert vektorokkal, és összekapcsolható az NTT matematikai jelentését leíró magasabb szintű tételekkel.
Az automatizálás további algoritmusokra terjed
A SymCrypt csapata az eszközláncot további Rust-alapú algoritmusokra is kiterjeszti, és ezeket Windows- és Linux-verziókba integrálja. A Microsoft példaként az AES-GCM-et, a FrodoKEM-et és az ML-DSA-t említi.
A bizonyítási munka skálázásához a Lean szimbolikus végrehajtást, aritmetikát, tömböket és bitvektorokat kezelő automatizmusokat használ. Az AI-ügynökök bizonyításokat és köztes tulajdonságokat írhatnak, miközben a fordítás, a kódkinyerés és a bizonyítás ellenőrzése determinisztikus, önállóan ellenőrizhető folyamat marad. A Microsoft megközelítésében az emberek főként a szabványok formalizálását és a legfontosabb tulajdonságok áttekintését végzik.
Ez a felhasználók számára azt jelenti, hogy a SymCryptben szereplő egyes kriptográfiai megvalósításokhoz a működést alátámasztó specifikációk és bizonyítások is hozzáférhetők. A vállalat célja, hogy a formális ellenőrzés a gyártásban használt, teljesítményorientált kód fejlesztési folyamatának része legyen.
Microsoft Research: Verifying Rust cryptography in SymCrypt, from standards to code
