A Google DeepMind bejelentette, hogy kutatói mesterséges intelligencia (AI) ügynökök irányításával formálisan bizonyították a Signal protokoll mögötti tényleges kriptográfiai kód egyes kulcsfontosságú biztonsági tulajdonságait. A Signal protokollot olyan alkalmazások használják, mint a Signal és a Google Messages; a technológia milliárdnyi privát beszélgetést véd.
Az eszköz: AlphaProof Code
A munkát az AlphaProof Code nevű új, ügynökalapú keretrendszerrel végezték, amely kombinálja az emberi szakértelmet és a több nyelvi modellből álló AI-csoportok munkáját. A keretrendszer célja a formális verifikáció — vagyis matematikai bizonyítékok előállítása arra, hogy a kód hibátlanul működik — mélyebb, automatizált szintre emelése.
Hogyan történt a verifikáció
- A projektben a DeepMind és a kutatócsapatok először a Signal biztonsági célkitűzéseit formális matematikai specifikációkká fordították, emberi szakértők felülvizsgálatával.
- Azután AI-ügynökök, köztük a Gemini Carbon modellel működő agentek, állították elő a bizonyításokat: az ügynökök több mint hatmillió (6 000 000+) sort generáltak Lean nyelven, amelyet számítógépes bizonyításokra használnak.
- Az ügynökök ellenőrizték a bizonyításokat és jelezték azokat a részeket, amelyek további emberi áttekintést igényeltek — a projekt szerint ez a teljes kódbázis mindössze egy százalékát érintette, ami jelentős időmegtakarítást eredményezett, mivel a Lean automatikusan ellenőrzi a maradékot.
Miért jelent ez előrelépést
A kriptográfiai protokollok vizsgálata hagyományosan a tervezési szinten áll; a valós rendszerek implementációja és a fordított, kész kód megfelelőségének bizonyítása jóval bonyolultabb. A DeepMind szerint ez az első alkalom, amikor AI-ügynökökre támaszkodva egy széles körben telepített kriptográfiai protokoll implementációját ilyen mélységben formálisan verifikálták — azaz nem csak a specifikációt, hanem a lefordított, eszközökön futó tényleges kódot is leellenőrizték a biztonsági tulajdonságokra.
Konkrétan a bizonyítások kiterjedtek olyan biztonsági jellemzőkre, mint az üzenetek védelme arra az esetre is, ha egy eszköz átmenetileg kompromittálódik (elők és utókondíciók). Mivel a valós sebezhetőségek gyakran a tervezés és az implementáció közötti hézagokban bújnak meg, ennek a héznak a lezárása növeli a biztonság bizonyosságát.
Idő és megbízhatóság
A DeepMind közlése szerint a teljes verifikációs folyamat mindössze négy hétig tartott — olyan feladat, amely hagyományosan évekig tartó, kézi munkát igényelt volna szakértői csapatoktól. A csapat a megbízhatóság ellenőrzésére két korábban javított, valós hibát visszajuttatott egy izolált Signal-kódbázisba: mindkét esetben a rendszer géppel ellenőrzött bizonyítást állított elő arról, hogy a hibás verzió nem biztosítja a kívánt biztonságot.
Kitekintés és alkalmazhatóság
A DeepMind hangsúlyozza, hogy az AlphaProof Code megközelítése lehetővé teszi a formális verifikáció kiterjesztését komplex, valós rendszerekre, és alkalmazható lehet más kritikus szoftverekre — például orvosi eszközök firmware-ére vagy az elektromos hálózati szoftverekre. A technika további kutatást és skálázási munkát igényel, de a vállalat szerint a kombináció automatizált védelmi ügynökökkel, például a CodeMenderrel, segíthet felvenni a versenyt a modern, ügynök-alapú kibertámadások sebességével.
Nyílt forrás és elismerések
A DeepMind közölte, hogy nyílt forrásúvá teszi a formális verifikációs anyagokat a közösség számára. A kutatásban részt vevő szerzők: Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton és Pushmeet Kohli. Külön köszönetet mondtak többek között Eric Wiesernek az open-source segítségért és a Signal képviselőinek — Rolfe Schmidtnek, Michael Rosenbergnek és Ehren Kretnek — a módszertanra vonatkozó visszajelzésekért.
Összegzés
A DeepMind állítása szerint az AlphaProof Code segítségével az AI-ügynökök négy hét alatt formálisan bizonyították a Signal alapkriptográfiájának implementációját, több millió sor Lean-bizonyítást előállítva és emberi áttekintést a kód mindössze egy százalékára szorítva. Ha az eredmények függetlenül is megerősítést nyernek, ez mérföldkő lehet a kritikus szoftverek matematikai garanciáinak szélesebb körű alkalmazásában.
