AlphaProof Code: AI-agentek igazolták a Signal kódját

Mi történt?

A Google DeepMind november 10-én mutatta be az AlphaProof Code-ot (Google DeepMind). Ez egy több LLM-re épülő agentes keretrendszer formális verifikációhoz, vagyis ahhoz, hogy matematikailag bizonyítsák: a kód hibátlanul azt csinálja, amit kell. Az első nagy eredmény a Signal protokoll, ami a Signal illetve a Google Messages titkosított beszélgetéseit védi.

A DeepMind szerint ez az első eset, hogy AI-jal ilyen mélységben formálisan igazoltak egy széles körben használt kriptográfiai protokollt. Sőt, ilyen protokoll implementációját eddig semmilyen módszerrel nem verifikálták így, AI-jal vagy anélkül.

Hogyan működik?

A munkamegosztás egy kutatócsoportot követ. A kutatók több modellel együtt fordították le a Signal biztonsági céljait formális matematikai specifikációkká, ezeket humán szakértők egyenként átnézték. A bizonyításokat a Gemini Carbon alapú agentek írták meg: több mint hatmillió sor Leant generáltak. A Lean egy programozási nyelv, amivel gépileg ellenőrizhető bizonyítás írható.

Utána az agentek maguk auditálták a bizonyítást. Megjelölték azokat a részeket, ahová ember kell. Ez a kód mindössze egy százaléka volt. A többit a Lean automatikusan ellenőrzi, így a szakértők oda koncentrálhattak, ahol tényleg emberi ítélet kell.

Miért nagy dolog?

A protokoll-verifikáció többnyire a tervezési szinten megáll. Az AlphaProof Code agentjei viszont azt bizonyították, hogy a lefordított kód teljesíti a kulcsfontosságú biztonsági tulajdonságokat, például azt, hogy az üzenetek védve maradnak egy eszköz átmeneti kompromittálása előtt illetve után is. A valós sérülékenységek gyakran épp a terv és az implementáció közötti résben bújnak meg.

A teljes folyamat négy hétig tartott, ami a DeepMind szerint korábban szakértői csapatoknak éveket vett igénybe. Ellenpróbaként két valódi, korábban már javított hibát visszaraktak a Signal kódjának egy izolált változatába. A rendszer mindkét esetben gépileg ellenőrzött bizonyítást adott arra, hogy a hibás verzió nem biztonságos.

Ehren Kret, a Signal CTO-ja szerint a korábbi formális verifikáció a kód kisebb részeire fókuszált, az élő kód érvényes Lean tételekké fordítása AI-agentekkel pedig jelentős áttörés.

Mit jelent ez nekünk?

Fejlesztői oldalról ez az egyik első jel, hogy a formális verifikáció kijöhet az akadémiai sarokból. Ha a specifikáció megírása marad emberi munka, a bizonyítás nagy része pedig agentekre bízható, akkor kritikus kódnál reális opció lehet. A DeepMind nyílt forrásként kiadja a verifikációs artifactokat, a technikai paper is elérhető.

A Google ezt az irányt a CodeMenderhez hasonló automatikus védelmi agentekkel párosítaná. Ugyanez a csapat nemrég RSA-1024 gyengeségeket is talált agentekkel, vagyis a DeepMind egyszerre dolgozik a támadó és a védekező oldalon.

Mit érdemes figyelni?

Egyelőre minden szám a DeepMind saját közléséből származik, független ellenőrzés még nincs. A kiadott artifactok lesznek az első valódi teszt. A következő célpontként orvosi eszközök firmware-jét illetve energiahálózati szoftvereket említenek, ezek skálázásához viszont a cég szerint még további kutatás kell.