Google DeepMind verifieert delen van libsignal met AI-agenten

AlphaProof Code maakt met een door mensen goedgekeurde specificatie en een team AI-agenten machine-checkbare Lean-bewijzen voor afgebakende beveiligingseigenschappen van libsignal, meldt Google DeepMind op 10 november; de controle loopt tot aan de gecompileerde machinecode.

Voor software- en beveiligingsteams die cryptografische onderdelen bouwen of inkopen, biedt dit een controleerbare uitspraak over één concrete build. Lean controleert de bewijsstappen automatisch; mensen beoordelen nog altijd de eigenschappen en aannames in de specificatie. Bij een leverancier of eigen bibliotheek tellen daardoor ook de exacte versie en de reikwijdte van het bewijs mee.

Mensen bepalen de eigenschap

AlphaProof Code verdeelt het werk over specificatie, code en bewijs. Onderzoekers vertaalden beveiligingsdoelen uit de vakliteratuur naar Lean, een taal voor formele uitspraken en bewijzen. Een agent hielp de specificatie opstellen, andere agenten controleerden die tegen de bronnen en de implementatie. Een mens keurde de definitieve specificatie goed voordat de bewijsagenten aan de slag gingen.

De onderzoekers compileerden de ongewijzigde Rust-code van libsignal naar een AArch64-uitvoerbaar bestand. Een team AI-agenten probeerde vervolgens de goedgekeurde eigenschappen voor die machinecode te bewijzen. Een gatekeeper liet een bewijs alleen door als de Lean-kernel het controleerde en een vergelijker bevestigde dat het bewijs bij exact dezelfde, goedgekeurde specificatie hoorde. De aankondiging noemt Gemini Carbon als model achter de bewijsagenten.

Het rapport telt ongeveer 6,5 miljoen regels Lean-bewijs en circa 26.000 regels aan vertrouwde specificaties en AArch64-semantiek. Die aantallen beschrijven verschillende lagen: de miljoenen bewijsregels worden machinaal gecontroleerd, terwijl de kleinere vertrouwde basis en de gekozen eigenschappen bepalend blijven voor wat de uitkomst betekent.

Vijf onderzoekers werkten vier weken aan symbolische en computationele bewijzen. DeepMind vergelijkt dat met jaren specialistisch werk bij eerdere verificatie-inspanningen, maar publiceert geen kostprijs per eigenschap of directe vergelijking met een gelijkwaardig project. Om te toetsen of de specificaties echte fouten konden signaleren, brachten de onderzoekers twee eerder verholpen bugs terug in een geïsoleerde versie van de code. In beide gevallen bewees het systeem dat de aangepaste code de vastgelegde beveiligingseigenschappen schond. Dat is een test met bekende fouten, geen melding dat AlphaProof Code een nieuwe kwetsbaarheid in Signal ontdekte.

De garantie stopt bij één-op-éénsessies

Het doel was niet de complete Signal-app. De onderzoekers bewezen eigenschappen van libsignal v0.105.4 in een kleine opdrachtregeltoepassing die als een nieuw proces op AArch64 Linux werd uitgevoerd. Het model beperkt de dekking tot één-op-éénsessies, met de PQXDH-handshake en de Triple Ratchet. De bewezen eigenschappen omvatten voorwaartse geheimhouding, authenticatie, veiligheid na een sleutelcompromis en geheimhouding van de handshake.

Groepsberichten bleven buiten het onderzoek. Ook sleutelgeneratie, zijkanalen, toestanden tussen meerdere apparaten en de servercode vallen niet onder deze garanties. De appversies voor Android en iOS gebruiken wel dezelfde Rust-bibliotheek, maar hebben andere compilerschakelaars, koppelingen en systeeminterfaces. De onderzoekers zeggen daarom niet dat deze apps automatisch door het bewijs zijn gedekt.

Ook het woord postkwantum vraagt afbakening. De onderzoekers bewijzen geheimhouding van de PQXDH-handshake tegen een toekomstige kwantumaanvaller in het symbolische model. Hun ratchetbewijzen tonen volgens het rapport niet aan dat SPQR de beveiliging herstelt nadat een aanvaller Diffie-Hellman kan breken. Een deel van de lage cryptografische routines staat bovendien als vertrouwde contracten buiten de verificatie. De Lean-kernel controleert dus of de code aan de goedgekeurde stellingen voldoet, niet of die stellingen elk denkbaar risico omvatten.

Andere AI-bewijzen beantwoorden andere vragen

In oktober meldde Anthropic dat Claude 239 fuzz-testdoelen uit 123 open sourcebibliotheken formeel crashvrij bewees voor invoer onder 64 megabyte. Anthropic beschrijft de beperkte RISC-V/Linux-opstelling met statische programma’s en één thread; voor sommige doelen repareerde Claude eerst een fout, waarna het bewijs voor de aangepaste code gold. Dat werk toetste crashvrij gedrag van geselecteerde ingangen, niet de cryptografische vertrouwelijkheid van een berichtensessie.

Anthropic publiceerde op 2 november FlashProve, dat een gegenereerd token met een cryptografisch bewijs aan vastgelegde modelgewichten koppelt. De techniek controleert de herkomst van modeluitvoer, niet of een softwarebibliotheek aan een beveiligingsspecificatie voldoet. De ontwikkelingen delen dus een werkwijze, geen algemene veiligheidsclaim: in elk geval moet eerst duidelijk zijn welke eigenschap en welke uitvoering het bewijs afdekt.

Een bewijs hoort bij een build

Voor Nederlandse organisaties die kritieke software bouwen of inkopen, verschuift de toets naar een concretere vraag: welke eigenschap is bewezen voor welke versie, met welke compiler, architectuur en vertrouwde onderdelen? De openbare Lean-bestanden van DeepMind geven teams materiaal om de specificaties en bewijsstappen zelf te bekijken. Wie een vergelijkbare controle voor eigen software wil, moet ook de formele eigenschappen, de bouwomgeving en de aannames kunnen onderhouden.

De aankondiging presenteert AlphaProof Code als onderzoek en noemt verdere uitbreiding naar andere systemen als toekomstig werk. Er is geen kant-en-klare dienst of doorlopende controle van nieuwe libsignal-versies aangekondigd. Voor een organisatie blijft de bewijswaarde daarom gekoppeld aan de exacte binary en aannames uit het experiment. Na een codewijziging moet de verificatie opnieuw aansluiten op de versie die daadwerkelijk wordt ingezet.