Исследователи Google DeepMind 10 ноября представили доказательства ключевых свойств безопасности libsignal — библиотеки, реализующей протокол шифрования Signal. Работа охватывает установление личной переписки и смену ключей для её сообщений. Главное отличие от проверки схемы протокола на бумаге: доказательства связаны с машинным кодом библиотеки, собранным для архитектуры ARM64.

По отчёту команды, работа заняла четыре недели. Пять исследователей определяли требования вместе с ИИ и проверяли их формулировки; агенты Gemini Carbon в системе AlphaProof Code написали около 6,5 млн строк доказательств. Их логическую корректность проверяет Lean — отдельная программа, а не сама языковая модель. При этом около 26 тысяч строк спецификаций и описания работы процессора остаются частью основания, которому нужно доверять и которое должны проверять люди.

В заданных авторами моделях доказаны, в частности, защита прежних сообщений при краже текущего состояния сеанса и восстановление защиты новых сообщений после временной компрометации — при предусмотренных условиях обмена свежими ключами. Чтобы проверить чувствительность метода к ошибкам, исследователи вернули в отдельную сборку две ранее исправленные уязвимости: для обеих получили машинно проверяемые доказательства нарушения защиты. О новых уязвимостях Signal команда не сообщает.

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

Спецификации, доказательства и инструкции проверки открыты. Это позволяет другим исследователям проверить результат, но завершённое независимое воспроизведение пока не установлено. Как и в исследовании SemantEq, остаются две разные задачи: проверить логику доказательства и убедиться, что правильно сформулировано само требование. Здесь проверку удалось довести до исполняемых инструкций криптографической библиотеки; выбор требований и границ защиты всё ещё потребовал работы людей.