Google DeepMind bruker KI-agenter til å verifisere Signals sentrale maskinkode

Google DeepMind lanserte AlphaProof Code 10. november 2026. Teamet brukte KI-agenter til å lage maskinkontrollerte Lean-bevis for angitte sikkerhetsegenskaper i Signals kompilerte libsignal-kode. Det fem personer store forskerteamet fullførte bevisarbeidet på fire uker og offentliggjorde spesifikasjonene og verifiseringsmaterialet for ekstern gjennomgang.

Arbeidet gikk fra en abstrakt modell av Signals protokolldesign til den kompilerte implementasjonen. Forskerne pakket de uendrede crate-pakkene libsignal v0.105.4 og SPQR v1.6.0 inn i et lite kommandolinjeverktøy og brukte deretter standardversjonen av rustc til å bygge en statisk lenket kjørbar fil for AArch64 Linux. Den tekniske artikkelen beskriver resultatet som de første sikkerhetsbevisene på protokollnivå for den uendrede koden i en mye brukt implementasjon av en kryptografisk protokoll.

Slik fordelte AlphaProof Code arbeidet

Fem forskere brukte fire uker på bevisarbeidet og lot agenter kjøre kontinuerlig på arbeidsstasjonene sine mens de arbeidet parallelt med symbolske og beregningsbaserte bevis. Ifølge artikkelen genererte agentene rundt 6,5 millioner linjer maskinkontrollert Lean-beviskode, basert på om lag 26 000 linjer med betrodde spesifikasjoner og AArch64-semantikk.

Mennesker valgte egenskapene, avklarte tvetydigheter og avveininger knyttet til sikkerhet, gjennomgikk spesifikasjonene og beholdt den endelige godkjenningsmyndigheten. Agenter drevet av Gemini 4 Carbon og Claude Opus 5.5 utarbeidet og gjennomgikk spesifikasjonene, også med en gjennomgang utført av en annen modellfamilie. Agentteam drevet av Gemini 4 Carbon genererte deretter all beviskoden; ingen av forfatterne skrev beviskode. Typiske kjøringer brukte 40 til 80 agenter på én maskin i 24 til 72 timer. En orkestrator og teamledere koordinerte agentene som utarbeidet bevis, mens arkitekt- og integratørrollene vedlikeholdt den delte bevisbasen.

En kontrollmekanisme godkjente et bevis først etter at Leans kjerne hadde kontrollert det, og en sammenligningsmekanisme hadde bekreftet at det stemte med den tilbakeholdte, menneskegodkjente spesifikasjonen, inkludert alle transitive definisjoner, og bare brukte Leans standardaksiomer. Agentene kunne foreslå mindre endringer når bevis avdekket problemer i spesifikasjonene, men endringer i betrodde forutsetninger krevde godkjenning fra et menneske eller en policy fastsatt av brukeren, og ble loggført med begrunnelser. Kontrollmekanismen håndterer en dokumentert risiko ved agentgenererte bevis: En spesifikasjon kan svekkes indirekte gjennom en av definisjonene sine.

Sikkerhetsdekning og tester med historiske feil

Det som ble verifisert, var koden for én-til-én-økter, som dekker PQXDH-håndtrykket og meldingsutveksling med Triple Ratchet. Forskerne rapporterer to uavhengige bevis: ti symbolske teoremer basert på idealiserte kryptografiske forutsetninger og et beregningsbasert bevis som avgrenser en angripers fordel ved hjelp av kryptografiske forutsetninger og statistiske ledd. Egenskapene omfatter fremoverskuende hemmelighold, som beskytter tidligere meldinger dersom den nåværende tilstanden blir stjålet; autentisering; sikkerhet etter kompromittering, som handler om gjenoppretting etter et kompromiss; og hemmelighold i håndtrykket. Det symbolske beviset dekker i tillegg hemmelighold i håndtrykket etter et senere Diffie–Hellman-brudd.

For å undersøke om spesifikasjonene kunne fange opp reelle feil, rullet teamet tilbake rettelsene for to tidligere utbedrede libsignal-feil, kjent som «svak tilstand» og «liten undergruppe», og kompilerte de endrede binærfilene på nytt. I begge tilfellene utarbeidet teamet Lean-bevis som viste at det symbolske sikkerhetsteoremet ikke holdt. Det offentlige verifiseringsarkivet skiller mellom materialet for beregningsbaserte bevis, symbolske bevis, den delte binærfilen og AArch64-semantikken, og forklarer hvordan bevisene kan bygges på nytt og kontrolleres uavhengig.

Signals teknologidirektør Ehren Kret sa at arbeidet «gir oss enda større tillit til personverngarantiene i koden vår».

Begrensninger og neste steg

Garantiene rekker langt fra til å sertifisere hele Signal-applikasjoner. De gjelder forskernes libsignal-cli-bygg, kjørt som en ny prosess. Nøkkelgenerering ble ikke verifisert, gruppemeldinger er utsatt til framtidig arbeid, og sidekanaler og tilstanden på flere enheter faller utenfor scenarioet. Lavnivå kryptografiske primitiver samt utvalgte utdata- og biblioteksrutiner er representert ved betrodde kontrakter. Resultatet avhenger derfor også av disse kontraktene, de godkjente spesifikasjonene, Leans kjerne, AArch64-semantikken og forutsetninger om primitivene.

Artikkelen slår fast at ingen av bevisene dokumenterer den postkvantehevingen SPQR er ment å tilføre: Det beregningsbaserte teoremet omfatter klassiske angripere, mens de symbolske ratchet-teoremene lar angriperen velge SPQR-nøkler. Den beregningsbaserte modellen begrenser også flere av angriperens handlinger og blir innholdsløs når antallet meldinger og økter blir tilstrekkelig stort. Disse grensene viser hva en ekstern kontrollør må ha tillit til før de maskinkontrollerte bevisene kan regnes som en sikkerhetsgaranti for en bestemt utrulling.

Forskerne oppgir at de neste stegene er å styrke teoremene, redusere mengden kode man må ha tillit til ved å verifisere flere tilkoblede rutiner og knytte kryptografiske kontrakter til verifiserte implementasjoner, samt utvide dekningen til gruppemeldinger, forseglet avsender og protokoller på serversiden. Målet om å verifisere nye libsignal-utgivelser før de sendes ut, er et forskningsmål, ikke en varslet utrulling.

Den umiddelbare betydningen av resultatet er arbeidsdelingen det viser: Agentene håndterte konstruksjonen av bevisene, mens tilliten fortsatt hviler på spesifikasjoner som er gjennomgått av mennesker, og på eksplisitte forutsetninger. Ved å offentliggjøre bevisene og kontrollprosedyrene får eksterne fagfeller mulighet til å prøve dette grunnlaget mens forskerne arbeider med å innlemme arbeidsflyten i den løpende utviklingen av libsignal.