Signals kryptering besto et KI-bevis på 6,5 millioner linjer

Signals krypteringskode har nå noe som nesten ingen mye brukt programvare kan vise til: et matematisk bevis på at den gjør det den lover. Et team med KI-agenter gikk gjennom libsignal, biblioteket som driver Signal-protokollen, og beviste at samtaler mellom to personer forblir hemmelige, bekrefter hvem som er i den andre enden og igjen stenger en angriper ute etter at en nøkkel er stjålet. De fant ingen nye feil.

Dette har betydning langt utover Signals egne brukere. Protokollen er den globale standarden for ende-til-ende-krypterte meldinger, og varianter av den beskytter samtaler i WhatsApp, Messenger og Google Messages. Det har tidligere vært så tidkrevende å kontrollere ferdig utrullet kode på dette detaljnivået at nesten ingen har forsøkt: En av fagfeltets største suksesser, en verifisert operativsystemkjerne, krevde tjue personår. Denne jobben tok fire uker.

Verktøyet, utviklet av Google DeepMind, heter AlphaProof Code. Først gjorde menneskelige eksperter og KI-modeller Signals sikkerhetsmål om til formelle påstander i Lean, et programmeringsspråk laget for matematiske bevis, og et menneske kontrollerte hver eneste påstand. Deretter skrev team på 40 til 80 agenter, drevet av Gemini Carbon, bevisene. De arbeidet i 24 til 72 timer av gangen på én enkelt maskin. Resultatet er rundt 6,5 millioner linjer Lean-kode.

Ingen trenger å stole på disse millionene av kodelinjer. Leans kjerne kontrollerer hvert trinn og forkaster alle bevis som ikke holder, så det spiller ingen rolle hvilken modell som skrev dem, eller hvor ofte den tok feil underveis. Det folk faktisk må stole på, er langt mindre: rundt 26 000 linjer med spesifikasjoner og en modell av hvordan en ARM-prosessor kjører kode.

Bevisene dekker delene av Signal som beskytter en samtale: PQXDH-håndtrykket som oppretter en samtale, og Triple Ratchet, som bytter nøkkel for hver melding. Dette omfatter også det postkvantiske laget, som skal motstå framtidige kvantedatamaskiner. I praksis betyr det at noen som stjeler de gjeldende nøklene fra en telefon, ikke får tilgang til eldre meldinger, og mister tilgangen igjen når de to partene utveksler nye nøkler.

For å vise at systemet kan skille god kode fra dårlig kode, la forskerne to gamle, allerede rettede feil i libsignal inn igjen. Den ene gjorde at biblioteket beholdt en kopi av en hemmelig nøkkel det skulle ha slettet. I begge tilfellene produserte AlphaProof Code et maskinkontrollert bevis på at versjonen med feilene var usikker.

Begrensningene er reelle. Beviset gjelder bare samtaler mellom to personer, og DeepMind oppgir gruppemeldinger som et område for framtidig arbeid. Det gjelder libsignal versjon 0.105.4, kompilert med standardkompilatoren for Rust for ARM Linux i et lite testprogram – ikke de fullstendige Signal-appene for iPhone, Android eller datamaskiner. Det forutsettes at de grunnleggende kryptografiske byggesteinene er sikre; de er ikke bevist sikre. En feil i spesifikasjonene som mennesker har godkjent, ville svekke garantien. WhatsApp og de andre appene bruker dessuten sine egne versjoner av protokollen, så resultatet gjelder ikke automatisk for dem. Google ville heller ikke fortelle Wired hva analysen kostet, eller om selskapet planlegger å selge den som en tjeneste.

Signal tok godt imot resultatet. «Etter hvert som KI-drevne sikkerhetstrusler øker, gir en grundig verifisering av implementeringen av Signal-protokollen oss enda større tillit til personverngarantiene i koden vår», sa Ehren Kret, Signals teknologidirektør, i en uttalelse. DeepMind-forskeren Swarat Chaudhuri var mer forsiktig. Til Wired sa han at det er «langt igjen» før metoden kan skaleres «til all programvaren i verden».

For dem som bruker Signal, er det ingenting som må installeres, og ingen innstillinger som må endres. Beviset gjelder kode som allerede finnes i appen.

DeepMind publiserte arbeidet 10. november, sammen med en teknisk artikkel, og har lagt ut spesifikasjonene og bevisene som åpen kildekode på GitHub. Selskapet omtaler Signal-prosjektet som en milepæl på veien mot en stor utfordring innen formell verifisering, som ble lansert i april. Det trekker fram fastvaren i medisinsk utstyr og programvare for strømnett som eksempler på systemer det vil kontrollere videre.

Chaudhuri trakk også en grense for hvor mye av arbeidet maskinene bør få gjøre. «Vi vil ikke ha en sånn verden der KI finner på målene og KI lager bevisene», sa han til Wired. Mennesker avgjør fortsatt hva som regnes som sikkert; KI-en beviser det bare.

Tagger: cybersikkerhet, Google DeepMind, AlphaProof Code, ende-til-ende-kryptering, formell verifisering, libsignal