Google DeepMind pomocí nového systému AlphaProof Code vytvořil strojově ověřené matematické důkazy bezpečnostních vlastností protokolu Signal. Práce oznámená 10. listopadu pokrývá důvěrnost zpráv, autentizaci, forward secrecy a post-compromise security a důkazy kontroluje nástroj Lean, včetně zhruba 140 000 instrukcí přeloženého strojového kódu.
Pět výzkumníků za čtyři týdny vygenerovalo přibližně 6,5 milionu řádků důkazů, což dříve trvalo specializovaným týmům roky. Pro ověření metody DeepMind vrátil do testovacích verzí dvě dříve opravené zranitelnosti Signalu a systém vytvořil důkazy, že obě upravené verze porušují bezpečnostní požadavky.
Rozsah je omezený: pokryty byly jen konverzace mezi dvěma lidmi, nikoli skupinové zprávy, více zařízení ani celá mobilní aplikace, a důkaz ověřuje jen zadané požadavky. Google zveřejnil důkazy a specifikace na GitHubu a uvádí, že komerční služba zatím neexistuje.