Google ha ampliato l’accesso a Gemini 4 Carbon e indica che agenti costruiti su questo modello hanno contribuito a verificare formalmente garanzie di sicurezza centrali del codice del protocollo Signal.
- Google amplia l’accesso a Gemini 4 Carbon a sviluppatori, aziende e abbonati Google AI Ultra.
- Agenti basati su Carbon hanno contribuito a verificare formalmente le garanzie di sicurezza di libsignal.
- Cinque ricercatori hanno completato il lavoro di prova in quattro settimane, generando circa 6,5 milioni di righe in Lean.
- I risultati riguardano il codice compilato testato, non le applicazioni Signal stesse.
Gli sviluppatori e le aziende che pagano possono ora utilizzare Carbon tramite l’API Gemini e Gemini for business, e gli abbonati Google AI Ultra vi hanno anche accesso. Si applicano tariffe di introduzione di 2 $ e 10 $ per milione di token in input e in output fino al 30 novembre, prima di essere raddoppiate. Un token è un’unità di testo che il modello elabora per leggere o produrre contenuti.
Fino ad ora, solo alcuni difensori della cybersicurezza membri del programma Fairwind di Google potevano utilizzare Carbon. Devono comunque appartenere a questo programma per accedere a Carbon for cyber, una versione che Google presenta come in testa ai principali benchmark di rilevamento, sfruttamento e correzione delle vulnerabilità.
Applicazioni nella cybersicurezza
Secondo Google, la società Wiz ha utilizzato Carbon for cyber per trovare falle di tipo « zero-day » presso due grandi fornitori di SaaS, in due ore. Il team Cloud Vulnerability Research (CVR) di Google ha, da parte sua, utilizzato il modello per confermare che due bug di un progetto open source popolare erano sfruttabili, con una gravità paragonabile a quella di PHP2Shell, una coppia di falle PHP già sfruttate da attaccanti.
« Utilizzando Carbon per costruire una proof of concept, CVR ha aiutato i manutentori a riclassificare il bug come critico e a pubblicare rapidamente una patch », indica Google.
Verificare il codice di Signal
Inoltre, Google DeepMind ha presentato AlphaProof Code, che associa esperti umani ad agenti di IA per verificare formalmente software, cioè dimostrare matematicamente che rispettano requisiti definiti. Il team lo ha applicato a libsignal, l’implementazione di riferimento del protocollo Signal. Versioni di questo protocollo funzionano anche in WhatsApp e Google Messages.
Degli umani hanno lavorato con agenti eseguiti su Carbon e su Claude Opus 5.5 per redigere le specifiche descriventi ciò che doveva essere provato. Agenti basati su Carbon hanno poi generato la totalità delle circa 6,5 milioni di righe di prove scritte in Lean, un assistente per le prove che rifiuta quelle invalide. Secondo Google, le garanzie provate, tra cui il segreto persistente (forward secrecy), la sicurezza dopo compromissione e l’autenticazione, valgono per il codice macchina compilato, mentre la maggior parte delle verifiche di protocolli riguarda solo la progettazione.
Cinque ricercatori hanno realizzato il lavoro di prova in quattro settimane, un lavoro che Google stima tradizionalmente riservato a specialisti per anni. Per verificare che il metodo rilevi vere falle, il team ha reintrodotto due vecchi bug di libsignal, già corretti, e ha provato che queste versioni non rispettano più le garanzie di sicurezza.
I risultati riguardano la versione del codice compilata da Google, eseguita tramite un piccolo strumento da riga di comando, e non sulle « applicazioni di Signal stesse ». Alcuni canali ausiliari sono stati anche esclusi da parti dell’analisi. « I risultati suggeriscono che l’IA può rendere la verifica formale, storicamente troppo costosa per la maggior parte dei software, praticabile per sistemi reali », scrivono i ricercatori. Ehren Kret, direttore tecnico di Signal, ha da parte sua dichiarato: « Mentre le minacce di sicurezza legate all’IA si moltiplicano, la verifica rigorosa dell’implementazione del protocollo Signal ci dà una fiducia ancora maggiore nelle garanzie di riservatezza del nostro codice. » Google pubblica inoltre le specifiche e le prove.
