Команда из пяти человек и искусственный интеллект доказали свойства кода Signal за четыре недели

Четыре недели. Именно столько времени потребовалось команде из пяти человек из Google DeepMind, работающей с ИИ-агентами, чтобы создать проверенные машинным способом доказательства ключевых свойств безопасности в скомпилированном коде основной библиотеки чата Signal. Доказательства занимают около 6,5 миллионов строк. Более ранние масштабные работы над другими системами занимали годы работы специалистов и обычно требовали написания кода, который нужно было доказать.

В исследовательской публикации от 10 ноября 2026 года изложен метод и его ограничения. В сопроводительном техническом документе эти данные представлены более подробно. Данная работа не является доказательством работоспособности приложения Signal в целом и не является доказательством работоспособности других приложений, использующих аналогичную архитектуру. Это доказательство определенных свойств библиотеки libsignal, эталонной библиотеки, для сессий «один к одному», доведенное до скомпилированного машинного кода, который фактически выполняется.

Что было доказано

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

Команда скомпилировала неизмененную библиотеку — версию 0.105.4, а также связанный с ней крейт SPQR версии 1.6.0 — с помощью обычного компилятора Rust в небольшой инструмент командной строки, работающий на 64-битной Arm Linux. Доказательства относятся именно к этому исполняемому файлу, а не к его переписанной версии. Проверенная библиотека занимает около 560 КБ, или примерно 140 000 машинных инструкций.

Они рассматривают рукопожатие PQXDH, с помощью которого два человека начинают приватную сессию, включая постквантовый этап, предназначенный для противостояния будущим квантовым компьютерам, и Triple Ratchet, который выдает новый ключ для каждого сообщения. В “символической” модели, которая рассматривает лежащую в основе криптографию как идеальную, в статье также утверждается о секретности рукопожатия против последующего злоумышленника с квантовым компьютером. Групповые чаты, запечатанный отправитель и протокол на стороне сервера остаются предметом дальнейших исследований.

Как выполнялась работа

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

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

В исследовательской работе говорится, что агенты для проверки работали на платформе Gemini Carbon. Сама работа по проверке была выполнена пятью исследователями в течение четырех недель, каждый из которых запускал агенты на своей рабочей станции. Это короткая кампания по меркам данной области. В статье отмечается, что микроядро seL4, известный пример более ранней проверки, заняло двадцать человеко-лет, а компилятор CompCert C — шесть. Оба этих кода были написаны с учетом проверки. Библиотека libsignal — нет.

Хотите, чтобы ИИ экономил вам часы в неделю? Наше бесплатное руководство покажет вам, как это сделать.Получите бесплатное руководство →

Сами доказательства могут быть длинными, поскольку в них говорится о машинном коде. Около 6,5 миллионов строк составляют доказательства: 5,3 миллиона — о двоичном коде, плюс отдельные файлы для двух моделей безопасности. Читателю, желающему доверять утверждениям в заголовке, все равно придется прочитать проверенные части: около 18 000 строк спецификации в репозитории, плюс около 8 000 строк модели машинного кода Arm и имена символов, сопоставленные с исполняемым файлом. Низкоуровневые криптографические процедуры, две функции вывода и несколько вызовов библиотек предполагаются по контракту, а не доказываются.

Проверка на наличие старых ошибок

Чтобы проверить, достаточно ли убедительны утверждения, команда повторно внесла две ошибки, которые исследователи ранее обнаружили в libsignal и которые с тех пор были исправлены. В обоих случаях они доказали, что теорема символической безопасности не выполняется в отношении бинарного файла с ошибками. Это полезная проверка: спецификация, которая по-прежнему “работает” на известном неисправном коде, была бы слишком слабой.

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

Что не говорится в результате

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

В статье отмечается, что варианты одного и того же протокола используются в WhatsApp, Meta Messenger и Google Messages. Эти приложения не являлись предметом доказательства. Доказательство, касающееся libsignal, не автоматически распространяется на каждый продукт, использующий аналогичный язык.

В исследовательской публикации цитируются слова технического директора Signal Эрена Крета о том, что тщательная проверка реализации протокола “дает нам еще большую уверенность в гарантиях конфиденциальности нашего кода”.

Доказательства и технические условия опубликованы в открытом репозитории.

Почему это важно

Большинство людей, отправляющих личные сообщения, никогда не видят библиотеку, которая их шифрует. Метод, позволяющий проверить скомпилированный код этой библиотеки за недели, а не за человеко-годы, представляет собой практическое изменение в способах аудита подобного программного обеспечения. Это не сертификат, подтверждающий отсутствие уязвимостей в Signal или любом другом чат-приложении. Это машинная проверка аргумента о заданных свойствах одной основной библиотеки, выполненная достаточно быстро, чтобы следующим шагом мог стать анализ другого критически важного кода.

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