DeepMinds AI har verifierat utvalda delar av Signal-protokollet
Forskare på Google DeepMind har med AI-ramverket AlphaProof Code formellt verifierat utvalda säkerhetsegenskaper i Signal-protokollet. Studien tog fyra veckor, beskrivs som ett proof of concept och gällde inte hela appen. Wired anger att det långsiktiga målet är att göra detsamma för "all världens mjukvara".
Källor 3 källor
- MediumWired (endast rubrik och ingress i uppdraget, artikeln gick inte att öppna)wired.com ↗
- MediumKantan Newskantan.news ↗
- MediumStartup Fortunestartupfortune.com ↗
Google DeepMind har använt ett AI-system kallat AlphaProof Code för att formellt verifiera centrala kryptografiska garantier i Signal-protokollet. Wired rubricerar det som att verktyget bevisat att protokollet är säkert, och i ingressen beskrivs det som att forskarna verifierat att protokollet fungerar som avsett. Vi har bara kunnat läsa Wired-rubriken och ingressen, så uppgifterna nedan bygger på Kantan News och på ingressen till Startup Fortune [1][2][3].
Formell verifiering innebär att man med matematiska bevis visar att programvara uppfyller ett angivet krav. Enligt Kantan News har det traditionellt krävt månader av arbete från experter, eftersom kodens egenskaper först ska översättas till formler och bevisen sedan tas fram. Kantan News skriver att DeepMinds agentbaserade system kortat tiden genom att automatisera sökandet efter bevis [2].
Vad som verifierades – och vad som inte gjorde det
Granskningen avsåg inte hela Signal-appen. Enligt Kantan News analyserades kritiska delar av det kryptografiska protokollet, inte appens hela kodbas, och studien beskrivs som ett proof of concept [2]. Startup Fortune skriver att det handlade om utvalda garantier och att forskarna inte hittade några nya sårbarheter i de delar de granskade [3].
För att testa verktyget körde forskarna det enligt Kantan News även på äldre Signal-versioner med kända, sedan åtgärdade sårbarheter. Systemet identifierade dem och visade att protokollet i det skicket inte gick att verifiera [2].
Människor kvar i processen
Enligt Kantan News beskriver forskarna arbetssättet som samarbete mellan människa och AI. AI-agenterna tar fram lösningar och kontrollerar sina egna fel, medan mänskliga experter övervakar vid kritiska kontrollpunkter [2].
Signal Foundations tekniska chef Ehren Kret uppges enligt Kantan News ha sagt att tidigare verifieringsarbeten gällt små kodstycken, medan DeepMinds metod gett mycket bredare täckning. Han ska också ha sagt att det är av stor vikt att matematiskt bekräfta protokollets integritetsgarantier när AI-drivna hot ökar [2].
DeepMind har enligt Startup Fortune publicerat specifikationen och beviset [3]. Kantan News skriver att materialet är tillgängligt för oberoende forskare att granska [2].
Öppna frågor om kostnad och skala
Google har enligt Startup Fortune inte velat uppge vad projektet kostade eller om man planerar att sälja verktyget [3]. Enligt Kantan News är det en pågående fråga i branschen om metoden kan anpassas kostnadseffektivt till kommersiella leveranskedjor och finansiella system [2]. Hur väl metoden fungerar på stora kodbaser är alltså inte känt utifrån de källor vi läst.
- Exakt vilka delar av Signal-protokollet och vilka garantier som verifierades, och vilka antaganden och vilket bevissystem som användes. Det framgår inte av de källor vi kunnat läsa.
- Vad projektet kostade och om Google tänker erbjuda verktyget kommersiellt. Google uppges inte vilja säga det.
- Om metoden fungerar på större och mer komplexa kodbaser.
Har vi fel? Skicka en rättelse.