Signals kryptering bestod et AI-bevis på 6,5 millioner linjer

Signals krypteringskode har nu noget, som næsten ingen udbredt software kan bryste sig af: et matematisk bevis for, at den gør det, den lover. Et hold AI-agenter gennemgik libsignal, biblioteket, der driver Signal-protokollen, og beviste, at en-til-en-samtaler forbliver hemmelige, bekræfter, hvem der er i den anden ende, og igen holder en angriber ude, efter at en nøgle er blevet stjålet. De fandt ingen nye fejl.

Det har betydning langt ud over Signals egne brugere. Protokollen er den globale standard for end-to-end-krypterede beskeder, og varianter af den beskytter samtaler i WhatsApp, Messenger og Google Messages. Det plejede at være så langsommeligt at kontrollere kode, der faktisk er udgivet, i så stor dybde, at næsten ingen forsøgte: En af feltets største succeser, en verificeret styresystemkerne, krævede tyve personår. Dette arbejde tog fire uger.

Værktøjet, som Google DeepMind har udviklet, hedder AlphaProof Code. Først omsatte menneskelige eksperter og AI-modeller Signals sikkerhedsmål til formelle udsagn i Lean, et programmeringssprog udviklet til matematiske beviser, og et menneske gennemgik hvert eneste udsagn. Derefter skrev hold på 40 til 80 agenter, drevet af Gemini Carbon, beviserne. De arbejdede i intervaller på 24 til 72 timer ad gangen på én enkelt maskine. Resultatet er omkring 6,5 millioner linjer Lean-kode.

Ingen behøver at stole på de millioner af linjer. Leans kerne kontrollerer hvert trin og forkaster ethvert bevis, der ikke holder, så det gør ingen forskel, hvilken model der skrev det, eller hvor ofte modellen tog fejl undervejs. Det, folk faktisk skal stole på, er langt mindre: omkring 26.000 linjer specifikationer og en model af, hvordan en ARM-processor afvikler kode.

Beviserne dækker de dele af Signal, der beskytter en samtale: PQXDH-håndtrykket, som opretter en chat, og Triple Ratchet, der skifter nøgle for hver besked, herunder det post-kvantelag, der skal modstå fremtidige kvantecomputere. I praksis betyder det, at et tyveri af telefonens aktuelle nøgler ikke giver adgang til ældre beskeder, og at tyven igen mister adgangen, når de to parter udveksler nye nøgler.

For at vise, at systemet kan skelne mellem god og dårlig kode, genindførte forskerne to gamle fejl i libsignal, som allerede var blevet rettet. Den ene fik biblioteket til at beholde en kopi af en hemmelig nøgle, som det burde have slettet. I begge tilfælde frembragte AlphaProof Code et maskinverificeret bevis for, at den fejlbehæftede version var usikker.

Begrænsningerne er reelle. Beviset omfatter kun en-til-en-sessioner, og DeepMind nævner gruppebeskeder som fremtidigt arbejde. Det gælder libsignal version 0.105.4, kompileret med standard-Rust-kompileren til ARM Linux i et lille testprogram – ikke de fulde Signal-apps til iPhone, Android eller computer. Det forudsættes, at de kryptografiske grundelementer på lavt niveau er sikre; det er ikke bevist. En fejl i de specifikationer, som mennesker har godkendt, ville svække garantien, og WhatsApp og de øvrige apps bruger deres egne versioner af protokollen, så resultatet kan ikke automatisk overføres til dem. Google ville heller ikke fortælle Wired, hvad analysen kostede, eller om virksomheden planlægger at sælge den som en tjeneste.

Signal tog godt imod resultatet. »I takt med at AI-drevne sikkerhedstrusler vokser, giver en grundig verificering af Signal-protokollens implementering os endnu større tillid til vores kodes garantier for privatlivets fred,« sagde Ehren Kret, Signals teknologidirektør, i en udtalelse. DeepMind-forskeren Swarat Chaudhuri var mere forbeholden og sagde til Wired, at der er »lang vej igen«, før metoden kan skaleres »til al software i verden«.

For alle, der bruger Signal, er der ikke noget, der skal installeres, og ingen indstilling, der skal ændres. Beviset handler om kode, som allerede findes i appen.

DeepMind offentliggjorde arbejdet den 10. november sammen med en teknisk artikel og har udgivet specifikationerne og beviserne som open source på GitHub. Projektet med Signal beskrives som en milepæl på vejen mod en stor udfordring inden for formel verificering, der blev lanceret i april. DeepMind nævner firmware til medicinsk udstyr og software til elnettet som eksempler på systemer, virksomheden gerne vil kontrollere som det næste.

Chaudhuri trak også en grænse for, hvor stor en del af arbejdet maskinerne bør stå for. »Vi ønsker ikke sådan en vibe-verden, hvor AI opstiller målene, og AI skaber beviserne,« sagde han til Wired. Mennesker afgør stadig, hvad der tæller som sikkert, og AI beviser det blot.

Tags: cybersikkerhed, Google DeepMind, AlphaProof Code, end-to-end-kryptering, formel verifikation, libsignal