A Apple Security Research blogján az Apple bejelentette, hogy a corecrypto legfrissebb kiadásával nyilvánosságra hozza a kvantumbiztos titkosítási algoritmusai (ML-KEM és ML-DSA) implementációját — és ami igazán szokatlan: a matematikai bizonyítékokat is, amelyekkel igazolják, hogy a kód hibátlanul megfelel a hivatalos szabványnak. Mindezt nyílt forrásként, hogy bárki ellenőrizhesse.
A corecrypto az Apple operációs rendszereinek alapvető kriptográfiai könyvtára — titkosítást, hashelést, véletlenszám-generálást és digitális aláírást biztosít több mint 2,5 milliárd aktív eszközön. Egyetlen kritikus hiba benne minden ráépülő appot és funkciót veszélyeztetne.
Mi az a kvantumbiztos kriptográfia, és miért most?
A jövőbeli kvantumszámítógépek képesek lesznek feltörni a ma használt titkosítási eljárások jelentős részét. Az Apple ezért már 2024-ben elkezdte beépíteni a posztkvantum titkosítást — először ott, ahol a legtöbbet ér: titkosított kommunikációnál (iMessage, VPN, TLS). A mostani lépés a következő szint: nemcsak beépítik, hanem matematikailag bizonyítják is, hogy a kód helyes.
A két algoritmus, amit az Apple választott — ML-KEM (FIPS 203) és ML-DSA (FIPS 204) — a NIST által szabványosított posztkvantum eljárások.
A „formális verifikáció” — miért más, mint a sima tesztelés?
Itt van a cikk lényege. A hagyományos szoftvertesztelés mintát vesz: bemenetek egy részére ellenőrzi, hogy jó-e a kimenet. A formális verifikáció ezzel szemben matematikai bizonyítást ad arra, hogy a kód minden lehetséges bemenetre helyesen működik.
Ahogy az Apple fogalmaz: ha bebizonyítható, hogy az implementáció matematikai formulája megegyezik a specifikációéval, akkor biztos, hogy a kód mindig a helyes kimenetet adja — ezt a szintű biztonságot hagyományos teszteléssel egyszerűen nem lehet elérni.
Az Apple egyébként több mint 15 éve használ formális verifikációt a chipfejlesztésben, 2019 óta pedig kriptográfiai hardvernél is.
Hogyan csinálták?
A folyamat több lépcsős, és pont ettől nehéz:
- A hordozható C kódot lefordítják a Cryptol nevű formális nyelvre, és a SAW eszközzel igazolják, hogy a kettő megegyezik.
- A Cryptol-modellt egy újonnan épített fordítóval (cryptol-to-isabelle) átültetik az Isabelle bizonyításasszisztensbe — így az emberi hiba kockázata is kiesik.
- A FIPS-szabványt is kézzel beültetik Isabelle-be, majd matematikailag igazolják a két oldal egyenértékűségét.
- Végül a kézzel optimalizált ARM64 assembly rutinokat is ellenőrzik — itt a C-verzióval vetik össze, ami már bizonyítottan helyes.
A léptékre jellemző: a teljes bizonyítás több mint 50 000 lépést igényelt.
Az eredmény: valódi hibákat fogtak meg
Nem elméleti gyakorlatról van szó. A formális verifikáció olyan hibákat talált, amiket a hagyományos tesztelés nem fogott volna meg:
- Egy korai ML-DSA implementációból hiányzott egy lépés, ami ritka esetekben tartományon kívüli bemenetet és hibás kimenetet okozhatott volna. Rosszabb esetben csendben elronthatott volna kriptográfiai számításokat — minden figyelmeztetés nélkül.
- Egy harmadik féltől származó bizonyításban is hibát találtak, amit önállóan kijavítottak a saját paramétereikre.
Mit jelent ez?
Két dolog miatt fontos. Egyrészt az Apple a lehető legmagasabb ma elérhető helyességi garanciát éri el egy éles, tömegesen használt ML-KEM/ML-DSA implementációnál — méghozzá úgy, hogy a kézzel optimalizált, gyors kódot is lefedi (ez eddig komoly trade-off volt).
Másrészt — és ez ritka egy Apple-től — mindent nyilvánosságra hoznak: a verifikációs könyvtárakat, a Galois-szal közösen épített fordítót, az Isabelle-elméleteket. A cél, hogy a szélesebb kriptográfiai közösség is használhassa és ellenőrizhesse. Az Apple itt tudatosan próbálja elkerülni azt a hibát, ami az elliptikus görbe kriptográfia korai bevezetésénél történt — ahol finom, kihasználható bugok bujkáltak évekig a kódban.
A háttérben pedig ott a nagyobb kép: ahogy a kvantumszámítás (lásd a mostani IBM-bejelentést) közeledik, úgy válik a posztkvantum kriptográfia helyessége nem akadémiai kérdéssé, hanem 2,5 milliárd eszköz biztonságának alapjává.
