Onderzoekers van Google DeepMind hebben een agentische AI gebruikt om wiskundig verschillende cruciale cryptografische garanties van het Signal-protocol aan te tonen. Dit werk, uitgevoerd als een proof-of-conceptproject in vier weken, maakt gebruik van een nieuw AI-framework genaamd AlphaProof Code.
- Google DeepMind gebruikt agentische AI om het Signal-protocol wiskundig te verifiëren.
- De onderzochte onderdelen bevatten geen nieuwe kwetsbaarheden, en de volledige mobiele app is niet geverifieerd.
- AI verkort de bewijslevering sterk, maar het opschalen naar redelijke kosten blijft onzeker.
Het Signal-protocol versleutelt de communicatie in de Signal-app, maar volgens de bron ook in Google Messages en WhatsApp. Voor het artikel vormt deze demonstratie een nieuwe onafhankelijke validatie van deze cryptografie, die wereldwijd een enorme hoeveelheid berichten beschermt. Het illustreert ook de mogelijkheden van formele verificatie van Google DeepMind.
Formele verificatie houdt in dat wiskunde wordt gebruikt om te controleren of software werkt zoals bedoeld, dat wil zeggen dat er geen kritieke fouten in zitten. Voorstanders beschouwen het al lang als de heilige graal van softwarebeveiliging. Maar het grootschalige gebruik blijft onzeker, net als de effectiviteit ervan bij grote hoeveelheden code.
Een gerichte analyse
Vóór het AI-tijdperk kostte het aanzienlijk veel tijd om de kenmerken van software te beschrijven, deze beschrijvingen om te zetten in formules en vervolgens het bewijs te leveren. Volgens de bron kan agentische AI de duur van deze laatste stap sterk verkorten. De reikwijdte van de analyse blijft echter beperkt: zo is bijvoorbeeld niet de volledige mobiele Signal-app formeel geverifieerd.
In de onderzochte delen van het protocol vonden de onderzoekers geen nieuwe kwetsbaarheden. Toen ze AlphaProof Code echter toepasten op oudere versies van Signal die bekende, al lang gerepareerde fouten bevatten, identificeerde de tool deze correct en toonde aan dat het protocol in die versies niet formeel kon worden geverifieerd. De onderzoekers publiceren de specificatie en het bewijs dat is opgesteld voor de analyse van het Signal-protocol, om ander formeel verificatiewerk te vergemakkelijken.
De snelheid van het project is deels te danken aan eerder werk van de Signal Foundation op dit gebied, zoals de DeepMind-onderzoekers benadrukken. « Waar eerdere formele verificatie zich richtte op kleinere delen van de code, maakt de aanpak van Google DeepMind een aanzienlijke uitbreiding mogelijk, » zegt Ehren Kret, technisch directeur van Signal, in een verklaring. « Terwijl AI-gerelateerde beveiligingsbedreigingen toenemen, geeft het rigoureus verifiëren van de implementatie van het Signal-protocol ons nog meer vertrouwen in de privacygaranties van onze code. »
Een kwestie van kosten en schaal
Voor kritieke diensten die in hoogrisicocontexten worden gebruikt, zou het formeel kunnen verifiëren van elke codebase en de volledige softwareleveringsketen een grote stap voorwaarts zijn, aldus Pushmeet Kohli, wetenschappelijk directeur van Google Cloud en vicepresident onderzoek bij DeepMind. « Als we nu de juistheid van deze implementaties kunnen verifiëren, kunnen we gerust zijn. Stel je voor dat banken en alle andere bedrijven die afhankelijk zijn van garanties en zich zorgen maken over bugs nu kunnen zeggen: ‘Ik kan deze eigenschappen bewijzen’, » zegt hij.
De vraag blijft, voor de hele technologiesector, of door AI geautomatiseerde formele verificatie echt kan opschalen tegen redelijke kosten. DeepMind voerde de Signal-analyse gratis uit als onderdeel van een onderzoeksproject, en Google wilde de kosten niet bekendmaken. Het bedrijf heeft ook niet aangegeven of het van plan is een product of dienst voor formele verificatie te commercialiseren.
De onderzoekers zijn van mening dat enkele van hun cruciale vooruitgangen betrekking hebben op een ‘mens-AI-samenwerkingsproces’, zoals Swarat Chaudhuri, onderzoekswetenschapper bij DeepMind, het uitdrukt. Dit proces stelt agenten in staat om bij bijna elke stap bij te dragen en zichzelf te corrigeren, terwijl op cruciale momenten menselijk advies en validatie wordt ingewonnen. « We willen niet die wereld van de sfeer, waar de AI de doelen stelt, de AI de bewijzen levert, en we de tests doorstaan die ze zelf heeft geschreven. Er is een tussenweg. »
