Google DeepMind använder AI-agenter för att verifiera Signals centrala maskinkod

Google DeepMind introducerade AlphaProof Code den 10 november 2026 och använde team av AI-agenter för att ta fram maskinkontrollerade Lean-bevis för angivna säkerhetsegenskaper hos Signals kompilerade libsignal-kod. Den fem personer starka forskargruppen slutförde bevisarbetet på fyra veckor och offentliggjorde specifikationerna och verifieringsunderlagen för extern granskning.

Arbetet gick från en abstrakt modell av Signals protokolldesign till den kompilerade implementationen. Forskarna bäddade in de oförändrade crate-paketen libsignal v0.105.4 och SPQR v1.6.0 i ett litet kommandoradsprogram och använde sedan standardversionen av rustc för att bygga en statiskt länkad körbar fil för AArch64 Linux. Den tekniska artikeln beskriver resultatet som de första säkerhetsbevisen på protokollnivå för den oförändrade koden i en brett använd kryptografisk protokollimplementation.

Så fördelade AlphaProof Code arbetet

Fem forskare ägnade fyra veckor åt bevisarbetet och lät agenter arbeta kontinuerligt på sina arbetsstationer samtidigt som de tog fram symboliska bevis och beräkningsbevis parallellt. Enligt artikeln genererade agenterna omkring 6,5 miljoner rader maskinkontrollerad Lean-beviskod, som byggde på ungefär 26 000 rader betrodda specifikationer och AArch64-semantik.

Människor valde egenskaperna, löste tvetydigheter och avvägningar kring säkerheten, granskade specifikationerna och behöll det slutliga godkännandet. Agenter som drevs av Gemini 4 Carbon och Claude Opus 5.5 utformade och granskade specifikationerna, bland annat genom granskning med en modell från en annan modellfamilj. Agentteam med Gemini 4 Carbon genererade sedan all beviskod; ingen av författarna skrev någon beviskod. Typiska körningar använde 40 till 80 agenter på en och samma maskin under 24 till 72 timmar. En orkestrerare och teamledare samordnade bevisarbetarna, medan arkitekt- och integratörsrollerna underhöll den gemensamma bevisbasen.

En kontrollfunktion godkände ett bevis först efter att Leans kärna hade kontrollerat det och ett jämförelseverktyg bekräftat att det stämde överens med den undanhållna, människogodkända specifikationen, inklusive alla transitiva definitioner, och att endast Leans standardaxiom hade använts. Agenterna kunde föreslå mindre ändringar när bevisen blottlade problem i specifikationerna, men ändringar av betrodda antaganden krävde mänskligt godkännande eller en policy som användaren hade ställt in, och loggfördes med motiveringar. Kontrollen hanterar en dokumenterad risk med agentgenererade bevis: en specifikation kan försvagas indirekt genom en av sina definitioner.

Säkerhetstäckning och tester med historiska buggar

Det verifierade målet var kod för en-till-en-sessioner som omfattade PQXDH-handskakningen och meddelandehantering med Triple Ratchet. Forskarna redovisar två oberoende argument: tio symboliska teorem under idealiserade kryptografiska antaganden och ett beräkningsbevis som begränsar en angripares fördel med hjälp av kryptografiska antaganden och statistiska storheter. Egenskaperna omfattar framåtsekretess, som skyddar tidigare meddelanden om det aktuella tillståndet stjäls; autentisering; säkerhet efter kompromettering, som handlar om återhämtning efter en kompromettering; samt sekretess för handskakningen. Det symboliska argumentet omfattar dessutom sekretess för handskakningen även efter ett senare Diffie–Hellman-genombrott.

För att testa om specifikationerna kunde upptäcka verkliga fel återställde teamet två tidigare åtgärdade buggar i libsignal, kallade ”weak state” och ”small subgroup”, genom att omvända korrigeringarna och kompilera de ändrade binärfilerna på nytt. I båda fallen tog teamet fram Lean-bevis för att det symboliska säkerhetsteoremet inte höll. Det offentliga verifieringsarkivet delar upp materialet i beräkningsbevis, symboliska bevis, gemensamma binärfiler och AArch64-semantik och beskriver hur man bygger om och kontrollerar bevisen oberoende.

Signals teknikchef Ehren Kret sade att arbetet ”ger oss ännu större förtroende för integritetsskyddet i vår kod”.

Begränsningar och nästa steg

Garantierna räcker inte på långa vägar till att certifiera Signals fullständiga appar. De gäller forskarnas libsignal-cli-bygge när det körs som en ny process. Nyckelgenerering verifierades inte, gruppmeddelanden lämnades till framtida arbete och sidokanaler samt tillstånd för flera enheter ingår inte i scenariot. Kryptografiska primitiver på låg nivå och utvalda utdata- och biblioteksrutiner representeras av betrodda kontrakt. Resultatet är därför också beroende av dessa kontrakt, de godkända specifikationerna, Leans kärna, AArch64-semantiken och antagandena om primitiverna.

Artikeln framhåller att inget av argumenten bevisar den postkvantumåterhämtning som SPQR är utformat för att tillföra: beräkningsteoremet omfattar klassiska angripare, medan angriparen i de symboliska ratchet-teoremen får välja SPQR-nycklar. Den beräkningsmässiga modellen begränsar också flera av angriparens handlingar och blir innehållslös när antalet meddelanden och sessioner blir tillräckligt stort. Dessa avgränsningar anger vad en extern granskare måste lita på innan de maskinkontrollerade bevisen kan betraktas som en säkerhetsgaranti för en viss driftsättning.

Forskarnas angivna nästa steg är att stärka teoremen, minska den betrodda basen genom att verifiera fler hookade rutiner och koppla kryptografiska kontrakt till verifierade implementationer samt utöka täckningen till gruppmeddelanden, Sealed Sender och protokoll på serversidan. Målet att verifiera nya versioner av libsignal före lansering är ett forskningsmål, inte en aviserad driftsättning.

Resultatets omedelbara betydelse ligger i den arbetsfördelning det visar: agenterna stod för beviskonstruktionen, medan tillförlitligheten fortfarande bygger på specifikationer som granskats av människor och på uttryckliga antaganden. Genom att offentliggöra bevisen och kontrollprocedurerna får externa granskare möjlighet att pröva den grunden, samtidigt som forskarna arbetar med att föra in arbetsflödet i den löpande utvecklingen av libsignal.