Google DeepMind uppger att de använde AlphaProof Code för att matematiskt kontrollera viktiga säkerhetsegenskaper i libsignal, referensimplementationen av meddelandeprotokollet Signal. Arbetet tog fyra veckor. Enligt DeepMind har liknande verifiering tidigare krävt flera års arbete av expertgrupper.
Systemet kombinerade mänskliga forskare med AI-agenter. Forskarna och AI:n hjälptes åt att omvandla Signals säkerhetsmål till matematiska specifikationer, som sedan granskades av människor. Därefter genererade agenter som drevs av Gemini Carbon omkring 6.5 miljoner rader Lean-beviskod. Lean är ett programmeringsspråk vars kontrollmekanism kan verifiera att ett matematiskt bevis följer språkets regler. Agenterna flaggade omkring en procent av kodbasen för mänsklig granskning.
Vad omfattade beviset?
Forskarna kontrollerade den kompilerade maskinkoden för libsignals postkvantumhandskakning PQXDH och Triple Ratchet. De bevisade specifika egenskaper, däribland framåtsekretess, autentisering och skydd efter att en enhet har komprometterats. I forskningsartikeln står det att koden kompilerades från oförändrad Rust-kod med en standardkompilator och sedan kontrollerades som AArch64-maskinkod.
Det här går längre än att bevisa att en abstrakt konstruktion är säker: det knyter specificerade säkerhetsgarantier till kompilerad kod. DeepMind kallar det den första formella verifieringen på den här detaljnivån av en implementation av ett brett använt kryptografiskt protokoll. Teamet lade också tillbaka två tidigare åtgärdade buggar i en isolerad version av koden. Systemet tog fram bevis som visade att de buggiga versionerna inte uppfyllde de angivna säkerhetsegenskaperna.
Beviset har begränsningar
Det här är ingen matematisk garanti för att varje del av Signal, eller varje app som använder protokollet, är fri från säkerhetsproblem. Beviset omfattar utvalda egenskaper i libsignal, inte hela appen. Det bygger också på godkända specifikationer, Leans kontrollmekanism och kontrakt för kryptografiska rutiner på låg nivå. The Register påpekar att resultatet inte bevisar den beräkningsmässiga sekretessen hos faktiska meddelandebytes. DeepMinds artikel beskriver bevis i både symboliska och beräkningsmässiga modeller, som bygger på antaganden om de underliggande kryptografiska primitivens egenskaper.
DeepMind uppger att verifieringsmaterialet görs tillgängligt för andra. Företaget hoppas kunna använda metoden inom områden som fast programvara för medicintekniska produkter och programvara för elnät, men säger att det krävs mer forskning för att skala upp metoden. Arbetet är ett steg mot att kontrollera mer verklig kod, inte ett belägg för att de andra systemen har verifierats.
Varför det spelar roll
För personer som använder Signal innebär arbetet ett maskinkontrollerat bevis för vissa säkerhetsegenskaper i protokollets centrala implementation. Det visar inte att hela appen är fri från buggar, och beviset bygger på antaganden om kryptografiska komponenter.
