Deepmind uppger att AI verifierade Signals krypteringskärna på fyra veckor

Deepmind presenterade AlphaProof Code den 10 november. Forskarna Pushmeet Kohli och Swarat Chaudhuri står bakom Deepminds blogginlägg. Enligt The Decoder bevisar systemet matematiskt att programvara uppfyller sina säkerhetskrav. Forskarna visade tekniken på Signals krypteringsprotokoll.

Så beskrivs metoden

Enligt The Decoder definierade experter först formella säkerhetskrav. Därefter skrev AI-agenter byggda på Googles modell Gemini Carbon bevis i bevisspråket Lean. En bildtext från Deepmind, som The Decoder återger, säger att AI-agenterna hjälper till att ta fram kraven och sedan självständigt bevisar att koden uppfyller dem. Deepminds egen sammanfattning beskriver bevisen som maskingranskade.

The Decoder skriver, med hänvisning till Deepminds blogginlägg, att tidigare verifieringsarbeten kring Signal stannade vid den teoretiska designen. Enligt The Decoder har AlphaProof Code i stället verifierat den faktiska kryptokoden som körs på användarnas enheter. Deepmind skriver i sammanfattningen att de centrala kryptografiska skydden i Signal verifierades ner till maskininstruktioner.

Vad som uppges om omfattningen

Enligt The Decoder skrev agenterna över sex miljoner rader bevis, och cirka en procent flaggades för mänsklig granskning. The Neuron anger 6,5 miljoner rader bevis på fyra veckor. Deepminds sammanfattning nämner över tre miljoner rader maskingranskade bevis. Formuleringen 'över tre miljoner' anger ingen övre gräns och motsäger därför inte nödvändigtvis de andra siffrorna. Vi har inte läst hela blogginlägget och kan inte avgöra varför siffrorna skiljer sig.

Att arbetet normalt tar år är en jämförelse som The Decoder gör. Vi har inte hittat något underlag för den eller någon oberoende mätning.

Testet med buggar

The Decoder skriver att två buggar som planterats avsiktligt för testet fångades direkt. Enligt The Neuron återinförde forskarna två tidigare åtgärdade säkerhetsbuggar för att se om systemet kunde fånga dem. Vi har inte tillgång till detaljer om buggarna.

Signals tekniska chef

Enligt The Decoder säger Signals tekniska chef Ehren Kret att metoden stärker förtroendet för dataintegritet när AI-hoten växer.

Nästa steg

Enligt The Decoder vill Deepmind utvidga metoden till kritisk infrastruktur som elnät och medicintekniska produkter, bland annat via system som CodeMender. Någon tidplan finns inte i de källor vi läst.

Ars Technica rubricerar sin artikel 'Signal's encryption just passed an AI-powered mathematical checkup' och skriver i ingressen att försöket antyder att AI kan göra formell verifiering betydligt mer praktisk. Vi har bara läst rubriken och ingressen. Det som hittills har redovisats är en demonstration på en kodbas, presenterad av Deepmind och återgiven av nyhetssajter.