Google DeepMind käyttää tekoälyagentteja Signalin keskeisen konekoodin varmentamiseen

Google DeepMind esitteli AlphaProof Coden 10. marraskuuta 2026. Se käytti tekoälyagenttiryhmiä tuottamaan koneellisesti tarkistettavia Lean-todistuksia Signal-koodin käännetyn libsignal-toteutuksen määritellyistä tietoturvaominaisuuksista. Viisihenkinen tutkimusryhmä sai todistustyön valmiiksi neljässä viikossa ja julkaisi spesifikaatiot ja varmennusaineiston ulkopuolista arviointia varten.

Työssä siirryttiin Signal-protokollan suunnittelun abstraktista mallista sen käännettyyn toteutukseen. Tutkijat käärivät muuttamattomat libsignal v0.105.4- ja SPQR v1.6.0 -paketit pieneen komentorivityökaluun ja käyttivät sitten vakiomuotoista rustc-kääntäjää staattisesti linkitetyn AArch64 Linux -suoritustiedoston rakentamiseen. Teknisessä artikkelissa tulosta kuvataan ensimmäisiksi protokollatason tietoturvatodistuksiksi laajasti käytössä olevan kryptografisen protokollan toteutuksen muuttamattomalle koodille.

Miten AlphaProof Code jakoi työn

Viisi tutkijaa käytti todistustyöhön neljä viikkoa ja ajoi agentteja jatkuvasti työasemillaan samalla, kun he työstivät rinnakkain symbolisia ja laskennallisia todistuksia. Artikkelin mukaan agentit tuottivat noin 6,5 miljoonaa riviä koneellisesti tarkistettavaa Lean-todistuskoodia, joka perustui noin 26 000 riviin luotettuja spesifikaatioita ja AArch64-semantiikkaa.

Ihmiset valitsivat ominaisuudet, ratkaisivat epäselvyydet ja tietoturvaan liittyvät kompromissit, tarkastivat spesifikaatiot ja säilyttivät lopullisen hyväksyntävallan. Gemini 4 Carbonin ja Claude Opus 5.5:n käyttämät agentit laativat spesifikaatioita ja tarkastivat niitä; tarkastukseen osallistui myös toisen malliperheen malli. Gemini 4 Carbon -agenttiryhmät tuottivat sen jälkeen kaiken todistuskoodin; yksikään kirjoittajista ei kirjoittanut todistuskoodia. Tyypillisissä ajoissa käytettiin 40–80 agenttia yhdellä koneella 24–72 tunnin ajan. Orkestroija ja tiiminvetäjät koordinoivat todistustyön tekijöitä, kun taas arkkitehdin ja integroijan rooleissa ylläpidettiin yhteistä todistuspohjaa.

Portinvartija hyväksyi todistuksen vasta, kun Lean-ydin oli tarkistanut sen ja vertailija varmistanut, että se vastasi erillään pidettyä, ihmisten hyväksymää spesifikaatiota kaikkine transitiivisine määritelmineen ja että siinä käytettiin vain Lean-standardin aksioomia. Agentit saivat ehdottaa pieniä muutoksia, jos todistuksissa paljastui ongelmia spesifikaatioissa, mutta luotettuihin oletuksiin tehtävät muutokset edellyttivät ihmisen hyväksyntää tai käyttäjän määrittämää käytäntöä, ja ne kirjattiin perusteluineen. Valvontamekanismi vastaa dokumentoituun agenttien tuottamiin todistuksiin liittyvään riskiin: spesifikaatiota voidaan heikentää epäsuorasti jonkin sen määritelmän kautta.

Tietoturvan kattavuus ja historiallisten virheiden testaus

