Google DeepMind bewijst met AI dat de code van Signal klopt

Google DeepMind heeft met een team van AI-agents wiskundig aangetoond dat de kern van de versleuteling in Signal doet wat hij belooft. Het systeem heet AlphaProof Code en toetste in vier weken de code waarop de berichtenapp draait. Volgens de aankondiging van DeepMind kostte dit soort werk expertteams tot nu toe jaren.

Wat AlphaProof Code precies deed

Signal gebruikt een eigen protocol om berichten end-to-end te versleutelen. Ook WhatsApp en andere apps bouwen daarop voort. DeepMind keek naar twee onderdelen: PQXDH, de handshake waarmee twee telefoons veilig sleutels afspreken (en die ook bestand is tegen toekomstige quantumcomputers) en de Triple Ratchet, het mechanisme dat tijdens een gesprek telkens nieuwe sleutels aanmaakt. Dat meldt ShiftDelete op basis van het technische paper.

De werkwijze bestaat uit twee lagen. Eerst vertaalden onderzoekers met hulp van verschillende modellen de beveiligingsdoelen van Signal naar formele specificaties en mensen keurden elke specificatie goed. Daarna schreven agents op basis van Gemini 4 Carbon de bewijzen in Lean, een taal waarin een computer elke stap automatisch narekent. Dat leverde ruim zes miljoen regels bewijs op. De agents controleerden hun eigen werk en zetten ongeveer 1 procent opzij voor menselijke beoordeling.

Bewijs op het niveau van machinecode

Het verschil met eerder werk zit in het niveau. Formele verificatie van protocollen stopt meestal bij het ontwerp op papier. DeepMind bewees de eigenschappen voor de gecompileerde machinecode van libsignal, de Rust-bibliotheek achter het protocol, zoals die op 64-bit Arm-processors draait. Volgens DeepMind zitten echte kwetsbaarheden vaak juist in het gat tussen ontwerp en uitvoering.

Bewezen zijn onder meer forward secrecy (oude berichten blijven veilig als een sleutel later uitlekt) en herstel na een tijdelijke inbraak op een toestel. Als controle zetten de onderzoekers twee echte, allang gerepareerde bugs terug in een afgeschermde kopie van de code. In beide gevallen leverde het systeem een sluitend bewijs dat die versie onveilig was. Signal-CTO Ehren Kret noemt de aanpak volgens TUN een grote doorbraak, omdat eerder werk slechts kleine stukken van de code besloeg.

De grenzen van het bewijs

Het onderzoek zegt niet dat de hele Signal-app foutloos is. De mobiele app zelf viel erbuiten, de bewijzen gelden voor één platform (AArch64 Linux) en de onderliggende cryptografische bouwstenen zijn als veilig aangenomen in plaats van bewezen. Nieuwe lekken vond DeepMind in het onderzochte deel niet. Het bedrijf deed het werk gratis voor Signal en zegt niets over de kosten. Specificaties en bewijzen komen als open source beschikbaar via de projectpagina.

Het past in een reeks: eerder vond AI van Google DeepMind twee zwakke plekken in RSA-1024 en liet Axiom AI-agents een enorm wiskundebewijs in Lean controleren.

Wat betekent dit

In de beveiliging wordt AI vooral ingezet om lekken te vinden, zoals toen OpenAI-agents 948 rootlekken in de Linux-kernel opspoorden. Dit project laat de andere kant zien: aantonen dat code klopt. Als dat in weken kan in plaats van jaren, komt formele controle binnen bereik voor software waar fouten duur zijn. DeepMind noemt zelf firmware van medische apparaten en software voor het stroomnet. Voor gewone Signal-gebruikers verandert er niets; updates blijven nodig, want buiten de geverifieerde kern kunnen nog steeds fouten zitten.