DeepMinds AI-agenter beviste Signals sikkerhed matematisk på fire uger

MA Martin Mensbo Christiansen · 11. november 2026 · 9 min læsning

Programkode på en computerskærm i bevægelsesslør med orange lys

Google DeepMind offentliggjorde 10. november AlphaProof Code, en ramme hvor AI-agenter matematisk beviste, at den faktiske kode bag Signal-protokollen holder det, den lover. Det er efter DeepMinds egne ord første gang, implementeringen af en så udbredt krypteringsprotokol er formelt verificeret med nogen metode, med eller uden AI. Signal-protokollen beskytter samtaler i blandt andet Signal-appen, WhatsApp, Messenger og Google Messages.

Historien er ikke endnu et cyberangreb. AI bruges i stigende grad til at finde og udnytte sårbarheder. Her går det den anden vej: agenterne leverer et matematisk bevis for, at koden er sikker. Vi har læst DeepMinds annoncering og hele den tekniske artikel, og gennemgangen herunder forklarer, hvad der blev bevist, hvordan mennesker og AI-agenter deler arbejdet, hvad beviset ikke dækker, og hvad det betyder for jeres egen softwaresikkerhed.

Hvad DeepMind og Signal har bevist

Formel verifikation er at skrive præcist ned, hvad et stykke software skal garantere, og derefter bevise matematisk, at det altid gør det. Et bevis udelukker enhver fejl eller ethvert angreb, der ville bryde de egenskaber, i modsætning til en test, der kun afprøver de tilfælde, nogen har tænkt på. Det er den højeste form for sikkerhedsgaranti, men det har historisk været så dyrt, at kun ganske få systemer har fået det.

Ifølge DeepMinds annoncering brugte fem forskere en gruppe AI-agenter til at bevise de centrale sikkerhedsegenskaber ved libsignal, referenceimplementeringen af Signal-protokollen, hele vejen ned til den kompilerede maskinkode. Det afgørende er netop dybden. De fleste tidligere analyser stopper ved protokollens design, altså den abstrakte beskrivelse. Her er beviset ført helt ned til den uændrede kode, der rent faktisk kører på enheder, for libsignal version 0.105.4. Rigtige sårbarheder gemmer sig ofte i springet mellem design og implementering, og det er præcis det spring, agenterne har lukket.

Beviserne dækker Signals post-kvante-handshake PQXDH og den såkaldte Triple Ratchet, og de etablerer fire egenskaber: forward secrecy (gamle beskeder forbliver hemmelige, selv om en nøgle senere lækker), post-compromise security (sikkerheden kommer tilbage efter en midlertidig kompromittering), autentificering og handshake-hemmeligholdelse, også mod en fremtidig angriber med en kvantecomputer. Som en kontrol genindførte forskerne to tidligere rettede fejl i en isoleret udgave af koden. I begge tilfælde producerede systemet et maskintjekket bevis for, at den fejlbehæftede version var usikker. Beviset kan altså skelne sikker kode fra usikker kode.

Sådan deler menneske og AI-agenter arbejdet

AlphaProof Code er bygget på et simpelt princip: mennesker bestemmer, hvad der skal bevises, og AI-agenter beviser det. Arbejdet falder i tre trin. Først oversætter mennesker sammen med en gruppe modeller Signals sikkerhedsmål til en formel specifikation i sproget Lean, og menneskelige eksperter gennemgår og godkender hver eneste. Dernæst kompileres den uændrede kode med standardcompileren, og den kørbare maskinkode læses ind sammen med en formel model af processoren. Til sidst beviser et hold af agenter, at koden lever op til specifikationen.

Selve bevisarbejdet udføres af et multi-agent-system, hvor hver AI-agent har sin rolle: en orkestrator fordeler opgaver, teamledere holder styr på større delmål, og en integrator samler de beviste dele. Agenterne er drevet af Gemini Carbon. I DeepMinds kampagner kørte et hold typisk 40 til 80 agenter på én maskine i 24 til 72 timer.

unnamed

Det vigtige for tilliden er, hvad der skal stoles på, og hvad der ikke skal. Agenternes millioner af linjer bevis er ikke betroet. En endelig vagthund, en komponent kaldet gatekeeper, godkender kun et bevis, hvis Leans kerne kontrollerer det mod en låst kopi af specifikationen. Logiske fejl i et agentbevis bliver afvist af kernen. Garantien afhænger derfor ikke af, at agenterne arbejder fejlfrit, men kun af specifikationen, Lean-kernen og modellen af maskinen. End ikke Rust-compileren behøver at være betroet. Det er det samme mønster, vi har set andre steder i branchen, hvor en uafhængig maskine kontrollerer agenternes arbejde, fremfor at AI både sætter målene og vurderer sig selv. Vi har tidligere beskrevet, hvordan OpenAI bruger flere lag til at overvåge sine egne AI-agenter.

