Az AI-agent négy hét alatt matematikailag igazolta a Signal-protokoll titkosítását

A Google DeepMind kutatói agentalapú AI-val matematikailag igazolták a Signal-protokoll több kulcsfontosságú kriptográfiai garanciáját — írja a WIRED. A „formális verifikáció” során a szoftver működését matematikai bizonyítással ellenőrzik, hogy kiderüljön, nincsenek-e kritikus sebezhetőségei.

A projekt négy hét alatt készült, proof-of-concept jelleggel. A kutatás a Signal alkalmazás mellett a Google Messages és a WhatsApp titkosításának függetlenebb ellenőrzését is jelenti. A DeepMind az eredményhez az AlphaProof Code nevű új AI-keretrendszert használta.

Mit talált az elemzés?

A vizsgált részekben a kutatók nem találtak új sebezhetőséget. A módszer ugyanakkor működését is igazolta: a régebbi Signal-verziókon, amelyekben ismert, már javított hibák voltak, az AlphaProof Code azonosította a sebezhetőségeket, és megmutatta, hogy az adott protokoll nem verifikálható formálisan.

Az elemzés hatóköre korlátozott volt. A teljes Signal mobilalkalmazást nem verifikálták formálisan. Swarat Chaudhuri, a DeepMind kutatója szerint az eredmény csak egy mérföldkő: „Nagyon izgat minket ez az eredmény, de hosszú út áll előttünk, mielőtt ezt a világ összes szoftverére ki tudjuk terjeszteni.”

Miért számít a sebesség?

A formális verifikáció korábban rendkívül időigényes volt, mert az embereknek formulákra kellett fordítaniuk a szoftver tulajdonságait, majd kidolgozniuk a bizonyítást. Az agentalapú AI jelentősen lerövidítheti az utóbbi szakaszt. A DeepMind kutatói hozzátették, hogy a gyorsaságban szerepet játszott a Signal Foundation korábbi formális verifikációs munkája is.

A Signal technológiai vezetője, Ehren Kret szerint a DeepMind megközelítése jelentős kiterjesztést tesz lehetővé, mivel a korábbi verifikáció kisebb kódrészekre koncentrált. A kutatók ezenkívül közzéteszik a Signal-elemzéshez készített specifikációt és bizonyítást, hogy más formális verifikációs munkákat is segítsenek.

Nyitott kérdések

Pushmeet Kohli, a Google Cloud főtudósa és a DeepMind kutatási alelnöke szerint, ha ezek az implementációk ellenőrizhetők, a bankok és más, bizonyosságra támaszkodó cégek is bizonyíthatnák tulajdonságaikat. A kutatás azonban nem tisztázza, hogy az AI-alapú formális verifikáció skálázható-e, és megfizethető-e. A DeepMind az elemzést díjmentesen végezte, a Google nem árulta el a költségeket, és nem nyilatkozott arról, tervez-e kereskedelmi terméket.