ИИ помог проверить шифрование Signal на уровне машинного кода
Google DeepMind проверила ключевые свойства библиотеки Signal на уровне машинных инструкций. ИИ-агенты подготовили около 6,5 млн строк доказательств, а Lean проверила их.
10 ноября Google DeepMind представила AlphaProof Code, систему для математической проверки программ с помощью ИИ. Первой большой задачей стала libsignal, библиотека, которая реализует протокол шифрования Signal. Исследователи проверили ключевые свойства конкретной сборки на уровне машинных инструкций. ИИ-агенты подготовили около 6,5 млн строк доказательств, а система Lean проверила их.
Зачем проверять библиотеку, если протокол уже изучали
Протокол описывает, как два собеседника договариваются о ключах и меняют их по ходу разговора. Библиотека превращает эту схему в работающую программу. Ей приходится учитывать детали, которых может не быть в модели протокола. Например, сообщения иногда приходят не по порядку. Чтобы получатель всё равно мог их прочитать, libsignal хранит ключи для опоздавших сообщений и состояние предыдущих сеансов. Ошибка в том, когда программа сохраняет или удаляет такой ключ, может повлиять на безопасность переписки.
Исследователи взяли для проверки исполняемый файл libsignal-cli, собранный для архитектуры AArch64. Это тестовая сборка с интерфейсом командной строки. Работа с машинным кодом позволила связать заявленные свойства с инструкциями, которые исполняет процессор. Например, авторы проверили, при каких условиях перехваченные сообщения остаются закрытыми и может ли протокол восстановить защиту переписки после утечки части ключей.
В эксперименте запускали отдельные процессы с заданными условиями работы. Результат относится к этой сборке библиотеки. Приложения Signal для телефонов и компьютеров целиком в эксперимент не входили.
ИИ писал доказательства, а Lean проверяла каждый шаг
Сначала исследователям нужно было точно описать, что считать защищённой перепиской и какие возможности есть у атакующего. Например, модель может допускать, что в определённый момент тот получает ключи одного из участников. Тогда исследователи отдельно задают вопрос о сообщениях, отправленных до утечки, и о сообщениях после следующей смены ключей. ИИ помогал записывать эти условия на языке Lean, а специалисты проверяли каждую спецификацию перед тем, как передать её агентам.
Затем агенты составляли доказательства, связывая поведение программы с утверждённой спецификацией. Ядро Lean принимало доказательство только после машинной проверки. Поэтому даже убедительное объяснение от модели само по себе ничего не решало. По данным авторов, пять участников команды работали над доказательствами четыре недели. Около 6,5 млн строк проверяемого кода опирались примерно на 26 тыс. строк спецификаций и описания работы машинных инструкций.
Чтобы проверить, замечает ли метод реальные ошибки, авторы вернули в библиотеку две ранее исправленные уязвимости. В одном случае запоздавшее сообщение могло заставить программу сохранить состояние нового сеанса вместе с копией секретного ключа. Для изменённых сборок исследователи смогли показать в Lean, какие свойства безопасности перестают выполняться. Так они проверили, что спецификация достаточно точно описывает хотя бы эти известные сбои.
Почему проверку Signal пришлось расширять
Signal представил PQXDH в 2023 году, чтобы защитить обмен ключами при установлении сеанса с учётом угрозы будущих квантовых компьютеров. В октябре 2025-го команда добавила SPQR, который усиливает защиту при смене ключей уже во время разговора. Вместе с прежним механизмом он образует Triple Ratchet. Из-за таких изменений доказательства для прежних версий протокола покрывали лишь часть того, что делает актуальная библиотека.
В апреле 2026 года Signal, Lean FRO и Beneficial AI Foundation запустили проект Signal Shot, чтобы формально проверить протокол и приложение. Ноябрьская работа закрывает часть этой задачи на уровне скомпилированной библиотеки. DeepMind опубликовала спецификации и доказательства, чтобы другие исследователи могли проверить, при каких условиях получены результаты.