Google DeepMinds AlphaProof Code verifieert Signal's cryptografische protocol formeel

Google DeepMind zegt een mijlpaal in softwarebeveiliging te hebben bereikt die lang als een grote uitdaging werd beschouwd: zijn onderzoekers hebben AI-agenten begeleid bij het wiskundig bewijzen van belangrijke beveiligingseigenschappen van de daadwerkelijke code onder het Signal-protocol, de technologie die miljarden privégesprekken beschermt in apps zoals Signal en Google Messages door berichten end-to-end te versleutelen, zodat alleen de afzender en de beoogde ontvanger ze kunnen lezen. De aankondiging werd gepubliceerd op de Google DeepMind-blog door Pushmeet Kohli en Swarat Chaudhuri.

Het resultaat werd bereikt met AlphaProof Code, een nieuw agentisch framework voor formele verificatie op ongekende diepte dat menselijke expertise combineert met AI-agenten. Formele verificatie — wiskundig bewijzen dat code correct en foutloos werkt — is de hoogste standaard van beveiligingszekerheid, maar is moeilijk en vaak arbeidsintensief. Conventioneel testen bemonstert het gedrag van een programma; een formeel bewijs sluit fouten uit bij elke mogelijke uitvoering — een niveau van zekerheid dat zo kostbaar is om te produceren dat het zelden breed ingezette software heeft bereikt.

Volgens het bedrijf markeert dit werk de eerste keer dat AI is gebruikt om een veelgebruikt cryptografisch protocol op deze diepte formeel te verifiëren. Het is ook de eerste keer dat de implementatie van een breed ingezet protocol van dit soort door welke methode dan ook formeel is geverifieerd, met of zonder AI.

Hoe Google DeepMind Signal verifieerde

AlphaProof Code is een multi-LLM agentisch framework dat het werk van formele verificatie verdeelt zoals een onderzoeksteam dat zou doen: menselijke experts werken samen met AI om te bepalen wat er bewezen moet worden, en een groep AI-agenten voert de bewijzen uit.

Eerst werkten de onderzoekers van Google DeepMind samen met een mix van modellen om Signal's beveiligingsdoelen te vertalen naar formele wiskundige specificaties, waarbij menselijke experts elke specificatie beoordeelden. Agenten aangedreven door Gemini Carbon voerden vervolgens de bewijzen uit en genereerden meer dan zes miljoen regels Lean, een computertaal die wiskundig de juistheid van code bewijst.

De agenten auditteven daarna het bewijs en markeerden de gebieden die een tweede blik van een mens nodig hadden — slechts één procent van de codebase, wat het bedrijf omschrijft als een enorme tijdwinst. Omdat Lean de rest automatisch controleerden, konden experts hun beoordeling richten op de plaatsen waar menselijk oordeel het belangrijkst is.

Beveiliging bewezen tot aan de draaiende code

Cryptografische protocollen vormen de basis van vrijwel alle digitale communicatie, van internetbankieren tot webbrowsing, en één enkele fout kan miljoenen mensen tegelijk blootstellen aan risico's. Daarom analyseren experts ze al decennia formeel, hoewel de meeste protocolverificatie op het ontwerpniveau stopt.

De agenten van Google DeepMind gingen verder en bewezen dat de gecompileerde code belangrijke beveiligingseigenschappen vervult — zoals het beschermen van berichten vóór en nadat een apparaat tijdelijk is gecompromitteerd, garanties die cryptografen kennen als forward secrecy en post-compromise security — tot aan de exacte code die op apparaten draait. Kwetsbaarheden in de praktijk schuilen vaak in de kloof tussen ontwerp en implementatie, en het overbruggen van die kloof maakt deze bewijzen aanzienlijk complexer.

Zelfs bij deze complexiteit nam het verificatieproces slechts vier weken in beslag — een taak die historisch gezien expertteams jaren kost, volgens het bedrijf — waarmee werd vastgesteld dat Signal's kerncryptografische code de beveiligingsbeschermingen levert die de onderzoekers hadden gespecificeerd.

Om te bevestigen dat AlphaProof Code correcte code kan onderscheiden van foutieve code, herintroduceerde het team twee echte, eerder verholpen bugs in een geïsoleerde versie van Signal's code. In beide gevallen produceerde het systeem een machinegecontroleerd bewijs dat de foutieve versie onveilig was — een controle die er toe doet, omdat een verificateur die foutieve code niet kan opsporen valse zekerheid zou bieden.

In AlphaProof Code helpen AI-agenten gebruikers een specificatie te schrijven en bewijzen ze vervolgens autonoom dat de implementatie daaraan voldoet. Elk bewijs wordt door Lean gecontroleerd om het werk van de agenten te verifiëren.

De reactie van Signal

"Waar eerdere formele verificatie zich richtte op kleinere delen van de code, maakt Google DeepMinds aanpak een aanzienlijke uitbreiding mogelijk," zei Ehren Kret, Chief Technology Officer van Signal. "Het gebruik van AI-agenten om live code te vertalen naar geldige Lean-stellingen is een belangrijke doorbraak. Naarmate AI-gedreven beveiligingsdreigingen toenemen, geeft het rigoureuze verifiëren van de implementatie van het Signal-protocol ons nog meer vertrouwen in de privacygaranties van onze code."

De toekomst van beveiliging

Google DeepMind stelt dat het overwinnen van deze lang bestaande uitdaging laat zien hoe AI elite-beveiligingszekerheid kan brengen aan bedrijven, overheden en kritieke infrastructuur, en helpt zich te verdedigen tegen agent-gedreven cyberdreigingen. De verificatie van Signal's kerncryptografie legt, zegt het bedrijf, de basis om andere vitale systemen te beveiligen, van firmware voor medische apparaten tot software voor het elektriciteitsnet.

Het opschalen van deze technieken vereist voortgezet onderzoek. Gecombineerd met geautomatiseerde verdedigingsagenten zoals CodeMender kan formele verificatie helpen de snelheid en schaal van moderne cyberdreigingen te weerstaan en software te creëren met wiskundig bewijs dat de beveiligingsmaatregelen werken.

Google DeepMind stelt zijn formele verificatie-artefacten open source beschikbaar voor gemeenschapsgebruik, gehost op google-deepmind.github.io/code-verification. Het volledige technische artikel is beschikbaar als PDF. Voor de onderzoeksgemeenschap op het gebied van beveiliging biedt die publicatie een manier om de machinegecontroleerde bewijzen en de methodologie direct te inspecteren — en hoe ver verificatie op deze diepte zich buiten Signal verspreidt, naar de medische, industriële en infrastructuursystemen die het bedrijf noemt, is de ontwikkeling om in de gaten te houden.

Dankwoord

Het onderzoek is ontwikkeld door Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton en Pushmeet Kohli.

Het team bedankte Eric Wieser voor hulp bij het open sourcen van de code, Owen Jones voor ondersteuning bij programmamanagement, en Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko en George Tsoukalas voor waardevolle discussies. De onderzoekers bedankten ook Signal's Rolfe Schmidt, Michael Rosenberg en Ehren Kret voor feedback op de methodologie, evenals Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis en Sundar Pichai voor hun steun aan het project.