Tekoäly todisti neljässä viikossa, että Signalin salaus pitää

Kun lähetät Signalissa viestin työkaverille tai sukulaiselle, puhelimessa käynnistyy salauskoodi, jonka pitäisi estää ketään muuta lukemasta sitä. Pitäisi. Tähän asti kukaan ei ole pystynyt todistamaan, että juuri puhelimessa ajettava koodi tekee täsmälleen sen, mitä protokollan suunnitelma lupaa.

Google DeepMind kertoi tiistaina 10. marraskuuta, että sen uusi AlphaProof Code -järjestelmä on tehnyt tämän todistuksen Signalin salauskirjastolle libsignalille. Työ kesti neljä viikkoa. DeepMindin mukaan vastaava urakka on vaatinut asiantuntijatiimeiltä vuosia, eikä näin laajasti käytetyn protokollan toteutusta ole aiemmin verifioitu formaalisti millään menetelmällä, tekoälyllä tai ilman.

Signal-protokolla suojaa DeepMindin mukaan miljardeja keskusteluja Signalissa ja Google Messagesissa. Molemmat ovat monen suomalaisenkin puhelimessa.

Testaamisen sijaan todistus

Ohjelmistoa testataan tavallisesti kokeilemalla: sisään syötetään erilaisia viestejä ja katsotaan, meneekö jokin rikki. Testi löytää vain ne virheet, joita joku osasi etsiä. Formaalissa verifioinnissa koodin käyttäytymisestä kirjoitetaan matemaattinen todistus, ja tietokone tarkistaa sen jokaisen askeleen.

Lean on ohjelmointikieli, johon tällaiset todistukset kirjoitetaan. Se hyväksyy todistuksen vain, jos jokainen päättelyaskel pitää, eikä se luota kirjoittajaan, oli tämä ihminen tai tekoäly.

Agentit kirjoittivat, ihmiset päättivät

Tutkijat käänsivät ensin Signalin turvallisuustavoitteet täsmällisiksi määrittelyiksi, ja ihmisasiantuntijat kävivät jokaisen läpi. Sen jälkeen Gemini Carbon -mallilla toimivat agentit kirjoittivat todistukset. Teknisen raportin mukaan samaan tehtävään osallistui tyypillisesti 40–80 agenttia kerrallaan. The Registerin mukaan hankkeessa työskenteli viisi tutkijaa.

Rivimäärästä on liikkunut eri lukuja. DeepMindin blogissa puhutaan yli kuudesta miljoonasta Lean-rivistä, ja teknisessä raportissa luku tarkentuu noin 6,5 miljoonaan riviin koneellisesti tarkistettua todistuskoodia. Joissakin tiivistelmissä esiintynyttä kolmen miljoonan riviä ei löydy DeepMindin omista julkaisuista. Todistukset nojaavat noin 26 000 riviin määrittelyjä ja prosessorin toiminnan kuvausta. Siihen osaan on pakko luottaa, ja sen tarkistivat ihmiset.

Lopuksi agentit auditoivat oman työnsä ja merkitsivät noin prosentin koodista ihmisen katsottavaksi.

Todistus koskee käännettyä konekoodia, siis sitä, mikä oikeasti ajetaan laitteella. Tutkijat käänsivät muuttamattoman libsignalin version 0.105.4 tavallisella Rust-kääntäjällä ARM-pohjaiselle Linuxille ja todistivat ominaisuudet tästä ohjelmasta. Todistettuihin ominaisuuksiin kuuluu esimerkiksi se, että viestit pysyvät suojassa sekä ennen että jälkeen sen, kun laite on hetkellisesti ollut hyökkääjän hallussa.

Kretin mukaan aiempi formaali verifiointi on keskittynyt Signalin koodin pienempiin osiin. Hänen mukaansa tarkka verifiointi ”antaa meille entistäkin enemmän luottamusta koodimme yksityisyystakuisiin”, kun tekoälyä hyödyntävät tietoturvauhat kasvavat.

Vanhat bugit jäivät kiinni

Pitää myös tietää, osaako järjestelmä erottaa rikkinäisen koodin ehjästä vai hyväksyykö se kaiken. Sitä varten tutkijat palauttivat libsignalin eristettyyn kopioon kaksi oikeaa, jo aikoja sitten korjattua haavoittuvuutta.

