Forskare vid Google DeepMind har visat att ett AI-system kan bevisa viktiga säkerhetsegenskaper hos meddelandeprotokollet Signal med matematiska metoder. Teamet använde ett nytt ramverk, AlphaProof Code, för att formellt verifiera flera kryptografiska garantier. Arbetet tog omkring fyra veckor och genomfördes som ett forskningsprojekt, inte som en kommersiell produkt. Inga nya buggar hittades i de delar som granskades, och när AI:n kördes på tidigare versioner av protokollet identifierade den korrekt äldre, redan åtgärdade brister.
Formell verifiering innebär att man med matematik kontrollerar att programvara fungerar exakt som avsett, utan utrymme för dolda sårbarheter. Historiskt har processen krävt att experter skriver detaljerade specifikationer, översätter dem till formler och sedan konstruerar ett bevis – ett arbetskrävande moment som kan ta månader. Genom att låta en agentisk AI (en AI som kan sätta upp och arbeta mot egna delmål) göra en stor del av det tunga arbetet kunde DeepMind korta tiden till några veckor. Forskarna säger att AI:n fortfarande behövde mänsklig tillsyn vid viktiga moment, men att den på egen hand kunde föreslå bevis och rätta sina egna misstag.
Signals teknikchef, Ehren Kret, påpekade att tidigare verifieringsarbete bara omfattade små kodfragment. DeepMinds metod gör det möjligt att ”utöka” vad som kan kontrolleras avsevärt, sade han. Teamet publicerar specifikationen och beviset som det tog fram, så att andra grupper kan bygga vidare på arbetet. Resultatet är lovande, men DeepMind varnar för att det fortfarande är en utmaning att skala upp metoden till hela appar eller kompletta programvaruleveranskedjor. Kostnaden för AI-driven verifiering har inte offentliggjorts.
Därför är det viktigt
Om AI på ett tillförlitligt sätt kan bevisa att kryptografiska protokoll är säkra kan vanliga användare av Signal, Google Messages, WhatsApp och liknande appar få större förtroende för att deras meddelanden förblir privata. För företag som är beroende av krypterad kommunikation – banker, vårdgivare och journalister – kan tekniken så småningom ge juridiskt verifierbara garantier för att programvaran inte har några kritiska brister.
Varför det spelar roll
För den vanliga användaren innebär nyheten att krypteringen som skyddar chattarna nu har granskats med ytterligare en matematisk kontroll, vilket minskar risken för dolda buggar. För företag som måste visa att de följer integritetsregler kan AI-stödd verifiering bli ett nytt sätt att påvisa säkerhet utan tidskrävande manuella granskningar.
