Google DeepMind bruger AI-agenter til at verificere Signals centrale maskinkode

Google DeepMind introducerede AlphaProof Code den 10. november 2026 og brugte hold af AI-agenter til at udarbejde maskinkontrollerede Lean-beviser for specificerede sikkerhedsegenskaber i Signals kompilerede libsignal-kode. Det fem personer store forskerhold færdiggjorde bevisarbejdet på fire uger og offentliggjorde specifikationerne og verifikationsmaterialet til ekstern gennemgang.

Arbejdet gik videre end en abstrakt model af Signals protokoldesign og omfattede den kompilerede implementering. Forskerne indpakkede de uændrede libsignal v0.105.4- og SPQR v1.6.0-crates i et lille kommandolinjeværktøj og brugte derefter standardudgaven af rustc til at bygge en statisk linket AArch64 Linux-eksekverbar fil. Den tekniske artikel beskriver resultatet som de første sikkerhedsbeviser på protokolniveau for den uændrede kode i en udbredt implementering af en kryptografisk protokol.

Sådan fordelte AlphaProof Code arbejdet

Fem forskere brugte fire uger på bevisarbejdet og lod agenter køre uafbrudt på deres arbejdsstationer, mens de sideløbende udarbejdede symbolske beviser og beregningsmæssige beviser. Artiklen oplyser, at agenterne genererede omkring 6,5 millioner linjer maskinkontrolleret Lean-beviskode, baseret på cirka 26.000 linjer betroede specifikationer og AArch64-semantik.

Mennesker udvalgte egenskaberne, afklarede tvetydigheder og afvejninger mellem sikkerhedshensyn, gennemgik specifikationerne og beholdt den endelige godkendelse. Agenter drevet af Gemini 4 Carbon og Claude Opus 5.5 udarbejdede og gennemgik specifikationerne, herunder gennemgang med en model fra en anden modelgruppe. Agenthold drevet af Gemini 4 Carbon genererede derefter al beviskoden; ingen af forfatterne skrev beviskode. Typiske kørsler brugte 40 til 80 agenter på én maskine i 24 til 72 timer. En orkestrator og teamledere koordinerede bevisarbejdet, mens arkitekt- og integratorroller vedligeholdt den fælles bevisbase.

En gatekeeper accepterede kun et bevis, når Leans kerne havde kontrolleret det, og en sammenligningsmekanisme havde bekræftet, at det stemte overens med den tilbageholdte, menneskegodkendte specifikation, herunder alle transitivt anvendte definitioner, og kun benyttede Leans standardaksiomer. Agenter kunne foreslå mindre ændringer, når beviser afslørede problemer med specifikationerne, men ændringer af betroede antagelser krævede menneskelig godkendelse eller en politik fastsat af brugeren og blev logført med begrundelser. Kontrollen håndterer en dokumenteret risiko ved agentgenererede beviser: En specifikation kan indirekte svækkes gennem en af dens definitioner.

Sikkerhedsdækning og test af historiske fejl

Det verificerede mål var kode til en-til-en-sessioner, der dækker PQXDH-håndtrykket og meddelelser via Triple Ratchet. Forskerne beskriver to uafhængige argumenter: ti symbolske sætninger under idealiserede kryptografiske antagelser og et beregningsmæssigt bevis, der begrænser en angribers fordel ved hjælp af kryptografiske antagelser og statistiske led. Egenskaberne omfatter fremadrettet hemmeligholdelse, som beskytter tidligere meddelelser, hvis den aktuelle tilstand bliver stjålet; autentificering; sikkerhed efter kompromittering, som handler om genopretning efter et kompromitteringsangreb; og hemmeligholdelse af håndtrykket. Det symbolske argument dækker desuden hemmeligholdelse af håndtrykket efter et senere Diffie–Hellman-brud.

For at undersøge, om specifikationerne kunne opdage reelle fejl, rullede holdet rettelserne af to tidligere afhjulpne libsignal-fejl tilbage, kendt som svag tilstand og lille undergruppe, og kompilerede de ændrede binærfiler igen. I begge tilfælde udarbejdede holdet Lean-beviser for, at den symbolske sikkerhedssætning ikke holdt. Det offentlige verifikationsarkiv adskiller materialet om beregningsmæssige beviser, symbolske beviser, den fælles binærfil og AArch64-semantik og beskriver, hvordan beviserne kan bygges igen og kontrolleres uafhængigt.

Signals teknologidirektør Ehren Kret sagde, at arbejdet “giver os endnu større tillid til vores kodes garantier for beskyttelse af privatlivet”.

Begrænsninger og næste skridt

Garantierne rækker langt fra til at certificere Signals komplette applikationer. De gælder forskernes libsignal-cli-build, der kører som en ny proces; nøglegenerering blev ikke verificeret, gruppemeddelelser blev overladt til fremtidigt arbejde, og sid kanaler samt tilstand på tværs af flere enheder falder uden for scenariet. Lavniveau-kryptografiske primitiver og udvalgte output- og biblioteksrutiner er beskrevet ved hjælp af betroede kontrakter. Resultatet afhænger derfor også af disse kontrakter, de godkendte specifikationer, Leans kerne, AArch64-semantikken og antagelserne om primitiverne.

Artiklen fastslår, at ingen af argumenterne beviser den postkvantegenopretning, som SPQR er udviklet til at tilføje: Det beregningsmæssige teorem dækker klassiske angribere, mens de symbolske ratchet-teoremer lader angriberen vælge SPQR-nøgler. Den beregningsmæssige model begrænser også flere af angriberens handlinger og bliver indholdsløs ved tilstrækkeligt store mængder meddelelser og sessioner. Disse afgrænsninger viser, hvad en ekstern kontrollant skal have tillid til, før de maskinkontrollerede beviser kan betragtes som en sikkerhedsgaranti for en bestemt implementering.

Forskernes beskrevne næste skridt er at styrke teoremerne, mindske den betroede base ved at verificere flere tilkoblede rutiner og forbinde kryptografiske kontrakter med verificerede implementeringer samt udvide dækningen til gruppemeddelelser, Sealed Sender og protokoller på serversiden. Målet om at verificere nye libsignal-versioner før udgivelse er et forskningsmål, ikke en annonceret implementering.

Resultatets umiddelbare betydning er den arbejdsdeling, det viser: Agenterne stod for at konstruere beviserne, mens sikkerheden stadig bygger på specifikationer, der er gennemgået af mennesker, og på eksplicitte antagelser. Ved at offentliggøre beviserne og kontrolprocedurerne får eksterne fagfæller mulighed for at efterprøve dette grundlag, mens forskerne arbejder på at føre arbejdsgangen ind i den løbende udvikling af libsignal.