Varmennuksen kohteena oli kahdenkeskisten istuntojen koodi, joka kattaa PQXDH-kättelyn ja Triple Ratchet -viestinnän. Tutkijoiden mukaan näyttö koostuu kahdesta toisistaan riippumattomasta perustelusta: kymmenestä symbolisesta lauseesta, jotka perustuvat idealisoituihin kryptografisiin oletuksiin, sekä laskennallisesta todistuksesta, joka rajaa hyökkääjän etua kryptografisten oletusten ja tilastollisten termien avulla. Ominaisuuksiin kuuluvat eteenpäin suuntautuva salassapito, joka suojaa aiempia viestejä nykyisen tilan varastamisen jälkeen; todennus; tietomurron jälkeinen tietoturva, joka liittyy palautumiseen tietomurron jälkeen; sekä kättelyn salassapito. Symbolinen perustelu kattaa lisäksi kättelyn salassapidon myöhemmän Diffie–Hellman-murron jälkeen.

Testatakseen, pystyivätkö spesifikaatiot havaitsemaan todellisia virheitä, ryhmä kumosi kahden aiemmin korjatun libsignal-virheen korjaukset. Virheet tunnettiin nimillä heikko tila ja pieni aliryhmä. Ryhmä käänsi muutetut binäärit uudelleen. Molemmissa tapauksissa se tuotti Lean-todistuksia siitä, että symbolinen tietoturvalause ei pätenyt. Julkinen varmennusvarasto sisältää erillään laskennallisen, symbolisen, yhteisen binääri- ja AArch64-semantiikkaa koskevan aineiston sekä ohjeet todistusten uudelleenrakentamiseen ja riippumattomaan tarkistamiseen.

Signalin teknologiajohtaja Ehren Kret sanoi, että työ ”lisää entisestään luottamustamme koodimme tietosuojatakuisiin”.

Rajoitukset ja seuraavat vaiheet

Takuut eivät lähimainkaan merkitse sitä, että Signal-sovellukset olisi sertifioitu kokonaisuudessaan. Ne koskevat tutkijoiden libsignal-cli-koontiversiota, joka suoritetaan uutena prosessina. Avainten luontia ei varmennettu, ryhmäviestintä jätettiin tulevan työn varaan, eivätkä sivukanavat ja monen laitteen tila kuulu tarkasteltuun tilanteeseen. Matalan tason kryptografiset primitiivit sekä valitut tulosteisiin liittyvät ja kirjaston rutiinit esitetään luotettuina sopimuksina. Siksi tulos riippuu myös näistä sopimuksista, hyväksytyistä spesifikaatioista, Lean-ytimestä, AArch64-semantiikasta ja primitiivejä koskevista oletuksista.

Artikkelissa todetaan, ettei kumpikaan perustelu todista SPQR:n tarkoituksena olevaa kvanttilaskennan jälkeistä palautumiskykyä: laskennallinen lause kattaa klassiset hyökkääjät, kun taas symbolisissa ratchettodistuksissa hyökkääjä voi valita SPQR-avaimet. Laskennallinen malli rajoittaa myös useita hyökkääjän toimia ja menettää merkityksensä, kun viestien ja istuntojen määrä kasvaa riittävän suureksi. Nämä rajat määrittävät, mihin ulkopuolisen arvioijan on luotettava ennen kuin hän voi pitää koneellisesti tarkistettuja todistuksia tietyn käyttöönoton tietoturvatakuuna.

Tutkijoiden ilmoittamiin seuraaviin vaiheisiin kuuluvat lauseiden vahvistaminen, luotetun perustan supistaminen varmentamalla useampia hook-kytkettyjä rutiineja ja yhdistämällä kryptografiset sopimukset varmennettuihin toteutuksiin sekä kattavuuden laajentaminen ryhmäviestintään, sinetöityyn lähettäjään ja palvelinpuolen protokolliin. Tavoite varmentaa uudet libsignal-julkaisut ennen niiden toimittamista on tutkimustavoite, ei ilmoitettu käyttöönotto.

Tuloksen välitön merkitys on siinä, että se osoittaa työnjaon: agentit hoitivat todistusten rakentamisen, kun taas varmistus perustuu edelleen ihmisten tarkastamiin spesifikaatioihin ja nimenomaisiin oletuksiin. Todistusten ja tarkistusmenettelyjen julkaiseminen antaa ulkopuolisille arvioijille mahdollisuuden testata tätä perustaa, kun tutkijat pyrkivät ottamaan työnkulun käyttöön libsignalin jatkuvassa kehitystyössä.