Een team van vijf personen en AI hebben de code van Signal in vier weken tijd bewezen

Vier weken. Zo lang had een team van vijf personen bij Google DeepMind, dat samenwerkte met AI-agenten, nodig om machinaal gecontroleerde bewijzen te leveren voor de belangrijkste beveiligingseigenschappen in de gecompileerde code van de kernbibliotheek van Signal's chatsysteem. De bewijzen beslaan ongeveer 6,5 miljoen regels. Eerdere baanbrekende pogingen op andere systemen vergden jaren van specialistisch werk en vereisten meestal dat er code werd geschreven om te bewijzen.

In het onderzoeksartikel, gedateerd 10 november 2026, wordt de methode en de beperkingen ervan beschreven. Het bijbehorende technische document geeft de cijfers gedetailleerder weer. Dit werk is geen bewijs voor de Signal-app als geheel, en ook geen bewijs voor andere apps die een vergelijkbaar ontwerp gebruiken. Het is een bewijs van specifieke eigenschappen van libsignal, de referentiebibliotheek, voor één-op-één-sessies, teruggebracht tot de gecompileerde machinecode die daadwerkelijk wordt uitgevoerd.

Wat werd bewezen

LibSignal is de bibliotheek die het encryptieontwerp van Signal implementeert. Simpel gezegd is dat ontwerp bedoeld om een bericht privé te houden, zelfs als een sleutel later wordt gestolen, en om te herstellen nadat een apparaat kortstondig is gecompromitteerd. Deze twee ideeën worden meestal forward secrecy en post-compromise security genoemd.

Het team compileerde de ongewijzigde bibliotheek — versie 0.105.4, plus de bijbehorende SPQR-crate in versie 1.6.0 — met de standaard Rust-compiler tot een klein commandoregelprogramma dat draait op 64-bits Arm Linux. De bewijzen hebben betrekking op dat uitvoerbare bestand, niet op een opgeschoonde herschrijving. De geverifieerde bibliotheek is ongeveer 560 KB groot, oftewel ongeveer 140.000 machine-instructies.

Ze behandelen de PQXDH-handshake, waarmee twee mensen een privésessie starten, inclusief een post-kwantumstap die bedoeld is om bestand te zijn tegen een toekomstige kwantumcomputer, en de Triple Ratchet, die voor elk bericht een nieuwe sleutel genereert. In het “symbolische” model, dat de onderliggende cryptografie als ideaal beschouwt, claimt het artikel ook geheimhouding van de handshake tegen een latere aanvaller met een kwantumcomputer. Groepschats, verzegelde afzenders en het serverprotocol worden als toekomstig onderzoek beschouwd.

Hoe het werk werd uitgevoerd

Formele verificatie houdt in dat er een precieze wiskundige beschrijving wordt gegeven van wat de code moet doen, en vervolgens wordt bewezen dat de code daaraan voldoet. Een enkele gemiste aanname kan het resultaat verzwakken, dus men moet nog steeds kiezen wat er bewezen moet worden en die beschrijving goedkeuren.

Het artikel is onomwonden over de scheiding. Mensen selecteerden de eigenschappen, losten onduidelijkheden op en keurden de specificatie goed. Agenten schreven vervolgens de bewijzen. Die bewijzen worden alleen geaccepteerd als Lean, een systeem voor bewijscontrole, ze bevestigt. De betrouwbaarheid van het resultaat, schrijven de auteurs, hangt niet af van de betrouwbaarheid van de bewijzende agenten, omdat de kernel van Lean de logica controleert.

Het onderzoeksartikel vermeldt dat de bewijsagenten werden aangedreven door Gemini Carbon. Het bewijswerk zelf werd in vier weken tijd door vijf onderzoekers uitgevoerd, waarbij elk agent op zijn eigen werkstation draaide. Dat is een korte campagne naar de maatstaven van het vakgebied. Het artikel merkt op dat de seL4-microkernel, een beroemde eerdere verificatie, twintig manjaar in beslag nam, en dat de CompCert C-compiler zes manjaar duurde. Beide codebases waren geschreven met bewijsvoering in gedachten. Libsignal niet.

