10 ноября 2026 г., Исследования
Пушмит Кохли и Сварат Чаудхури
Как исследователи из Google DeepMind создали новую агентную структуру, которая формально верифицировала код криптографического протокола Signal, долгое время считавшегося сложнейшей задачей в области безопасности
Сегодня мы делимся вехой в сфере безопасности программного обеспечения, которая долгое время считалась сложнейшей задачей: исследователи Google DeepMind направили ИИ-агентов на математическое доказательство ключевых свойств безопасности реального кода, лежащего в основе протокола Signal — технологии, которая защищает миллиарды личных разговоров в таких приложениях, как Signal и Google Messages.
Это прорывное открытие было сделано с помощью AlphaProof Code, новой агентной структуры для формальной верификации на беспрецедентной глубине, которая объединяет человеческий опыт и ИИ-агентов. Формальная верификация — математическое доказательство правильной работы кода без сбоев — это высочайший стандарт обеспечения безопасности; однако она сложна и часто требует больших трудозатрат.
Наша работа знаменует собой первый случай использования ИИ для формальной верификации широко используемого криптографического протокола на такой глубине. Это также первый случай, когда реализация подобного широко распространенного протокола была формально верифицирована каким-либо методом, с использованием ИИ или без него.
Как мы верифицировали Signal
AlphaProof Code — это многомодельная агентная структура на базе LLM, которая распределяет работу по формальной верификации так, как это делала бы исследовательская команда: эксперты-люди работают с ИИ, чтобы определить, что именно нужно доказать, а группа ИИ-агентов выполняет эту задачу.
Сначала наши исследователи в сотрудничестве с комбинацией моделей перевели цели безопасности Signal в формальные математические спецификации, причем эксперты-люди проверяли каждую из них. После этого агенты на базе Gemini Carbon выполнили доказательства, сгенерировав более шести миллионов строк кода на Lean — компьютерном языке, который математически доказывает точность кода.
Затем агенты провели аудит доказательства и выделили области, требующие повторного внимания человека, — всего один процент кодовой базы, что позволило сэкономить колоссальное количество времени. Поскольку Lean автоматически проверяет остальную часть, наши эксперты смогли сосредоточить свою проверку там, где человеческое суждение имеет наибольшее значение.
Криптографические протоколы лежат в основе практически всех цифровых коммуникаций: от онлайн-банкинга до веб-серфинга, и всего одна уязвимость может одновременно подвергнуть риску миллионы людей. Именно поэтому эксперты тратят десятилетия на их формальный анализ.
Но большая часть верификации протоколов останавливается на уровне проектирования. Наши агенты пошли дальше, доказав, что скомпилированный код отвечает ключевым свойствам безопасности — таким как защита сообщений до и после временного взлома устройства — вплоть до точного кода, выполняющегося на устройствах. Поскольку реальные уязвимости часто скрываются в зазоре между проектированием и реализацией, преодоление этого разрыва делает такие доказательства намного более сложными.
Даже при такой сложности наш процесс верификации занял всего четыре недели (задача, на решение которой у экспертных команд исторически уходили годы), доказав, что основной криптографический код Signal обеспечивает защиту безопасности, заданную нашими экспертами.
Чтобы подтвердить, что AlphaProof Code способен отличать корректный код от кода с ошибками, мы внедрили две реальные, ранее исправленные ошибки в изолированную версию кода Signal. В обоих случаях система создала проверенное машинными средствами доказательство того, что версия с ошибками небезопасна.
В AlphaProof Code ИИ-агенты помогают пользователям написать спецификацию, а затем автономно доказывают, что реализация ей соответствует. Каждое доказательство проверяется в Lean для верификации работы агентов.
Хотя предыдущие работы по формальной верификации неизбежно фокусировались на более узких масштабах, этот новый подход позволяет значительно расширить их рамки. Традиционно верификация того, что производственный код строго соответствует своему криптографическому проекту, требовала огромных ручных усилий, поэтому использование ИИ-агентов для автоматического перевода реального кода в корректные теоремы Lean является большим прорывом. По мере роста угроз безопасности, управляемых ИИ, строгая верификация основного протокола Signal с помощью автоматизированного доказывания теорем дает нам еще большую уверенность в том, что наш код выполняет свои гарантии конфиденциальности.
Будущее безопасности
Решение этой давней задачи демонстрирует, как ИИ может обеспечить высочайший уровень безопасности для бизнеса, правительств и критической инфраструктуры, помогая защищаться от киберугроз, управляемых агентами.
Верификация основных криптографических механизмов Signal закладывает основу для защиты других жизненно важных систем: от прошивки медицинских устройств до программного обеспечения электросетей.
Масштабирование этих методов требует продолжения исследований. В сочетании с агентами автоматизированной защиты, такими как CodeMender, формальная верификация может помочь противостоять скорости и масштабу современных киберугроз для создания программного обеспечения с математическим доказательством работоспособности его средств защиты.
Мы открываем исходный код наших артефактов формальной верификации для использования сообществом. Ознакомьтесь с техническим документом ниже.
Благодарности
Это исследование было проведено Сваратом Чаудхури, Эндрю Ферраьюоло, Антоном Ковшаровым, Тейем Чаджедом, Сэмом Шлезингером, Карном Сетом, Джонатаном Катцем, Чарльзом Саттоном и Пушмитом Кохли.
Мы благодарим Эрика Визера за помощь в открытии исходного кода, Оуэна Джонса за поддержку в управлении проектом, а также Мартина Абади, Кристофера Хенсона, Катерину Христову, Генрика Михалевского, Джонатана Протченко и Джорджа Цукаласа за полезные обсуждения. Мы благодарны Рольфу Шмидту, Майклу Розенбергу и Эрену Крету из компании Signal за отзывы о нашей методологии. Мы также благодарим Тулси Доши, Фора Флинна, Кейт Ольшевскую, Алисию Хуан, Энди Лю, Бенуа Шиллингса, Ралуку Аду Попу, Мелвина Джонсона, Корая Кавукджуоглу, Демиса Хассабиса и Сундара Пичаи за поддержку проекта.
