Google DeepMind verifieert het Signal-protocol formeel met AI

Onderzoekers van Google DeepMind hebben met een agentisch AI-raamwerk genaamd AlphaProof Code verschillende cruciale cryptografische garanties van het Signal-protocol wiskundig bewezen, meldt Wired. Het werk, een proof of concept dat in vier weken is afgerond, is een voorbeeld van formele verificatie: een methode die wiskunde gebruikt om te controleren of software doet wat bedoeld is, in plaats van een steekproef van gevallen te testen.

Het Signal-protocol is het versleutelingsschema achter de Signal-app en beschermt, zoals Wired opmerkt, ook de communicatie in Google Messages en WhatsApp. De analyse geldt daarom als extra onafhankelijke bevestiging van cryptografie die een enorm aantal berichten beveiligt. Wired noemt het een mijlpaal voor de cryptografie en voor AI zelf, maar benadrukt dat de reikwijdte beperkt is.

Wat heeft DeepMind precies bewezen?

Het team bewees “een aantal” kerngaranties van het protocol, niet alle. Wired maakt duidelijk dat de volledige mobiele Signal-app niet formeel is geverifieerd, en de onderzoekers beschrijven hun resultaat als een mijlpaal in een groter proces. “We zijn erg blij met dit resultaat, maar er is nog een lange weg te gaan voordat we dit kunnen opschalen naar alle software ter wereld, en dat willen we”, zei Swarat Chaudhuri, onderzoeker bij DeepMind, tegen Wired.

Volgens hetzelfde artikel vond de analyse geen nieuwe kwetsbaarheid in de onderzochte delen van het protocol. De onderzoekers lieten AlphaProof Code ook los op oudere Signal-versies met bekende, allang verholpen kwetsbaarheden: de tool herkende ze correct en liet zien dat die versies niet formeel te verifiëren waren. Die test is belangrijk, omdat hij laat zien dat de methode kan falen als er een fout zit, en niet alleen slaagt als die er niet is.

• Tool: AlphaProof Code, een nieuw agentisch AI-raamwerk van Google DeepMind.
• Duur: vier weken, als proof-of-conceptproject.
• Resultaat: cruciale cryptografische garanties bewezen; geen nieuwe kwetsbaarheid in de geanalyseerde delen.
• Oudere versies: bekende, allang verholpen fouten opgespoord en het protocol als niet verifieerbaar aangemerkt.
• Publicatie: de specificatie en het bewijs worden vrijgegeven om ander verificatiewerk te helpen.
• Kosten: niet bekendgemaakt; de analyse gebeurde gratis, als onderzoeksproject.

Hoe verdeelden AI en mensen het werk?

Vóór het AI-tijdperk moesten mensen de eigenschappen beschrijven die ze wilden bewijzen, die in formules omzetten en daarna het bewijs ontwikkelen. Wired legt uit dat agentische AI de tijd voor die laatste stap sterk kan verkorten, en dat maakte de Signal-evaluatie in vier weken mogelijk. De DeepMind-onderzoekers voegen toe dat ze een voorsprong hadden, omdat de Signal Foundation al formele verificatie had uitgevoerd op kleinere delen van de code.

Ehren Kret, technisch directeur van Signal, zei in een door Wired geciteerde verklaring: “Waar eerdere formele verificatie zich richtte op kleinere delen van de code, maakt de aanpak van Google DeepMind een aanzienlijke uitbreiding mogelijk.” Het rigoureus verifiëren van de implementatie geeft Signal naar eigen zeggen nog meer vertrouwen in de privacygaranties van zijn code, nu door AI gedreven beveiligingsdreigingen toenemen.

DeepMind ziet zijn belangrijkste doorbraak in een “samenwerkingsproces tussen mens en AI”: agenten dragen in bijna elke fase bij en corrigeren zichzelf, terwijl mensen op sleutelmomenten controleren. “We willen geen wereld waarin AI de doelen en de bewijzen genereert”, zei Chaudhuri. Een formeel bewijs garandeert alleen de eigenschappen die zijn opgeschreven, daarom blijft menselijke controle van de specificatie centraal.

Een parallelle inspanning rond Signal

Het werk van DeepMind is niet de enige poging om Signals cryptografie te bewijzen. De Beneficial AI Foundation lanceerde samen met Rolfe Schmidt van Signal en het Lean FRO “Signal Shot”, een openbaar project om het protocol en de Rust-implementatie te verifiëren met de bewijsassistent Lean. Het plan is Signals Rust-code met de tool Aeneas naar Lean te vertalen; als te verifiëren onderdelen worden onder meer de post-quantum sleuteluitwisseling PQXDH, de Double Ratchet en de SPQR/Triple Ratchet genoemd. Wired koppelt dit initiatief niet aan dat van DeepMind: het zijn twee aparte inspanningen.

Wat blijft onzeker?

De open vraag, schrijft Wired, is of door AI geautomatiseerde formele verificatie tegen werkbare kosten kan opschalen. Google weigerde de kosten van de Signal-analyse te delen en te zeggen of het een commercieel product of dienst voor formele verificatie plant. Pushmeet Kohli, hoofdwetenschapper van Google Cloud en vicepresident onderzoek bij DeepMind, ziet voor zich dat banken en andere bedrijven die zich zorgen maken over bugs kunnen zeggen dat ze bepaalde eigenschappen van hun software kunnen bewijzen. Dat is een visie, geen aangekondigd aanbod.

Wat dit verandert voor bedrijven

Voor een bedrijf dat een berichtendienst kiest of voortbouwt op het Signal-protocol is het resultaat een geruststellend signaal over het ontwerp van het protocol, geen certificaat voor elke app die het gebruikt: de volledige Signal-app is niet geverifieerd, en de uitrol, de servers en de instellingen van een product vallen buiten het bewijs. De gepubliceerde specificatie en het bewijs geven beveiligingsteams materiaal om te bestuderen en te hergebruiken. Omdat kosten en een eventueel commercieel aanbod onbekend zijn, moeten bedrijven er nog niet op rekenen hun eigen code zo formeel te verifiëren, maar ze kunnen leveranciers van kritieke software al vragen welke eigenschappen zijn gespecificeerd en bewezen.