Google DeepMind je završio formalnu matematičku proveru delova Signal protokola, sistema za end-to-end enkripciju koji se koristi u aplikacijama Signal, WhatsApp i Google Messages. Analiza nije otkrila nove slabosti u obuhvaćenim segmentima i predstavlja dodatnu nezavisnu potvrdu ključnih bezbednosnih garancija protokola.
Formalna verifikacija se razlikuje od uobičajenog testiranja softvera. Umesto da samo traži poznate ili moguće greške, ona koristi matematičke dokaze da proveri da li određena svojstva sistema važe prema postavljenim pravilima. U ovom slučaju, DeepMind je radio sa specifikacijom Signal protokola i razvio dokaz za deo njegovih kriptografskih mehanizama.
Projekat je realizovan za četiri nedelje, ali istraživači naglašavaju da rezultat ne znači da je proverena cela aplikacija Signal, niti sve njene komponente. Obuhvaćeni su sam protokol i odabrana bezbednosna svojstva, a ne kompletan kod mobilne aplikacije ili cela infrastruktura povezana sa uslugama koje ga koriste.
Kao dodatni test, sistem je primenjen i na starija izdanja Signala koja su sadržala već poznate i ispravljene propuste. U tim slučajevima, provera je pokazala da protokol ne može da ispuni uslove za formalnu verifikaciju, odnosno prepoznala je probleme koji su prethodno bili otkriveni i uklonjeni.
DeepMind će objaviti specifikaciju i dokaz razvijene za analizu, kako bi poslužili za dalji rad u oblasti formalne provere. Signal Foundation je već imao prethodni rad na ovakvim proverama, ali je on bio usmeren na manje delove koda. Nova analiza proširuje obuhvat proverenih elemenata.
Praktična primena ovakvih metoda u širem obimu i dalje ostaje otvoreno pitanje. Ovakve provere zahtevaju značajne resurse, a Google nije objavio koliko je analiza koštala niti da li planira komercijalnu uslugu zasnovanu na ovoj tehnologiji. Ipak, rezultat pokazuje potencijal za strožu proveru kritičnog softvera, naročito kod usluga gde su privatnost i bezbednost ključne.