Google DeepMind формально доказала безопасность протокола Signal

Что именно проверили

Протокол Signal давно считают эталоном сквозного шифрования, его публично поддерживал, в частности, Эдвард Сноуден. Теперь аналитики DeepMind «формально верифицировали» его безопасность.

Формальная верификация — это математическое доказательство (или опровержение) того, что криптографический алгоритм или протокол выполняет свои гарантии безопасности при любых условиях. Обычное тестирование ищет уязвимости, но не может обещать, что других нет. Формальное доказательство, напротив, исключает сценарии, в которых протокол даст сбой.

Важная оговорка: проверили сам протокол, а не приложение Signal целиком. Ошибки в реализации, интерфейсе или на устройстве пользователя этой работой не охватываются.

Как это сделали и почему это важно

Для верификации использовали агентный ИИ — системы, которые самостоятельно выполняют цепочки задач. По оценке 9to5Mac, применение таких агентов для формальных доказательств — крупный шаг и для криптографии, и для самого ИИ.

Для проверки метода исследователи прогнали его на старых версиях Signal с уже известными уязвимостями. ИИ нашёл эти проблемы и пометил версии как не прошедшие верификацию. Это косвенно подтверждает, что инструмент действительно отличает надёжный протокол от дырявого.

Команда опиралась и на более раннюю работу по формальной верификации, выполненную без ИИ. Анализ занял четыре недели, а сколько вычислительных ресурсов потребовалось, Google не раскрывает.

Что это значит для пользователей

На практике ничего менять не нужно: если вы пользуетесь Signal, WhatsApp или Google Messages, вывод для вас один — математическая основа шифрования подтверждена ещё одним, очень строгим способом. Это не отменяет базовых правил: обновлять приложения, не передавать коды подтверждения и следить за безопасностью самого устройства.

Массовой проверки других протоколов ждать не стоит. Метод очень требователен к вычислительным мощностям, и, как сообщила Google изданию Wired, пока неясно, насколько практично применять его шире. Исследователь DeepMind Сварат Чаудхури заявил Wired, что результат радует, но до масштабирования на весь софт мира ещё «большая дистанция», хотя команда хочет к этому прийти.