Исследователи Google DeepMind с помощью ИИ-агентов проверили криптографическую защиту протокола Signal и математически подтвердили ряд ключевых гарантий его безопасности. Результаты работы опубликовало издание Wired. Для анализа команда использовала инструмент AlphaProof Code, а сама проверка заняла около четырёх недель.
Протокол Signal применяется не только в одноимённом мессенджере, но и в WhatsApp* и Google Messages. DeepMind удалось доказать, что проверенные части протокола соответствуют заявленным требованиям безопасности. Новых уязвимостей исследователи не обнаружили. При этом на старых версиях Signal, в которых ранее исправили ошибки, инструмент смог выявить проблемы и показать, что такие сборки не проходят формальную проверку.
Работа стала пилотным исследовательским проектом. Проверку провели бесплатно, а её стоимость Google не раскрыла. При этом речь не идёт о полной проверке Signal, поскольку анализ охватил только отдельные компоненты протокола. Быстро выполнить задачу помогли и предыдущие исследования Signal Foundation, уже занимавшейся формальной верификацией своего ПО.
DeepMind планирует опубликовать спецификацию и математические доказательства в открытом доступе. Научный сотрудник компании Сварат Чаудхури отметил, что команда довольна результатом, но до масштабирования подобного подхода на всё программное обеспечение ещё далеко. В Signal считают, что новая методика позволит проверять гораздо большие объёмы кода, чем прежние инструменты.
* Деятельность Meta (соцсети Facebook и Instagram) запрещена в России как экстремистская.
