Google DeepMind с помощью ИИ проверила криптографический код Signal

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

Проект занял четыре недели и потребовал участия пяти исследователей. За это время агенты на базе Gemini 4 Carbon создали около 6,5 млн строк доказательств на языке Lean, которые проверялись математическим ядром этой системы. Результаты опубликованы вместе с технической документацией и исходным кодом, чтобы другие специалисты могли изучить и воспроизвести проверку.

Какие механизмы безопасности Signal проверили исследователи

Основным объектом исследования стала библиотека libsignal, реализующая криптографический протокол Signal. Этот протокол используется для сквозного шифрования сообщений не только в одноименном мессенджере, но и в других коммуникационных сервисах, включая WhatsApp и Google Messages. Ученые изучили два важных механизма: PQXDH, отвечающий за защищенный обмен ключами при установлении соединения, и Triple Ratchet, который обновляет криптографические ключи по мере переписки.

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

В отличие от традиционной проверки математической модели протокола, DeepMind изучала непосредственно скомпилированную реализацию. Для этого ученые использовали версию libsignal 0.105.4 и исследовали исполняемый код для архитектуры AArch64, применяемой в процессорах Arm. Такой подход позволяет проверить не только криптографическую схему, но и то, насколько ее программная реализация соответствует заданным свойствам безопасности.

Как AlphaProof Code использует ИИ для проверки программ

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

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

В ходе исследования было подготовлено около 6,5 млн строк машинно проверенных доказательств. Они опирались примерно на 26 000 строк доверенных спецификаций и описания работы процессорной архитектуры. Система также выделяла участки, требующие дополнительной проверки людьми, что позволяло исследователям сосредоточиться на наиболее важных допущениях.

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

Означает ли это, что Signal полностью защищен

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

Кроме того, математические доказательства действуют при определенных предположениях о безопасности используемых криптографических алгоритмов. Исследователи применили две модели: символическую, в которой криптографические операции рассматриваются в идеализированном виде, и вычислительную, учитывающую возможности атакующих при заданных условиях. При этом вычислительное доказательство не распространяется на квантовых противников, а некоторые постквантовые свойства Triple Ratchet еще требуют отдельной проверки.

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

Почему исследование важно для разработки программ

По оценке Google DeepMind, AlphaProof Code может существенно снизить трудозатраты на формальную проверку сложного программного обеспечения. Ранее такие проекты занимали годы работы специалистов: например, формальная верификация микроядра операционной системы seL4 потребовала около 20 человеко-лет, а разработка проверенного компилятора CompCert C заняла шесть лет.

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

В дальнейшем Google DeepMind рассчитывает применять подобные методы к другим сложным программным системам, включая банковское программное обеспечение и критически важную инфраструктуру. Однако возможность масштабирования технологии на большие кодовые базы, стоимость вычислений и объем необходимого человеческого контроля пока остаются открытыми вопросами.