# DeepMind lät AI kontrollera Signals kryptografiska kod

> AlphaProof Code kontrollerade viktiga säkerhetsegenskaper i kompilerad Signal-kod på fyra veckor. Beviset gäller vissa garantier, inte alla delar av Signal.

Oossa · 2026-11-11 · https://oossa.com/sv/deepmind-used-ai-to-verify-signal-s-cryptographic-code

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.

## Fakta

- Google DeepMind presenterade AlphaProof Code den November 10, 2026.
- Systemet genererade omkring 6.5 miljoner rader Lean-beviskod i arbetet med libsignal.
- Verifieringen omfattade handskakningen PQXDH och Triple Ratchet i kompilerad AArch64-maskinkod.
- Forskarna återinförde två tidigare åtgärdade buggar, och systemet bevisade att de berörda versionerna inte uppfyllde de specificerade säkerhetsegenskaperna.

## 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.

## Källor och referenser

1. [Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years](https://the-decoder.com/google-deepminds-alphaproof-code-verified-signals-cryptographic-core-in-four-weeks-instead-of-years/) – The Decoder, 2026-11-11
2. [Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/) – Google DeepMind, 2026-11-10
3. [Google DeepMind](https://google-deepmind.github.io/code-verification/) – Google DeepMind
4. [The Register](https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/5308625) – The Register

Senast uppdaterad: 2026-11-11