Google DeepMind heeft met een nieuw AI-systeem wiskundig bewezen dat belangrijke beveiligingsgaranties van het Signal-protocol kloppen. Dat protocol versleutelt niet alleen berichten in de Signal-app, maar ook die in WhatsApp en Google Messages. Het onderzoek duurde volgens WIRED maar vier weken en is bedoeld als proefproject voor een nieuwe tool: AlphaProof Code.
Wat is formele verificatie?
Bij formele verificatie test je software niet met losse voorbeelden, maar bewijs je met wiskunde dat ze onder alle omstandigheden doet wat de bedoeling is. Beveiligers zien dat al jaren als een soort heilige graal, omdat een geslaagd bewijs aantoont dat bepaalde soorten fouten er simpelweg niet in kunnen zitten. Het nadeel: het is extreem arbeidsintensief. Mensen moeten eerst precies beschrijven welke eigenschappen ze willen bewijzen, die omzetten in formules en dan het bewijs uitwerken. Vooral dat laatste kunnen AI-agents nu flink versnellen.
Zo werkte het volgens DeepMind
In zijn eigen aankondiging beschrijft DeepMind AlphaProof Code als een raamwerk met meerdere taalmodellen dat werkt als een onderzoeksteam. Onderzoekers zetten samen met AI de beveiligingsdoelen van Signal om in wiskundige specificaties, en mensen keurden elk daarvan. Daarna schreven agents op basis van Gemini Carbon de bewijzen: volgens DeepMind ruim zes miljoen regels in Lean, een programmeertaal waarmee een computer een bewijs stap voor stap controleert. De agents markeerden zelf welke stukken nog menselijke controle nodig hadden; dat was ongeveer één procent.
Volgens DeepMind is het de eerste keer dat de daadwerkelijke code van zo'n breed gebruikt protocol is geverifieerd, met of zonder AI. Eerdere analyses keken meestal alleen naar het ontwerp, terwijl lekken in de praktijk vaak zitten in het verschil tussen ontwerp en uitvoering. Dat zijn claims van DeepMind zelf.
Geen nieuwe lekken, oude wel herkend
In de onderdelen van het protocol die DeepMind onderzocht, vond de AI geen nieuwe kwetsbaarheden. Als controle zetten de onderzoekers twee echte, al lang gedichte fouten terug in een afgeschermde versie van de Signal-code. In beide gevallen leverde het systeem een machinaal gecontroleerd bewijs dat die versie onveilig was. DeepMind maakt de specificatie en het bewijs openbaar, zodat anderen erop kunnen voortbouwen.
De reikwijdte is wel beperkt. De volledige Signal-app is niet geverifieerd, alleen een deel van de cryptografische garanties van het protocol. Ook kreeg DeepMind een voorsprong doordat de Signal Foundation eerder al zelf aan formele verificatie had gewerkt. Signal-CTO Ehren Kret zegt in een verklaring dat de aanpak van DeepMind veel verder reikt dan eerdere verificaties van kleinere stukken code.
Mens blijft in de lus
DeepMind-onderzoeker Swarat Chaudhuri benadrukt dat agents in bijna elke stap meedoen en zichzelf corrigeren, maar dat mensen op belangrijke punten blijven meekijken. Hij wil geen situatie waarin AI zowel de doelen als de bewijzen bedenkt en "zelfgeschreven toetsen" maakt. Het einddoel noemt hij ambitieus: op termijn "alle software van de wereld" op deze manier verifiëren.
Kosten blijven de grote vraag
Of dit ook betaalbaar op grote schaal kan, is onduidelijk. Google deed het Signal-onderzoek gratis als onderzoeksproject, wil niet zeggen wat het kostte en zegt niets over een eventueel commercieel product. Toch is de timing interessant. AI-modellen vinden steeds sneller lekken, zoals wij eerder schreven in AI vindt lekken sneller dan beveiligers ze kunnen dichten. Formele verificatie is de tegenhanger daarvan: niet zoeken naar fouten, maar bewijzen dat ze er niet zijn.
Voor Nederlandse gebruikers is het vooral geruststellend nieuws: de versleuteling achter de chatapps die miljoenen mensen hier dagelijks gebruiken, heeft weer een onafhankelijke controle doorstaan. Voor overheden en banken, die onder Europese regels als NIS2 en DORA moeten aantonen dat hun kritieke software betrouwbaar is, kan AI-gestuurde verificatie op termijn een praktisch hulpmiddel worden, als de prijs meevalt.
Bijgewerkt op 10 november: aangevuld met details uit de officiële aankondiging van Google DeepMind over de werkwijze, de omvang van het bewijs en de controle met teruggezette fouten.
