Signals kryptering klarade ett AI-bevis på 6,5 miljoner rader

Signals krypteringskod har nu något som nästan ingen annan programvara med bred användning kan visa upp: ett matematiskt bevis för att den gör det den lovar. En grupp AI-agenter gick igenom libsignal, biblioteket som driver Signal-protokollet, och bevisade att enskilda chattar förblir hemliga, bekräftar vem som finns på andra sidan och åter stänger ute en angripare efter att en nyckel har stulits. De hittade inga nya sårbarheter.

Det här har betydelse långt utanför Signals egna användarkrets. Protokollet är den globala standarden för totalsträckskrypterade meddelanden, och varianter av det skyddar chattar i WhatsApp, Messenger och Google Messages. Att granska verklig, driftsatt kod så här grundligt brukade ta så lång tid att nästan ingen försökte: en av fältets största framgångar, en verifierad operativsystemskärna, tog tjugo personår. Det här arbetet tog fyra veckor.

Verktyget, som utvecklats av Google DeepMind, heter AlphaProof Code. Först omvandlade mänskliga experter och AI-modeller Signals säkerhetsmål till formella påståenden i Lean, ett programmeringsspråk utvecklat för matematiska bevis, och en människa granskade vart och ett av dem. Därefter skrev grupper med 40 till 80 agenter, drivna av Gemini Carbon, bevisen. De arbetade i 24 till 72 timmar åt gången på en enda maskin. Resultatet är omkring 6,5 miljoner rader Lean-kod.

Ingen behöver lita på de miljontals raderna. Leans kärna kontrollerar varje steg och underkänner alla bevis som inte håller, så det spelar ingen roll vilken modell som skrev beviset eller hur många gånger den gjorde fel på vägen. Det människor faktiskt måste lita på är betydligt mindre: omkring 26 000 rader specifikationer och en modell av hur en ARM-processor kör kod.

Bevisen omfattar de delar av Signal som skyddar en konversation: handskakningen PQXDH, som upprättar en chatt, och Triple Ratchet, som byter nyckel för varje meddelande, inklusive det postkvantumskikt som ska stå emot framtida kvantdatorer. I praktiken innebär det att en stulen telefons aktuella nycklar inte låser upp äldre meddelanden, och att tjuven åter förlorar åtkomsten när de två parterna utbyter nya nycklar.

För att visa att systemet kan skilja bra kod från dålig återinförde forskarna två äldre, redan åtgärdade buggar i libsignal. Den ena fick biblioteket att behålla en kopia av en hemlig nyckel som det borde ha raderat. I båda fallen tog AlphaProof Code fram ett maskinkontrollerat bevis för att den felaktiga versionen var osäker.

Begränsningarna är verkliga. Beviset omfattar bara en-till-en-sessioner, och DeepMind beskriver gruppmeddelanden som framtida arbete. Det gäller libsignal version 0.105.4, kompilerad med standardkompilatorn för Rust för ARM Linux i ett litet testprogram – inte de fullständiga Signal-apparna för iPhone, Android eller dator. Man utgår från att de kryptografiska byggstenarna på låg nivå är säkra; de har inte bevisats vara det. Ett misstag i specifikationerna som godkänts av människor skulle försvaga garantin, och WhatsApp och de andra apparna kör egna versioner av protokollet, så resultatet gäller inte automatiskt även för dem. Google ville inte heller berätta för Wired vad analysen kostade eller om företaget planerar att sälja den som en tjänst.

Signal välkomnade resultatet. »I takt med att AI-drivna säkerhetshot ökar ger en rigorös verifiering av Signal-protokollets implementation oss ännu större förtroende för de integritetsgarantier vår kod erbjuder«, sade Ehren Kret, Signals teknikchef, i ett uttalande. DeepMinds forskare Swarat Chaudhuri var mer försiktig och sade till Wired att det är »långt kvar« innan metoden kan skalas upp »till all programvara i världen«.

För den som använder Signal finns inget att installera och ingen inställning att ändra. Beviset gäller kod som redan finns i appen.

DeepMind publicerade arbetet den 10 november tillsammans med en teknisk artikel och har gjort specifikationerna och bevisen tillgängliga som öppen källkod på GitHub. Företaget beskriver Signal-projektet som en milstolpe på vägen mot en stor utmaning inom formell verifiering, som presenterades i april, och nämner inbyggd programvara för medicintekniska produkter och programvara för elnät som exempel på system man vill granska härnäst.

Chaudhuri drog också en gräns för hur stor del av arbetet maskinerna bör få ta över. »Vi vill inte ha en sådan här vibe-värld där AI skapar målen och AI skapar bevisen«, sade han till Wired. Människor avgör fortfarande vad som räknas som säkert; AI:n bevisar det bara.

Taggar: cybersäkerhet, Google DeepMind, AlphaProof Code, formell verifiering, libsignal, Signal