Google DeepMind ha annunciato il 10 novembre 2026 di avere verificato matematicamente proprietà di sicurezza selezionate del codice crittografico usato da Signal. Il progetto AlphaProof Code combina specifiche formulate da ricercatori, agenti AI e un sistema di controllo delle dimostrazioni. Non dimostra che ogni componente dell’app Signal sia invulnerabile, né elimina i rischi legati a phishing e compromissione dei dispositivi.
La comunicazione ufficiale Google DeepMind descrive un risultato significativo per la verifica formale del software: invece di limitarsi a controllare il modello teorico, il gruppo ha analizzato proprietà crittografiche del codice reale. L’interesse non riguarda una nuova funzione da attivare nell’app, ma la possibilità di trovare e prevenire errori in componenti fondamentali.
Che cosa è stato dimostrato su Signal?
Gli autori hanno affrontato proprietà crittografiche specifiche di libsignal, la libreria che implementa componenti dei protocolli di messaggistica protetta. La verifica formale dimostra che determinate condizioni matematiche sono rispettate dal codice analizzato, tenendo conto delle ipotesi definite dagli specialisti.
Una parte rilevante del lavoro arriva al livello del codice macchina AArch64. È un passaggio importante: una prova relativa soltanto al protocollo astratto non sarebbe sufficiente, da sola, a garantire che un’implementazione concreta si comporti nello stesso modo.
Tra gli obiettivi vi sono garanzie crittografiche relative alla sicurezza delle comunicazioni e alla protezione dei messaggi entro modelli che considerano possibili compromissioni. Il risultato va letto come una prova delimitata, non come una certificazione complessiva di telefoni, applicazioni, rete e utenti.
Come funziona AlphaProof Code?
La ricerca combina il lavoro di esperti che definiscono le proprietà da dimostrare e l’impiego di agenti di intelligenza artificiale che costruiscono le prove. Le dimostrazioni vengono poi controllate tramite strumenti formali basati su Lean: non basta che il modello generativo affermi che una proprietà è vera.
Secondo il materiale tecnico pubblicato con l’annuncio, il progetto ha prodotto milioni di righe di prove controllate automaticamente e un insieme di specifiche e semantiche che costituisce parte della base fidata. L’annuncio riporta circa quattro settimane di lavoro per il progetto: il dato descrive questa esperienza, non un tempo garantito per qualsiasi verifica futura.
Signal è diventato sicuro al cento per cento?
No. La dimostrazione formale rafforza le garanzie soltanto entro il perimetro delle proprietà, delle specifiche e delle versioni del codice considerate. Non esclude in assoluto difetti in componenti non analizzate né protegge contro chi convince un utente a consegnare credenziali o codici di recupero.
| Cosa aggiunge la ricerca | Cosa non prova |
|---|---|
| Prove matematiche per proprietà selezionate | Assenza di ogni possibile vulnerabilità |
| Analisi profonda dell’implementazione | Sicurezza di ogni versione futura o piattaforma |
| Controllo automatico delle dimostrazioni | Immunità a malware, furto del telefono e phishing |
| Metodo promettente per altri software | Applicabilità immediata a tutti i sistemi critici |
Chi usa Signal deve quindi continuare a proteggere il proprio dispositivo, aggiornare il software e diffidare dei falsi messaggi di assistenza. La nostra guida alla truffa Signal Support spiega perché la protezione crittografica non impedisce a un attaccante di tentare il furto delle credenziali o delle informazioni di recupero.
Perché la verifica del codice macchina conta
Un algoritmo formalmente solido può diventare vulnerabile se viene implementato con errori. Dimostrare proprietà del software effettivo riduce questo divario, ma richiede di modellare con precisione istruzioni, condizioni di esecuzione e ipotesi crittografiche. La ricerca di DeepMind è interessante proprio per la profondità della catena di verifica.
Il lavoro è descritto nella documentazione tecnica collegata all’annuncio, insieme agli artefatti che il gruppo dichiara di voler rendere disponibili alla comunità. La riproducibilità da parte di gruppi indipendenti e l’estensione ad altri componenti restano aspetti da valutare nel tempo.
Cosa cambia per gli utenti e per chi sviluppa software?
Per gli utenti non c’è una nuova impostazione Signal da abilitare: la notizia è un avanzamento nella ricerca sulle tecniche di sicurezza. Per gli sviluppatori, invece, AlphaProof Code propone un percorso verso verifiche più profonde di software complesso, con potenziali applicazioni future anche oltre la messaggistica.
Una prova matematica non sostituisce da sola test, aggiornamenti e risposta agli incidenti. Può aggiungere un livello di garanzia molto forte su domande precise, purché la specifica rappresenti davvero la proprietà desiderata e il codice eseguito corrisponda alla porzione verificata.
La conclusione corretta è che alcune garanzie crittografiche di Signal hanno ricevuto una verifica formale particolarmente approfondita, non che l’app sia al riparo da ogni attacco. Questa distinzione rende il risultato scientificamente più utile e comprensibile anche fuori dall’ambito della ricerca.
Entra nella conversazione
Condividi il tuo punto di vista: non serve creare un account. I contributi restano soggetti alla moderazione editoriale.