Google a élargi l’accès à Gemini 4 Carbon et indique que des agents construits sur ce modèle ont contribué à vérifier formellement des garanties de sécurité centrales du code du protocole Signal.
- Google élargit l’accès à Gemini 4 Carbon aux développeurs payants, à Gemini for business et aux abonnés Google AI Ultra.
- Des agents fondés sur Carbon génèrent des preuves formelles pour vérifier le code libsignal du protocole Signal.
- Cinq chercheurs terminent ce travail de preuve en quatre semaines, alors qu’il exigeait auparavant des années de spécialistes.
- Les résultats concernent la version compilée testée par Google, et non les applications Signal elles-mêmes.
Les développeurs et entreprises qui paient peuvent désormais utiliser Carbon via l’API Gemini et Gemini for business, et les abonnés Google AI Ultra y ont également accès. Des tarifs d’introduction de 2 $ et 10 $ par million de tokens en entrée et en sortie s’appliquent jusqu’au 30 novembre, avant d’être doublés. Un token est une unité de texte que le modèle traite pour lire ou produire du contenu.
Jusqu’ici, seuls certains défenseurs en cybersécurité membres du programme Fairwind de Google pouvaient utiliser Carbon. Ils doivent toujours appartenir à ce programme pour accéder à Carbon for cyber, une version que Google présente comme en tête des principaux benchmarks de détection, d’exploitation et de correction des vulnérabilités.
Des applications en cybersécurité
Selon Google, la société Wiz a utilisé Carbon for cyber pour trouver des failles de type « zero-day » chez deux grands fournisseurs de SaaS, en deux heures. L’équipe Cloud Vulnerability Research (CVR) de Google a, de son côté, utilisé le modèle pour confirmer que deux bogues d’un projet open source populaire étaient exploitables, avec une gravité comparable à celle de PHP2Shell, une paire de failles PHP déjà exploitées par des attaquants.
« En utilisant Carbon pour construire une preuve de concept, CVR a aidé les mainteneurs à reclasser le bogue comme critique et à publier rapidement un correctif », indique Google.
Vérifier le code de Signal
Par ailleurs, Google DeepMind a présenté AlphaProof Code, qui associe des experts humains à des agents d’IA pour vérifier formellement des logiciels, c’est-à-dire démontrer mathématiquement qu’ils respectent des exigences définies. L’équipe l’a appliqué à libsignal, l’implémentation de référence du protocole Signal. Des versions de ce protocole fonctionnent aussi dans WhatsApp et Google Messages.
Des humains ont travaillé avec des agents exécutés sur Carbon et sur Claude Opus 5.5 pour rédiger les spécifications décrivant ce qui devait être prouvé. Des agents fondés sur Carbon ont ensuite généré la totalité des quelque 6,5 millions de lignes de preuves écrites en Lean, un assistant de preuves qui rejette celles qui sont invalides. Selon Google, les garanties prouvées, dont le secret persistant (forward secrecy), la sécurité après compromission et l’authentification, valent pour le code machine compilé, alors que la plupart des vérifications de protocoles portent seulement sur la conception.
Cinq chercheurs ont réalisé le travail de preuve en quatre semaines, un travail que Google estime traditionnellement réservé à des spécialistes pendant des années. Pour vérifier que la méthode détecte de vraies failles, l’équipe a réintroduit deux anciens bogues de libsignal, déjà corrigés, et a prouvé que ces versions ne respectent plus les garanties de sécurité.
Les résultats portent sur la version du code compilée par Google, exécutée via un petit outil en ligne de commande, et non sur « les applications de Signal elles-mêmes ». Certains canaux auxiliaires ont également été exclus de parties de l’analyse. « Les résultats suggèrent que l’IA peut rendre la vérification formelle, historiquement trop coûteuse pour la plupart des logiciels, praticable pour des systèmes réels », écrivent les chercheurs. Ehren Kret, directeur technique de Signal, a pour sa part déclaré : « Alors que les menaces de sécurité liées à l’IA se multiplient, la vérification rigoureuse de l’implémentation du protocole Signal nous donne une confiance encore plus grande dans les garanties de confidentialité de notre code. » Google publie par ailleurs les spécifications et les preuves.
