EnglishGoogle DeepMind verifieert cryptografische code van Signal met AI-agents
Google DeepMind heeft met AI-agents wiskundig bewezen dat de kern van de versleuteling van Signal belangrijke beveiligingseisen haalt, tot in de code die echt op de processor draait. Het werk duurde vier weken en ging over één-op-één-gesprekken, niet over de hele app.
Google DeepMind heeft met een nieuw systeem, genaamd AlphaProof Code, wiskundig gecontroleerd of de kern van de versleuteling van Signal doet wat hij moet doen. Volgens het AI-onderzoekslab van Google is het de eerste keer dat de werkende code van zo'n veelgebruikt versleutelingsprotocol op dit niveau is bewezen, met of zonder AI. Het Signal-protocol beschermt gesprekken in onder meer de berichtenapp Signal en Google Messages.
Twee onderdelen van de versleuteling
Het team keek naar twee onderdelen in libsignal, de softwarebibliotheek van Signal. Het eerste onderdeel, PQXDH, spreekt aan het begin van een gesprek de geheime sleutels af, op een manier die ook bestand moet zijn tegen toekomstige quantumcomputers. Het tweede, de Triple Ratchet, maakt bij elk bericht steeds nieuwe sleutels. Daardoor blijven berichten beschermd, ook als een aanvaller even toegang had tot een toestel.
De onderzoekers controleerden niet de broncode die programmeurs schrijven, maar het gecompileerde programma: de instructies die een ARM-processor, het type chip in de meeste telefoons, echt uitvoert. Zo telt ook een fout mee die pas ontstaat bij het omzetten van broncode naar een werkend programma.
Mensen bepalen wat bewezen moet worden
Formele verificatie betekent dat je met een wiskundig bewijs vaststelt dat software aan vastgelegde eisen voldoet, in plaats van haar alleen te testen. Eerst vertaalden de onderzoekers met hulp van AI-modellen de beveiligingsdoelen van Signal naar precieze wiskundige eisen. Menselijke experts controleerden elke eis.
Daarna schreven AI-agents met Gemini 4 Carbon, het nieuwste topmodel van Google, de bewijzen in Lean: een taal waarin een computer elk bewijs stap voor stap nakijkt. Teams van 40 tot 80 agents werkten op één computer telkens een tot drie dagen. Samen schreven ze ongeveer 6,5 miljoen regels bewijs. De agents markeerden ongeveer één procent van het werk voor een extra blik van een mens; de rest controleerde Lean automatisch.
Een team van vijf mensen deed het werk in vier weken. Vergelijkbare projecten kostten expertteams volgens Google DeepMind van oudsher jaren. Het team bouwde voort op eerdere wiskundige analyses van het protocol, ook van het werk dat Signal zelf al liet doen. Signals technisch directeur Ehren Kret noemt het een grote doorbraak dat AI-agents werkende code kunnen omzetten in bewijzen die kloppen.
In de onderzochte onderdelen kwamen geen nieuwe zwakke plekken aan het licht. Om te testen of de methode fouten echt opmerkt, brachten de onderzoekers twee oude, al lang verholpen fouten opnieuw aan in een aparte versie van de code. In beide gevallen bewees het systeem dat die versie onveilig was.
Wat er nog buiten valt
Het bewijs gaat ervan uit dat de bouwstenen van de versleuteling zelf, zoals de wiskundige sleutelfuncties, foutloos werken. Het gaat over gesprekken tussen twee mensen, niet over groepsgesprekken, en niet over de complete apps op telefoons. Groepsgesprekken staan op de lijst voor later. Google DeepMind maakt de eisen en bewijzen openbaar, zodat anderen ze kunnen nalopen. Wat het onderzoek kostte, wilde Google niet zeggen.
Wat betekent dit voor de weg naar de singulariteit?
AI-agents schrijven al langer code, maar hier bewezen ze dat bestaande code veilig werkt. Eerder deze maand lieten duizend Claude-agents zien dat ze een beroemd wiskundig bewijs in Lean kunnen omzetten; bij Signal gaat dezelfde soort controle over software die miljoenen mensen dagelijks gebruiken. Lukt het om dit op te schalen, dan kan bewezen betrouwbare software ook binnen bereik komen voor bijvoorbeeld medische apparaten en elektriciteitsnetten, met mensen die blijven bepalen wat er bewezen moet worden.