Wil je dat AI je wekelijks uren bespaart? Ons gratis stappenplan laat je zien hoe.Download de gratis gids →

De bewijzen zelf kunnen lang zijn omdat ze over machinecode gaan. Ongeveer 6,5 miljoen regels bestaan uit bewijzen: 5,3 miljoen over de binaire code, plus aparte bestanden voor de twee beveiligingsmodellen. Een lezer die de beweringen in de koptekst wil vertrouwen, moet nog steeds de betrouwbare delen lezen: ongeveer 18.000 regels specificatie in de repository, plus ongeveer 8.000 regels van het Arm-machinecodemodel en de symboolnamen die aan het uitvoerbare bestand zijn gekoppeld. De cryptografische routines op laag niveau, twee uitvoerfuncties en een paar bibliotheekaanroepen worden contractueel verondersteld, niet bewezen.

Een controle op oude bugs

Om te testen of de beweringen sterk genoeg waren, introduceerde het team twee bugs opnieuw die onderzoekers eerder in libsignal hadden gevonden en die inmiddels waren verholpen. In beide gevallen bewezen ze dat de symbolische beveiligingstheorie niet opgaat voor het betreffende binaire bestand. Dat is een nuttige controle: een specificatie die nog steeds “slaagt” op bekende, gebrekkige code zou te zwak zijn.

Een van die bugs bewaarde de status van een nieuwe sessie, inclusief een kopie van een geheim, nadat een prekey-bericht alleen onder een oudere sessie was gedecodeerd. De andere accepteerde een handshake waarvan de basissleutel was vervormd, waardoor een tweede sessie met hetzelfde gedeelde geheim werd gecreëerd.

Wat het resultaat niet zegt

De auteurs zijn zorgvuldig te werk gegaan en de beperkingen zijn van belang. De bewijzen dekken niet elk onderdeel van Signal, elke mogelijke aanval of de cryptografische primitieven zelf. Side channels vallen buiten het bestek. Het computationele bewijs, dat de kans op succes van een echte aanvaller probeert te begrenzen, biedt geen garantie tegen een kwantumtegenstander, en de grens ervan verliest zijn waarde bij meerdere lange sessies met vele rondes.

Varianten van hetzelfde protocol worden gebruikt in WhatsApp, Meta Messenger en Google Messages, zo blijkt uit het artikel. Die apps waren niet het artefact dat werd bewezen. Een bewijs over libsignal is niet automatisch van toepassing op elk product dat een vergelijkbare taal spreekt.

Ehren Kret, de chief technology officer van Signal, wordt in het onderzoeksartikel geciteerd met de uitspraak dat het rigoureus verifiëren van de protocolimplementatie “ons nog meer vertrouwen geeft in de privacygaranties van onze code”.

De bewijzen en specificaties zijn gepubliceerd in een open repository.

Waarom het belangrijk is

De meeste mensen die een privébericht versturen, zien nooit de bibliotheek die het versleutelt. Een methode die de gecompileerde code van die bibliotheek binnen enkele weken in plaats van jaren kan controleren, is een praktische verbetering in de manier waarop dergelijke software gecontroleerd kan worden. Het is geen certificaat dat Signal, of welke andere chat-app dan ook, foutloos is. Het is een machinaal gecontroleerd argument over specifieke eigenschappen van één kernbibliotheek, dat snel genoeg geproduceerd wordt zodat andere cruciale code mogelijk snel daarna aan de beurt is.

De meeste gangbare chatprogramma's beschikken nog steeds niet over dergelijk bewijs, en sommige populaire tools versleutelen berichten helemaal niet van begin tot eind. Een eerder rapport ging over een chatprogramma voor consumenten dat berichten verstuurt zonder die bescherming.