Google DeepMind berättade om resultatet den 10 november i ett blogginlägg och en teknisk artikel. Wired och ZDNet rapporterade samma dag utifrån bolagets pressmeddelande och intervjuer. De bekräftar alltså inte resultaten oberoende.

Signal-protokollet krypterar meddelanden i Signal-appen och Google Messages, och enligt Wired och ZDNet även i WhatsApp. DeepMind uppger att agenterna bevisade egenskaperna inte bara för protokollets utformning utan för själva implementationen. Bolaget motiverar det med att verkliga sårbarheter ofta döljer sig i skillnaderna mellan utformning och implementation.

Människor specificerade, agenter bevisade

Vid formell verifiering testas programmet inte bara, utan man visar matematiskt att det fungerar enligt specifikationen i alla lägen. Beviset omfattar alltså bara det som står i specifikationen.

I AlphaProof Code formulerade forskarna först Signals säkerhetsmål som matematiska specifikationer med hjälp av flera språkmodeller. Experter granskade varje specifikation. Därefter skrev AI-agenter som drivs av DeepMinds modell Gemini Carbon bevisen, sammanlagt över sex miljoner rader Lean. Lean är ett programmeringsspråk där datorn kontrollerar varje steg i ett bevis.

Agenterna gick dessutom igenom bevisen och markerade en procent av koden för mänsklig granskning. Resten kontrollerar Lean automatiskt.

”Vi vill inte ha en sådan här vibbvärld där AI genererar både målen och bevisen och i princip skriver sina egna prov”, sade DeepMind-forskaren Swarat Chaudhuri till Wired.

Vad som bevisades och vad som lämnades utanför

Enligt DeepMind bevisades egenskaperna för den kompilerade kod som enheterna kör. En av egenskaperna är att meddelandena förblir skyddade både före och efter att en enhet tillfälligt har komprometterats. Granskningen omfattade till exempel inte hela Signals mobilapp, skriver Wired.

Arbetet tog fyra veckor. Bolaget uppger att motsvarande arbete har tagit expertgrupper flera år. DeepMinds forskare påpekar i Wired att Signal Foundations tidigare formella verifiering gav dem ett visst försprång. DeepMind säger att implementationen av ett så allmänt använt protokoll aldrig tidigare har verifierats formellt med någon metod. Signals teknikchef Ehren Kret konstaterar i ett uttalande att den tidigare verifieringen var inriktad på mindre delar av koden.

Enligt Wired hittades inga nya sårbarheter i de granskade delarna av protokollet. I ett test återinförde forskarna två tidigare åtgärdade verkliga buggar i en isolerad version av koden. I båda fallen tog systemet fram ett maskinkontrollerat bevis för att versionen var osäker.

Chaudhuri säger att det är långt kvar innan metoden kan utvidgas till all programvara i världen. Google berättade inte för Wired vad analysen kostade.

Vad som öppnas för andra

DeepMind gör verifieringsmaterialet tillgängligt för andra – enligt Wired specifikationen och beviset. ZDNet skriver i en underrubrik att bolaget också planerar att öppna själva AlphaProof Code, men DeepMinds pressmeddelande nämner bara verifieringsmaterialet. Google kommenterade inte om en kommersiell produkt är på väg, uppger Wired.