Google heeft de toegang tot Gemini 4 Carbon verruimd en geeft aan dat op dit model gebouwde agents hebben bijgedragen aan de formele verificatie van centrale veiligheidsgaranties in de code van het Signal-protocol.
Ontwikkelaars en bedrijven die betalen, kunnen Carbon nu gebruiken via de Gemini API en Gemini for business, en ook Google AI Ultra-abonnees hebben er toegang toe. Introductietarieven van $2 en $10 per miljoen tokens voor invoer en uitvoer gelden tot 30 november, waarna ze verdubbelen. Een token is een eenheid tekst die het model verwerkt om inhoud te lezen of te produceren.
Tot nu toe konden alleen bepaalde cybersecurity-verdedigers die deel uitmaken van Googles Fairwind-programma Carbon gebruiken. Ze moeten nog steeds tot dit programma behoren om toegang te krijgen tot Carbon for cyber, een versie die Google presenteert als leidend in belangrijke benchmarks voor het detecteren, exploiteren en herstellen van kwetsbaarheden.
Toepassingen in cybersecurity
Volgens Google heeft het bedrijf Wiz Carbon for cyber gebruikt om binnen twee uur ‘zero-day’-kwetsbaarheden bij twee grote SaaS-leveranciers te vinden. Het Cloud Vulnerability Research (CVR)-team van Google heeft op zijn beurt het model gebruikt om te bevestigen dat twee bugs in een populair open-sourceproject exploiteerbaar waren, met een ernst vergelijkbaar met die van PHP2Shell, een paar PHP-kwetsbaarheden die al door aanvallers zijn geëxploiteerd.
« Door Carbon te gebruiken om een proof of concept te bouwen, heeft CVR de onderhouders geholpen de bug als kritiek te herclassificeren en snel een patch uit te brengen », aldus Google.
Code van Signal verifiëren
Daarnaast heeft Google DeepMind AlphaProof Code gepresenteerd, dat menselijke experts combineert met AI-agents om software formeel te verifiëren, dat wil zeggen wiskundig aan te tonen dat ze aan gedefinieerde vereisten voldoet. Het team heeft dit toegepast op libsignal, de referentie-implementatie van het Signal-protocol. Versies van dit protocol werken ook in WhatsApp en Google Messages.
Mensen werkten samen met agents die draaiden op Carbon en op Claude Opus 5.5 om de specificaties te schrijven die beschrijven wat bewezen moest worden. Op Carbon gebaseerde agents genereerden vervolgens de volledige set van ongeveer 6,5 miljoen regels bewijs geschreven in Lean, een proof assistant die ongeldige bewijzen afwijst. Volgens Google gelden de bewezen garanties, waaronder persistent geheimhouding (forward secrecy), veiligheid na compromittering en authenticatie, voor de gecompileerde machinecode, terwijl de meeste protocolverificaties alleen op het ontwerp betrekking hebben.
Vijf onderzoekers voltooiden het bewijswerk in vier weken, een taak die Google traditioneel voorbehoudt aan specialisten gedurende jaren. Om te verifiëren dat de methode echte kwetsbaarheden detecteert, heeft het team twee oude, reeds herstelde bugs in libsignal opnieuw geïntroduceerd en bewezen dat deze versies niet meer aan de veiligheidsgaranties voldoen.
De resultaten hebben betrekking op de versie van de code die door Google is gecompileerd, uitgevoerd via een klein command-line tool, en niet op « de Signal-applicaties zelf ». Sommige side-channel-aanvallen zijn ook uitgesloten van delen van de analyse. « De resultaten suggereren dat AI formele verificatie, historisch gezien te kostbaar voor de meeste software, haalbaar kan maken voor echte systemen », schrijven de onderzoekers. Ehren Kret, technisch directeur van Signal, verklaarde op zijn beurt: « Terwijl AI-gerelateerde veiligheidsdreigingen toenemen, geeft rigoureuze verificatie van de implementatie van het Signal-protocol ons nog meer vertrouwen in de privacygaranties van onze code. » Google publiceert verder de specificaties en bewijzen.
