Как Google DeepMind использует ИИ-агентов для проверки основного машинного кода Signal

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

Работа вышла за рамки абстрактной модели устройства протокола Signal и охватила его скомпилированную реализацию. Исследователи поместили неизменённые крейты libsignal v0.105.4 и SPQR v1.6.0 в небольшую оболочку командной строки, а затем с помощью стандартного rustc собрали статически скомпонованный исполняемый файл для Linux на AArch64. В технической статье результат назван первым доказательством безопасности на уровне протокола для неизменённого кода широко используемой реализации криптографического протокола.

Как AlphaProof Code распределила работу

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

Люди выбирали свойства, разрешали неоднозначности и определяли компромиссы в вопросах безопасности, проверяли спецификации и сохраняли за собой право окончательного утверждения. Агенты на базе Gemini 4 Carbon и Claude Opus 5.5 составляли и проверяли эти спецификации; проверку также проводила модель другого семейства. Затем команды агентов Gemini 4 Carbon сгенерировали весь код доказательств — ни один из авторов не писал его вручную. В обычных запусках на одном компьютере одновременно работали от 40 до 80 агентов в течение 24–72 часов: оркестратор и руководители команд координировали работу агентов, создававших доказательства, а архитекторы и интеграторы поддерживали общую базу доказательств.

Проверяющий модуль принимал доказательство только после того, как его проверяло ядро Lean, а средство сравнения подтверждало его соответствие скрытой от агентов спецификации, утверждённой человеком, включая все транзитивные определения; при этом допускались только стандартные аксиомы Lean. Если в доказательствах обнаруживались проблемы со спецификациями, агенты могли предлагать небольшие поправки, но изменения доверенных допущений требовали одобрения человека или политики, заданной пользователем, и регистрировались с обоснованиями. Этот механизм устраняет задокументированный риск, связанный с доказательствами, создаваемыми агентами: спецификацию можно ослабить косвенным образом, изменив одно из её определений.

Охват проверки безопасности и тестирование на исторических уязвимостях

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

Чтобы проверить, способны ли эти спецификации выявлять реальные ошибки, команда отменила исправления двух ранее устранённых ошибок libsignal — известных как «слабое состояние» и «малая подгруппа» — и заново скомпилировала изменённые двоичные файлы. В обоих случаях исследователи создали доказательства на Lean, показывающие, что символическая теорема безопасности не выполняется. В общедоступном репозитории с материалами проверки отдельно размещены материалы по вычислительным и символическим доказательствам, общие двоичные файлы и материалы по семантике AArch64; там же описано, как повторно собрать файлы и независимо проверить доказательства.

Технический директор Signal Эрен Крет заявил, что эта работа «ещё больше укрепляет нашу уверенность в гарантиях конфиденциальности нашего кода».

Ограничения и дальнейшие шаги

Эти гарантии не дают оснований считать полностью сертифицированными приложения Signal. Они относятся к сборке libsignal-cli, подготовленной исследователями и запущенной как новый процесс; генерация ключей не проверялась, групповые сообщения оставлены для будущих исследований, а побочные каналы и состояние на нескольких устройствах не входят в рассматриваемый сценарий. Низкоуровневые криптографические примитивы, а также отдельные функции вывода и библиотечные процедуры представлены доверенными контрактами. Поэтому результат зависит и от этих контрактов, утверждённых спецификаций, ядра Lean, семантики AArch64 и допущений о примитивах.

В статье указано, что ни одно из двух доказательств не подтверждает постквантовое восстановление защиты, которое призван обеспечить SPQR: вычислительная теорема охватывает классических атакующих, тогда как в символических теоремах о ратчете атакующий может выбирать ключи SPQR. Кроме того, вычислительная модель ограничивает ряд действий атакующего и становится тривиально истинной при достаточно большом числе сообщений и сессий. Эти границы определяют, чему должен доверять внешний проверяющий, прежде чем считать машинно проверяемые доказательства гарантией безопасности для конкретного развёртывания.

Исследователи называют следующие дальнейшие шаги: усилить теоремы, сократить доверенную базу за счёт проверки большего числа подключённых процедур и привязки криптографических контрактов к проверенным реализациям, а также расширить охват на групповые сообщения, запечатанного отправителя и серверные протоколы. Цель проверять новые выпуски libsignal до их поставки — это исследовательская задача, а не объявленный план внедрения.

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