DeepMind verifica formalmente il protocollo Signal e punta a tutto il software

I ricercatori di Google DeepMind sono riusciti a verificare formalmente il protocollo Signal, lo schema di crittografia alla base di molte applicazioni di messaggistica. La dimostrazione stabilisce che il protocollo si comporta come previsto, cioè che le garanzie dichiarate dai suoi autori reggono a un'analisi matematica e non soltanto a prove empiriche su casi scelti [1].

Verificare formalmente significa dimostrare che ogni esecuzione possibile rispetta una specifica di partenza. È un passaggio diverso dal collaudo del codice di una singola app: la verifica riguarda il protocollo in sé, quindi vale per qualunque implementazione che ne rispetti le regole, non per un prodotto specifico [1].

La rilevanza sta nella diffusione dello schema: Signal è descritto come un protocollo di crittografia largamente usato, e una prova formale della sua correttezza riguarda una platea ampia di servizi che lo adottano, non un caso isolato di laboratorio [1].

Il gruppo non si è fermato al risultato immediato. Il suo obiettivo dichiarato, definito dagli stessi ricercatori come obiettivo a lungo termine, è fare la stessa cosa per «tutto il software del mondo», cioè estendere la verifica formale oltre i protocolli di comunicazione [1].

Restano aperti diversi punti. Il titolo non indica quanto tempo abbia richiesto la verifica, quali componenti del protocollo siano stati coperti, né se i risultati siano stati sottoposti a revisione indipendente. L'estensione a tutto il software è per ora un proposito, non un risultato [1].