Google DeepMind заврши формална математичка проверка на делови од Signal протоколот, системот за енкрипција од крај до крај што се користи во Signal, WhatsApp и Google Messages. Анализата не открила нови слабости во опфатените сегменти и претставува дополнителна независна потврда за клучните безбедносни гаранции на протоколот.
Формалната верификација се разликува од вообичаеното тестирање на софтвер. Наместо само да бара познати или можни грешки, таа користи математички докази за да провери дали определени својства на системот важат според поставените правила. Во овој случај, DeepMind работел со спецификација на Signal протоколот и развил доказ за дел од неговите криптографски механизми.
Проектот бил реализиран за четири недели, но истражувачите нагласуваат дека резултатот не значи дека е проверена целата апликација Signal, ниту сите нејзини компоненти. Опфатен е самиот протокол и избрани безбедносни својства, а не комплетниот код на мобилната апликација или целата инфраструктура поврзана со услугите што го користат.
Како дополнителен тест, системот бил применет и на постари изданија на Signal кои содржеле веќе познати и поправени пропусти. Во тие случаи, проверката покажала дека протоколот не може да ги исполни условите за формална верификација, односно ги препознала проблемите што претходно биле откриени и отстранети.
DeepMind ќе ги објави спецификацијата и доказот развиени за анализата, со цел тие да послужат за понатамошна работа во областа на формалната проверка. Signal Foundation веќе имал претходна работа на вакви проверки, но таа била насочена кон помали делови од кодот. Новата анализа го проширува опфатот на проверените елементи.
Практичната примена на вакви методи во поширок обем сè уште останува отворено прашање. Ваквите проверки бараат значителни ресурси, а Google не објави колку чинела анализата ниту дали планира комерцијална услуга базирана на оваа технологија. Сепак, резултатот покажува потенцијал за построго проверување на критичен софтвер, особено кај услуги каде приватноста и безбедноста се суштински.