Mønsteret løser samtidig et velkendt problem med sprogmodeller. En model kan finde på et bevis, der ser rigtigt ud, men ikke er det, og netop den slags AI-hallucinationer fanges, fordi Lean-kernen afviser alt, der ikke holder. At spørgsmålet om, hvilken model der faktisk svarede, også kan gøres til noget, man kan bevise, har vi set i et andet stykke forskning om beviselig inferens.

Tallene: 6,5 millioner linjer bevis på fire uger

Ifølge den tekniske artikel skrev agenterne omkring 6,5 millioner linjer maskintjekket Lean-bevis. De hviler på omkring 26.000 linjer betroet specifikation og processormodel, altså den del, et menneske skal læse og stole på. Agenterne auditerede selv beviset og markerede kun cirka én procent af arbejdet til en ekstra menneskelig gennemgang, fordi Lean automatisk tjekker resten.

Det tog fire uger. Til sammenligning tog den formelle verifikation af seL4-mikrokernen, et af feltets største resultater, tyve årsværk, og CompCert-compileren tog seks. Og i de tilfælde var koden skrevet specifikt med verifikation for øje. Her er det modsat: agenterne arbejdede på eksisterende produktionskode, som de ikke måtte ændre for at gøre beviset lettere. Det er den kombination, der gør resultatet bemærkelsesværdigt. Hvis omkostningen ved formel verifikation falder fra årsværk til uger, ændrer det, hvilke systemer der realistisk kan få den slags garanti.

Et vigtigt forbehold: DeepMind har ikke offentliggjort en pris for arbejdet. Beviserne og specifikationerne er lagt frit tilgængeligt som open source, så andre kan efterprøve dem, men regningen for selve computerkraften er ikke oplyst. For en virksomhed, der overvejer det samme på egen kode, er det stadig et åbent spørgsmål, hvad det koster.

Det beviset ikke dækker

Et bevis er kun så stærkt som det, man har bevist, og her er flere klare grænser. Kun én-til-én-samtaler er verificeret, ikke gruppebeskeder, som forskerne lader stå som fremtidigt arbejde. Beviset kører gennem en lille kommandolinjeudgave af libsignal, ikke Signals egne mobilapps, selv om den samme kode kører på Android og iPhone. Det stærkeste punkt og den største begrænsning er det samme sted.

Arbejdet foregår i to modeller af sikkerhed. Den symbolske model, hvor ti sætninger bevises, antager perfekt kryptografi og dækker også en fremtidig kvanteangriber. Den beregningsmæssige model giver en konkret grænse for en angribers chancer, men dækker kun klassiske angribere, ikke kvantecomputere. De underliggende kryptografiske byggeklodser, som AES og de enkelte Diffie-Hellman-operationer, er beskrevet via kontrakter og ikke bevist. Garantien er altså betinget af, at de byggeklodser er sikre. Nøglegenerering er heller ikke verificeret.

Den vigtigste pointe, forskerne selv fremhæver, er at det svære nu er specifikationen snarere end selve beviset. En specifikation, der antager for meget om inputtet eller kræver for lidt af resultatet, kan holde selv for fejlbehæftet kode. Det er her, det menneskelige arbejde nu ligger, og det er også her, en fejl ville svække garantien, uden at nogen maskine fanger det.

Hvorfor det betyder noget for AI-sikkerhed

Resultatet skal ses i en større sammenhæng, hvor AI i stigende grad bruges offensivt. Vi har beskrevet, hvordan OpenAIs cybermodel fandt 948 veje til root i Linux, og hvordan de store laboratorier holder deres stærkeste cybermodeller tilbage, fordi de samme evner kan bruges til angreb. AlphaProof Code peger på den defensive modvægt. Hvor en cybermodel finder fejl hurtigere, leverer et bevis noget andet: en garanti for, at hele klasser af fejl slet ikke findes i koden.

Arbejdet er samtidig et skridt mod en offentlig udfordring, som Beneficial AI Foundation stillede i april 2026, om at verificere Signals protokol og app med Lean. DeepMind kobler det eksplicit til forsvarsagenter som CodeMender og til behovet for at kunne modstå den hastighed og skala, som AI-drevne cyberangreb nu kan opnå. Signals tekniske direktør Ehren Kret kalder det et gennembrud at kunne oversætte kørende kode til gyldige Lean-teoremer, og siger, at det giver større tillid til, at koden holder sine løfter om privatliv.

