Google DeepMind kertoi tuloksesta 10. marraskuuta blogikirjoituksessa ja teknisessä artikkelissa. Wired ja ZDNet uutisoivat asiasta samana päivänä yhtiön tiedotteen ja haastattelujen pohjalta, joten ne eivät vahvista tuloksia riippumattomasti.

Signal-protokolla salaa viestit Signal-sovelluksessa ja Google Messagesissa, Wiredin ja ZDNetin mukaan myös WhatsAppissa. DeepMindin mukaan agentit eivät todistaneet ominaisuuksia vain protokollan suunnitelmalle vaan itse toteutukselle. Yhtiö perustelee tätä sillä, että todelliset haavoittuvuudet piilevät usein suunnitelman ja toteutuksen eroissa.

Ihmiset määrittelivät, agentit todistivat

Formaalissa verifioinnissa ohjelmaa ei vain testata, vaan sen osoitetaan matemaattisesti toimivan määrittelyn mukaisesti kaikissa tilanteissa. Todistus kattaa siis vain sen, mitä määrittelyyn on kirjattu.

AlphaProof Codessa tutkijat muotoilivat ensin useiden kielimallien avulla Signalin tietoturvatavoitteet matemaattisiksi määrittelyiksi. Asiantuntijat tarkistivat jokaisen. Sen jälkeen DeepMindin Gemini Carbon -mallia käyttävät tekoälyagentit kirjoittivat todistukset, yhteensä yli kuusi miljoonaa riviä Leania. Lean on ohjelmointikieli, jossa tietokone tarkistaa todistuksen jokaisen askeleen.

Lisäksi agentit kävivät todistukset läpi ja merkitsivät prosentin koodista ihmisen tarkistettavaksi. Muun osan Lean tarkistaa automaattisesti.

”Emme halua tällaista fiilispohjaista maailmaa, jossa tekoäly tuottaa sekä tavoitteet että todistukset ja käytännössä tekee itse kirjoittamiaan kokeita”, DeepMindin tutkija Swarat Chaudhuri sanoi Wiredille.

Mitä todistettiin ja mitä jäi ulkopuolelle

DeepMindin mukaan ominaisuudet todistettiin käännetylle koodille, jota laitteet ajavat. Yksi ominaisuuksista on, että viestit pysyvät suojassa sekä ennen laitteen tilapäistä murtamista että sen jälkeen. Wiredin mukaan tarkistus ei kattanut esimerkiksi koko Signalin mobiilisovellusta.

Työ kesti neljä viikkoa. Yhtiön mukaan vastaava on vienyt asiantuntijaryhmiltä vuosia. DeepMindin tutkijat huomauttavat Wiredissä, että Signal-säätiön aiempi formaali verifiointi antoi heille jonkin verran etumatkaa. DeepMind sanoo, ettei tällaisen laajalti käytetyn protokollan toteutusta ole aiemmin verifioitu formaalisti millään menetelmällä. Signalin teknologiajohtaja Ehren Kret toteaa lausunnossaan, että aiempi verifiointi keskittyi koodin pienempiin osiin.

Wiredin mukaan protokollan tarkastelluista osista ei löytynyt uusia haavoittuvuuksia. Testissä tutkijat palauttivat eristettyyn koodiversioon kaksi aiemmin korjattua todellista virhettä. Molemmissa tapauksissa järjestelmä tuotti koneellisesti tarkistetun todistuksen siitä, että versio oli turvaton.

Chaudhurin mukaan menetelmän laajentamiseen kaikkiin maailman ohjelmistoihin on vielä pitkä matka. Google ei kertonut Wiredille analyysin kustannuksia.

Mitä avataan muiden käyttöön

DeepMind avaa verifioinnin aineistot muiden käyttöön, Wiredin mukaan määrittelyn ja todistuksen. ZDNetin alaotsikon mukaan yhtiö aikoo avata myös itse AlphaProof Coden, mutta DeepMindin tiedote puhuu vain verifioinnin aineistoista. Wiredin mukaan Google ei kommentoinut, onko kaupallinen tuote tulossa.