Протокол Signal защищает переписку в приложении Signal, а также в WhatsApp, Messenger и Google Messages. Исследователи DeepMind проверили libsignal — библиотеку шифрования Signal с открытым исходным кодом — вплоть до машинного кода, который выполняется на устройстве. В блоге DeepMind лаборатория назвала это первым подобным достижением. По её словам, никто прежде не проводил формальную верификацию кода столь широко используемого протокола — «каким-либо методом, с ИИ или без него». В технической статье описаны метод и его ограничения.
«По мере роста угроз безопасности, связанных с ИИ, строгая верификация ядра протокола Signal с помощью автоматического доказательства теорем даёт нам ещё большую уверенность в том, что наш код выполняет свои гарантии конфиденциальности», — заявил технический директор Signal Эрен Крет в комментарии, опубликованном DeepMind.
Как агенты справились с задачей
Формальная верификация с помощью математики доказывает, что программа делает то, что должна. Вместо того чтобы выискивать ошибки по одной, она исключает целые их классы. Долгое время этот процесс был медленным и дорогим: в статье отмечается, что верификация микроядра seL4 заняла 20 человеко-лет.
AlphaProof Code разделяет работу. Люди выбирали, что именно доказывать. ИИ-агенты помогали переводить цели безопасности Signal в формальные спецификации, а эксперты-люди проверяли каждую из них. Затем команды из 40–80 агентов на базе Gemini 4 Carbon писали доказательства. Они использовали Lean — язык для математики с машинной проверкой.
За четыре недели агенты создали около 6,5 млн строк доказательств для команды из пяти исследователей. Согласно статье, никто из авторов не писал код доказательств. Спецификации составляли и проверяли агенты на базе Gemini 4 Carbon и Claude Opus 5.5 от Anthropic.
Доказательства охватывают постквантовое рукопожатие Signal и его Triple Ratchet, который даёт каждому сообщению новый ключ. Они подтверждают прямую секретность, благодаря которой старые сообщения остаются защищёнными, даже если кто-то позже похитит ключи с телефона. Также доказаны аутентификация и безопасность после компрометации — способность протокола восстанавливаться после взлома.
Чтобы проверить метод, команда вернула в код две старые ошибки libsignal, которые Signal уже исправил. В обоих случаях система доказала, что код с ошибками небезопасен. Новых уязвимостей в проверенных частях она не обнаружила, сообщила Лили Хэй Ньюман в Wired.
Чего это не доказывает
Гарантии уже, чем утверждение «Signal безопасен». Статья охватывает личные чаты в собственной сборке библиотеки, сделанной исследователями, а не приложения Signal. Групповые переписки исследователи оставили на будущее, а генерацию ключей не верифицировали. Кроме того, доказательства исходят из того, что низкоуровневые криптографические процедуры работают в соответствии со спецификацией.
Как говорится в статье, ни одно из доказательств не подтверждает постквантовое «самовосстановление», которое призван добавить новейший уровень храповика Signal. Открытым остаётся и вопрос стоимости. Как сообщил Wired, Google отказалась раскрыть, во сколько обошёлся проект и планирует ли компания коммерческий продукт для верификации.
«Мы очень воодушевлены этим результатом, но предстоит пройти долгий путь, прежде чем мы сможем масштабировать это на всё программное обеспечение в мире, и мы хотим это сделать», — сказал Wired научный сотрудник DeepMind Сварат Чаудхури.
Чаудхури сообщил The Register, что теперь сложнее всего решить, что именно проверять, а не саму проверку.
«Мы искренне верим, что следующим рубежом станет не доказательство, а спецификация», — сказал Чаудхури The Register.
Эта работа — шаг к Signal Shot. Этот вызов в апреле объявили Beneficial AI Foundation, Signal и Lean FRO: верифицировать протокол и приложение Signal в Lean. DeepMind публикует свои спецификации и доказательства на GitHub, чтобы другие могли их проверить. На этой неделе Google открыла доступ к Gemini 4 Carbon для платных разработчиков.
Опубликовано 12 ноября 2026 - 04:07 Наверх
