Google DeepMindin tekoäly todisti Signalin salauksen turvallisuuden

Google DeepMindin (Alphabet Inc. ↘ 0.21%) tutkijat käyttivät uutta AlphaProof Code -tekoälykehystä todistaakseen matemaattisesti useita Signalin protokollan keskeisiä kryptografisia takuita. Neljä viikkoa kestäneessä konseptitodistusprojektissa ei löytynyt uusia haavoittuvuuksia tutkituista protokollan osista, WIRED raportoi 10. marraskuutawired.com. Tuloksella on merkitystä Signalin ulkopuolellakin. Samaa protokollaa käytetään viestien suojaamiseen Google Messagesissa ja Meta Platforms, Inc:n ↗ 0.22% WhatsAppissa, joten analyysi tarjoaa riippumattoman tarkistuksen salaukselle, joka suojaa suurta osaa maailman viestinnästä, WIRED kertoo. Se osoittaa myös, että tekoälyagentit voivat nopeuttaa muodollista verifiointia, joka on pitkään tavoiteltu mutta hidas tapa käyttää matematiikkaa ohjelmistojen toiminnan varmistamiseenwired.com. ## Mitä analyysi paljasti Tutkijat testasivat AlphaProof Codea Signalin vanhemmilla versioilla, joissa oli tunnettuja, jo kauan sitten korjattuja haavoittuvuuksia. Työkalu löysi nämä virheet oikein ja osoitti, ettei kyseisiä versioita voitu verifioida muodollisesti, WIRED raportoi. DeepMind julkaisee luomansa määrittelyt ja todistukset, jotta muutkin verifiointihankkeet voivat hyödyntää niitäwired.com. Työn laajuus oli rajattu. Se ei verifioinut koko Signalin mobiilisovellusta, ja tutkijat kuvasivat sitä yhdeksi virstanpylvääksi pidemmässä prosessissa. "Olemme erittäin innoissamme tästä tuloksesta, mutta matkaa on vielä paljon ennen kuin voimme skaalata tämän kaikkeen maailman ohjelmistoon, ja haluamme tehdä niin", DeepMindin tutkija Swarat Chaudhuri kertoi WIREDillewired.com. Tiimin mukaan Signalin aiempi muodollinen verifiointityö antoi heille etumatkaa. "Vaikka aiempi muodollinen verifiointi keskittyi koodin pienempiin osiin, Google DeepMindin lähestymistapa mahdollistaa merkittävän laajentumisen", Signalin teknologiajohtaja Ehren Kret sanoi lausunnossaan ja lisäsi, että verifiointi antaa yritykselle "entistä suuremman luottamuksen" tekoälypohjaisten tietoturvauhkien kasvaessawired.com. ## Ruuhkainen ala DeepMindin työ valmistui samaan aikaan, kun muut ryhmät tavoittelevat vastaavia päämääriä. Huhtikuussa 2026 Signal, Beneficial AI Foundation ja Lean FRO käynnistivät Signal Shot -hankkeen, jonka tavoitteena on verifioida Signalin protokolla ja sen Rust-toteutus Lean-todistusavustajaa käyttäen. Projektin tarkoituksena on kääntää Signalin koodi Lean-kielelle ja todistaa sen vastaavan protokollan verifioitua mallia, säätiö kertoo. DeepMindin tulos on erillinen tästä hankkeesta, Startup Fortune huomauttibeneficialaifoundation.org+2. ## Avoimia kysymyksiä kustannuksista On vielä epäselvää, voidaanko tekoälyavusteinen verifiointi skaalata järkevin kustannuksin. DeepMind teki Signalin analyysin ilmaiseksi tutkimusprojektina. Google ei kertonut, mitä se maksoi tai aikooko se kehittää kaupallisen verifiointituotteen, WIRED raportoiwired.com. Chaudhurin mukaan keskeinen edistysaskel oli prosessi, jossa tekoälyagentit osallistuvat ja korjaavat omaa työtään ihmisten tarkistaessa sitä kriittisissä kohdissa. "Emme halua tällaista maailmaa, jossa tekoäly luo tavoitteet ja todistukset ja käytännössä suorittaa itse kirjoittamiaan testejä", hän sanoi. "On olemassa kultainen keskitie"wired.com.