Google математически доказал: переписку в WhatsApp и Signal прочитать нельзя

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

Раньше проверка безопасности кода сводилась к тестам: специалисты искали уязвимости и убеждались, что в проверенных случаях всё работает. Формальная верификация, которую применили исследователи, идёт дальше — она доказывает, что программа ведёт себя строго по заданным правилам при любых условиях. Обычно такой процесс занимает годы ручной работы, но здесь на помощь пришли ИИ-агенты AlphaProof Code на базе модели Gemini.

Команда из пяти человек разделила работу: люди определяли, что именно нужно доказать, а ИИ-агенты самостоятельно генерировали математические доказательства, которые затем автоматически проверялись системой Lean. За четыре недели было создано около 6,5 миллиона строк проверенных доказательств. Вручную специалистам пришлось просмотреть лишь около 1% кода. Чтобы убедиться, что метод действительно работает, исследователи специально вернули в код две уже исправленные ранее ошибки — и система их обнаружила.

Проверка охватила версию libsignal 0.105.4 и касалась обмена ключами и защиты переписки один на один, включая устойчивость к будущим квантовым компьютерам. Групповые чаты и синхронизация между устройствами пока вне зоны проверки, а весь код приложения целиком не проверялся. Подробности на сайте.

Что это значит для пользователя

Для обычного человека, который каждый день пишет в WhatsApp или Signal, главное — сама технология шифрования подтверждена математически, а не только на словах разработчиков. Это не отменяет других рисков: незаблокированный телефон, нешифрованные резервные копии в облаке или мошенник на другом конце переписки по-прежнему остаются слабыми местами. Но сама «математика» защиты теперь имеет строгое доказательство.

Исследователи отмечают, что метод пока очень затратен и не факт, что его легко масштабировать. Тем не менее работа открыта для сообщества, и её можно развивать дальше.

Технологии защиты переписки развиваются быстро, и разобраться в них проще, чем кажется. Если хотите быть в курсе подобных новостей и понимать, как устроены сервисы, которыми вы пользуетесь каждый день, узнайте больше.

📌 Чтобы не пропустить новые публикации, подписывайтесь там, где вам удобнее: Дзен или MAX.

💛 Если статья оказалась полезной, поддержите автора донатом.

Материал подготовлен на основе информации из открытых источников. Все права на исходные материалы принадлежат их авторам. Если вы являетесь правообладателем и возражаете против использования, свяжитесь с нами по адресу info@11st.press.