Google DeepMind формально верифицировала часть протокола Signal — Ars Technica

Google DeepMind с помощью агентного искусственного интеллекта математически подтвердила ряд ключевых криптографических гарантий протокола Signal. Исследовательский проект, продолжавшийся четыре недели, носил демонстрационный характер и использовал новый ИИ-фреймворк AlphaProof Code, сообщает Ars Technica.

Проверка криптографических свойств

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

По данным издания, агентный ИИ способен существенно сократить время, необходимое для создания такого доказательства. В то же время исследование DeepMind имело ограниченный масштаб: оно не охватывало всё мобильное приложение Signal, а касалось отдельных частей протокола.

В ходе анализа исследователи не выявили новых уязвимостей в проверенных частях протокола Signal. Когда AlphaProof Code применили к более ранним версиям Signal с известными и давно исправленными проблемами, система правильно обнаружила эти уязвимости и показала, что при их наличии протокол невозможно формально верифицировать.

Больше актуальных новостей — в Telegram-канале UA.News Telegram.

Ограничения исследования

В DeepMind подчеркнули, что результат является лишь одним этапом более широкой работы. Масштабирование формальной верификации с помощью ИИ на большие объёмы программного кода и все программные системы всё ещё требует дальнейшего развития.

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

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

В DeepMind описали подход как сотрудничество человека и ИИ: агенты могут помогать на разных этапах и исправлять собственную работу, однако на ключевых этапах предусмотрены человеческий вклад и проверка.