Ensimmäinen liittyi tilanteeseen, jossa viesti aukesi vain arkistoidulla istunnolla. Silloin kirjasto tallensi uuden istunnon tilan ja sen mukana kopion salaisesta avaimesta. Toinen oli X25519-avainten käsittelyyn liittyvä niin sanottu small subgroup -virhe.

Molemmissa tapauksissa järjestelmä tuotti koneellisesti tarkistetun todistuksen siitä, että vanhan virheen sisältävä versio ei täytä turvallisuusvaatimusta. Sama koneisto, joka sanoo koodia turvalliseksi, pystyy siis myös näyttämään toteen, milloin koodi ei ole turvallinen.

Mitä todistus ei kata

Matemaattinen todistus on vain niin kattava kuin sen oletukset. Raportin mukaan työ koskee kahdenkeskisiä keskusteluja, ja ryhmäviestit jätettiin myöhemmäksi. Avainten luontia ei verifioitu, eikä tarkastelu kata tilannetta, jossa samalla tilillä on useita laitteita.

Salausalgoritmit itsessään oletettiin turvallisiksi. Todistus näyttää, että libsignal käyttää niitä oikein, mutta ei sitä, että itse algoritmit kestävät hyökkäykset. Kvanttitietokonetta käyttävä hyökkääjä on rajattu laskennallisen todistuksen ulkopuolelle, ja Signalin SPQR-lisäosan lupaamaa toipumista kvanttihyökkäyksestä ei todistettu.

Tavallisen käyttäjän kannalta tärkein rajaus on yksinkertainen: todistus ei suojaa puhelinta. Jos laitteessa on vakoiluohjelma tai joku lukee näyttöä olan yli, salaus ei auta. Todistus ei kerro mitään metatiedoista, kuten siitä, kuka viestii kenen kanssa ja milloin. Se ei kata myöskään sivukanavahyökkäyksiä, joissa salaisuuksia päätellään esimerkiksi laskennan ajoituksesta.

Google Messagesista pitää tehdä erillinen varaus. DeepMind mainitsee sovelluksen protokollan käyttäjänä, mutta verifioitu koodi on Signalin oma libsignal-kirjasto. Blogin mukaan Google Messagesin toteutusta ei ole käyty läpi.

Kuka tarkistaa tarkistajan?

Kaikki tähänastiset kommentit tulevat DeepMindilta tai Signalilta, joka on hankkeen yhteistyökumppani. Riippumattomien kryptografiatutkijoiden arvioita ei ollut julkaistu keskiviikkoaamuun mennessä. Koska todistukset ovat avoimesti saatavilla, kuka tahansa voi ajaa Leanin tarkistuksen itse, ja ulkopuolisia arvioita on todennäköisesti tulossa.

DeepMindin tutkija, Texasin yliopiston professori Swarat Chaudhuri kuvasi The Registerille alan vanhaa uskomusta englanniksi näin: ”Formaaleissa menetelmissä olemme aina uskoneet, että verifiointi on se vaikea osa.” Hänen mukaansa asetelma on nyt kääntymässä: ”Uskomme vahvasti, että tällaisessa tutkimuksessa seuraava rintama ei ole todistaminen vaan määrittely.”

Tämä on jutun tärkein jatkokysymys. Jos kone pystyy todistamaan sen, mitä siltä pyydetään, ratkaisevaksi nousee se, pyysikö ihminen oikeaa asiaa. Noin 26 000 riviä määrittelyjä on se kohta, jossa virhe voisi vielä piillä, ja sen tarkistamiseen tarvitaan edelleen ihmisiä.

Vaikutus voi ulottua pikaviestimiä laajemmalle. DeepMind mainitsee mahdollisina kohteina lääkintälaitteiden ja sähköverkkojen ohjelmistot. Niissä virhe maksaa enemmän kuin vuotanut viesti, ja tähän asti formaali verifiointi on ollut niin kallista, että siihen on ollut varaa vain harvoilla. Jos työ, joka ennen kesti vuosia, onnistuu kuukaudessa, yhä useampi ohjelmistotoimittaja voi joutua selittämään asiakkailleen, miksi niiden koodia ei ole todistettu.

Signalin käyttäjälle muutos ei näy mitenkään. Sovellus ei päivity eikä toimi toisin. DeepMindin tavoitteena on, että uudet libsignal-versiot voitaisiin todistaa ennen julkaisua, mutta raportin mukaan se on vasta tutkimustavoite eikä käytössä oleva käytäntö.