ИИ от Google DeepMind за месяц доказал неуязвимость шифрования Signal

Команда Google DeepMind провела необычный эксперимент: всего за четыре недели новый инструмент на базе искусственного интеллекта AlphaProof Code формально верифицировал ключевые части криптографического протокола Signal. Этот протокол лежит в основе сквозного шифрования в мессенджерах Signal, WhatsApp и Google Messages, которыми пользуются миллиарды людей. Результат важен вдвойне.

Во-первых, он служит независимым подтверждением стойкости защиты, на которую полагается огромный объём мировых коммуникаций. Во-вторых, работа демонстрирует возможности AlphaProof Code — новой системы автоматизированного доказательства корректности кода, разработанной в DeepMind. Формальная верификация десятилетиями считалась своего рода святым граалем в безопасности программ.

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

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

Однако когда исследователи скормили AlphaProof Code старые сборки с известными и давно исправленными багами, инструмент безошибочно их обнаружил и показал, что в таком виде протокол формально верифицировать невозможно. Скорость проекта отчасти объясняется заделом, который ранее создал фонд Signal. «Предыдущие формальные проверки охватывали меньшие участки кода, а подход Google DeepMind позволяет значительно расширить масштаб», — отметил технический директор Signal Эрен Крет.

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

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

Подобные инструменты, как и недавние инициативы OpenAI объединит лимиты ChatGPT и Codex: общий ресурс для общения и кода с декабря 2026 года, показывают, что индустрия движется к более тесной интеграции ИИ в процессы разработки и аудита кода. Главный вопрос, который висит над всей отраслью, — сможет ли автоматизированная формальная верификация действительно стать массовой и экономически оправданной. DeepMind провела анализ Signal бесплатно, в рамках исследовательского проекта, и в Google отказались раскрыть его стоимость, а также комментировать планы по коммерциализации подобных сервисов.

Если технологию удастся масштабировать, выиграют все, кто зависит от безупречной работы критического софта. «Можно представить банки и компании, которые сегодня трясутся над каждой ошибкой, — рассуждает главный научный сотрудник Google Cloud и вице-президент DeepMind по исследованиям Пушмит Кохли. — Если вы способны доказать корректность реализации, можно спать спокойно».

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