DeepMind verifica matematicamente parti chiave del protocollo Signal

Google DeepMind ha verificato matematicamente parti chiave del protocollo di Signal, in un progetto durato quattro settimane [4]. La verifica formale dimostra con strumenti matematici che un software si comporta come dichiarato, invece di limitarsi a testarne il funzionamento su casi campione.

Signal è un sistema di messaggistica cifrata molto diffuso, e una prova formale su sue componenti riguarda proprietà di sicurezza del protocollo. Secondo la fonte, il progetto suggerisce che l'AI possa rendere la verifica formale molto più praticabile [4], cioè applicabile a software che finora restava fuori dalla portata dei team di sviluppo.

La verifica formale è costosa e richiede specialisti, per questo è rimasta confinata a componenti critici. Se un modello può accelerare la stesura delle dimostrazioni, il collo di bottiglia si sposta sulla definizione di ciò che va dimostrato e sulla revisione umana del risultato [4].

Non è indicato quali parti del protocollo siano state verificate, con quali strumenti, né se i risultati siano stati controllati da revisori indipendenti. DeepMind non ha annunciato un prodotto: il valore della notizia è la dimostrazione di fattibilità su un bersaglio reale e in tempi brevi [4].