За четыре недели Google DeepMind математически подтвердила ключевые гарантии шифрования Signal на уровне машинного кода. Система AlphaProof Code проверила реализацию протокола, а не только его теоретическую схему. Разновидности Signal Protocol защищают переписку в Signal, WhatsApp, Google Messages и Messenger, но доказательства не распространяются автоматически на все приложения.
О результатах 10 ноября сообщила Google DeepMind. Пятеро специалистов управляли ИИ-агентами, создавшими около 6,5 млн строк математических доказательств на языке Lean. Проверяющая система Lean оценивала выводы независимо от нейросетей. Работа охватила около 560 КБ кода, соответствующих 140 тысячам машинных инструкций архитектуры AArch64.
Проверяли libsignal версии 0.105.4 в специально собранной программе libsignal-cli. Доказательства охватывают установление защищённого соединения PQXDH и механизм Triple Ratchet, который регулярно обновляет ключи. Авторы подтвердили конфиденциальность и подлинность сообщений, защиту старой переписки после кражи ключей и восстановление секретности при определённых условиях.
Люди формулировали требования к защите и утверждали математические спецификации, а ИИ строил доказательства. Причём в подготовке требований участвовали Gemini 4 Carbon и Claude Opus 5.5, тогда как сами доказательства создавали агенты Gemini. Разработчики раскрыли подробности проверки и выложили результаты в открытый доступ.
Для испытания AlphaProof Code авторы вернули в тестовую сборку две ранее исправленные ошибки. Первая приводила к сохранению небезопасного состояния сеанса, вторая нарушала проверку открытого ключа при повторном соединении. В обоих случаях ИИ доказал нарушение гарантий. Кроме того, команда нашла 15 пробелов и ошибок в прежнем научном анализе Double Ratchet, но не в коде действующего Signal.
Проверка не охватывала групповые чаты, несколько устройств, побочные каналы утечки и весь код мобильного Signal. Часть доказательств учитывает квантового противника, но полного подтверждения постквантовой безопасности нет. Результат относится к конкретной сборке AArch64 и основан на допущениях о криптографических примитивах, поэтому не гарантирует безопасность всех платформ и версий.
Масштаб ограничен и в других мессенджерах. Независимая научная работа 2026 года выявила различия между оригинальной libsignal и реализацией WhatsApp Web. А защита от подмены собеседника требует отдельного механизма: в августе Signal добавил автоматическую проверку ключей. AlphaProof Code не оценивала работу такой функции в готовом приложении.
Сильное шифрование не исключает кражу переписки другими способами. Например, уже описана привязка постороннего устройства к защищённому чату без взлома криптографии. Google DeepMind не раскрыла стоимость эксперимента и не объявила коммерческий запуск AlphaProof Code. Возможность столь же быстро проверять другие большие программы пока остаётся открытым вопросом.