ИИ доказал защиту Signal, но не всего мессенджера
Математическая проверка подтвердила надёжность ключевых механизмов шифрования, но не исключила другие уязвимости.
В опубликованной 10 ноября работе Google DeepMind описан необычный способ проверки программ: не искать отдельные уязвимости тестами, а доказать, что код выполняет заранее сформулированные требования безопасности. Для этого специалисты разработали AlphaProof Code — систему, в которой несколько ИИ-агентов работают над формальными доказательствами, а человек определяет, что именно нужно доказать.
Объектом стала libsignal — библиотека, реализующая криптографический протокол Signal. Исследователи изучали не только описание алгоритмов, но и собранный машинный код для архитектуры AArch64. Это принципиальная разница: даже надёжный на бумаге алгоритм можно неправильно реализовать в программе, которая обрабатывает сообщения, ключи и состояние сеанса.
В проверку вошли механизм установления защищённого соединения PQXDH и Triple Ratchet, обновляющий ключи по мере обмена сообщениями. Доказательства касались конфиденциальности и подлинности сообщений, защиты ранее отправленного при последующей утечке ключей, а также восстановления некоторых гарантий после временной компрометации ключевого материала. Но эта последняя возможность предполагает, что злоумышленник больше не контролирует устройство и происходит необходимое обновление ключей.
Работа заняла четыре недели. По данным авторов, агенты создали около 6,5 миллиона строк доказательств на языке Lean. Сам Lean автоматически проверял их логическую корректность. При этом примерно 26 тысяч строк доверенных спецификаций и описания машинной архитектуры оставались основой, правильность которой требовала человеческой экспертизы. ИИ не мог произвольно объявить собственный ответ доказанным.
Авторы проверили систему и обратным способом: в отдельную копию кода вернули две ранее устранённые ошибки. В обоих случаях инструмент смог математически показать нарушение проверяемого требования безопасности. Исходные материалы доказательств опубликованы для дальнейшего анализа специалистами.
Однако слово «доказано» здесь имеет строгие границы. Исследователи рассмотрели конкретные компоненты и модели угроз, а не весь Signal для Android, iOS и компьютеров. Групповые чаты, работа нескольких связанных устройств и утечки через побочные каналы не получили такого же подтверждения. Часть постквантовых гарантий тоже осталась за пределами доказанного: в вычислительной модели не рассматривались квантовые атакующие.
Это особенно важно на фоне октябрьского сообщения об ошибке завершения звонка в Signal. Уязвимость CVE-2026-113380 в библиотеке RingRTC позволяла уже подключённому к разговору собеседнику перегружать очередь событий. Из-за этого попытка закончить вызов могла не остановить передачу звука, а при определённых условиях и видео. Ошибку исправили в сентябре; подтверждённых сообщений о её использовании в реальных атаках не было.
Никакого противоречия между двумя историями нет. Проверенная DeepMind криптография отвечает за защиту содержания сообщений и ключей. Ошибка RingRTC касалась управления вызовом: программа могла продолжить передавать данные законному участнику разговора вопреки намерению пользователя. Даже математически безупречное шифрование не определяет, когда нужно выключить микрофон.
Для пользователя практический вывод остаётся простым: обновлять Signal, проверять подключённые устройства и не считать защищённую переписку гарантией безопасности самого телефона. Новая работа усиливает доверие к проверенным частям протокола, но не заменяет поиск ошибок в остальных компонентах приложения.
Новизна AlphaProof Code не в обещании мессенджера без единой уязвимости. Исследователи показали, что математическую проверку сложного промышленного кода можно приблизить к темпу его разработки. Если метод удастся применять к новым версиям программ, доказательства станут не разовым сертификатом, а частью регулярной проверки обновлений.
Изображение: редакция ИЗНАНКИ.