For jer er den praktiske læring todelt. Dels viser det, hvor AI-assisteret formel verifikation er på vej hen for sikkerhedskritiske komponenter. Dels er selve arbejdsdelingen værd at tage med hjem: mennesker godkender, hvad der skal gælde, agenter udfører det tunge arbejde, og en uafhængig maskine kontrollerer resultatet. Det mønster kan overføres til jeres egne agent-arbejdsgange, hvor det sjældent er klogt at lade en agent både sætte målet og bedømme sit eget svar.

Hvad det betyder for danske virksomheder

Det her er forskning, ikke et produkt, I kan købe i dag. Der er derfor intet akut at gøre. Men retningen er relevant, og der er konkrete ting at tage fat på.

Følg feltet, hvis I bygger eller sælger sikkerhedskritisk software som betaling, kryptering eller adgangskontrol. Billigere formel verifikation kan på sigt blive et stærkt argument over for kunder, revisorer og myndigheder.
Kortlæg, hvor i jeres kode et bevis ville give mere værdi end endnu en test. Det er typisk de få komponenter, hvor en enkelt fejl rammer mange på én gang.
Overfør arbejdsdelingen til jeres AI-agenter nu: lad et menneske definere og godkende, hvad der skal gælde, og byg en uafhængig kontrol af agentens output ind, fremfor at stole på agenten selv.
Stil leverandørkrav. Spørg, hvordan jeres leverandører sikrer kode, der er skrevet eller gennemgået af AI, og hvad deres kontrol hviler på.

På reguleringssiden skruer EU's Cyber Resilience Act og NIS2 op for kravene til sikker software og håndtering af sårbarheder. Billigere formel verifikation kan blive et konkret værktøj til at dokumentere, at kritiske komponenter holder, hvad de lover. For organisationer, der bruger end-to-end-krypteret kommunikation, er Signal-eksemplet desuden en påmindelse om, at sikkerheden i praksis afhænger af hele systemet, ikke kun protokollen. Vi gennemgår de nærliggende AI-regler i vores guide til EU AI Act.

Ofte stillede spørgsmål

Hvad er formel verifikation, og hvordan adskiller det sig fra test?

Test afprøver de tilfælde, nogen har skrevet en test for, og kan vise, at der er fejl, men ikke at der ikke er nogen. Formel verifikation skriver præcist ned, hvad softwaren skal garantere, og beviser matematisk, at den altid gør det. Et bevis udelukker enhver fejl eller ethvert angreb, der ville bryde de egenskaber. Til gengæld er det kun så stærkt som specifikationen, man beviser.

Betyder det, at Signal nu er fuldstændig sikker?

Nej. Beviset dækker centrale sikkerhedsegenskaber ved én-til-én-samtaler i libsignal, ikke gruppebeskeder, ikke selve mobilapperne og ikke de underliggende kryptografiske byggeklodser, som beskrives via kontrakter frem for at blive bevist. Garantien er betinget af, at de byggeklodser er sikre, og af, at specifikationen er korrekt. Det er et stort skridt, men ikke et bevis for at alt ved Signal er fejlfrit.

Kan min virksomhed bruge AlphaProof Code?

Ikke uden videre. AlphaProof Code er et forskningsprojekt, og DeepMind har ikke lanceret et produkt eller oplyst en pris. Specifikationer og beviser er dog lagt frit tilgængeligt som open source, så metoden kan studeres. For de fleste virksomheder er det relevante lige nu at følge feltet og overveje, hvor i egen kode et bevis ville give mere end en test.

Hvad har det med EU-regler at gøre?

Ikke direkte. Nyheden udløser ingen GDPR- eller AI Act-forpligtelser i sig selv. Men EU's Cyber Resilience Act og NIS2 stiller skærpede krav til sikker software og håndtering af sårbarheder, og billigere formel verifikation kan blive et værktøj til at dokumentere, at kritiske komponenter er sikre.

Signal fik et stempel. Men det interessante er prisen. Matematisk sikkerhed har hidtil kostet årevis af specialistarbejde, og her blev et bevis ført på fire uger af mennesker og agenter i fællesskab. Det flytter grænsen for, hvilken software der kan få den højeste form for garanti. Samtidig er beviset holdt op med at være det svære. Nu er det specifikationen, altså præcist at beskrive, hvad sikker egentlig betyder. Den opgave kræver stadig mennesker, og det er værd at huske, næste gang en agent tilbyder at bedømme sit eget arbejde.

Fortsæt læsningen

Lange rækker af blå indkøbsvogne med røde håndtag under gadelys om aftenen