Команда Google DeepMind применила искусственный интеллект для проведения формальной верификации протокола шифрования Signal. Этот математический метод позволяет доказать надежность сквозного шифрования, которое также используют мессенджеры WhatsApp и Google Messages.
Формальная верификация использует математические доказательства для проверки безопасности алгоритмов во всех заданных условиях, в отличие от традиционного тестирования. В ходе исследования ИИ-агенты успешно выявили уязвимости в старых версиях протокола Signal, которые не прошли проверку.
Весь процесс анализа занял около четырех недель. Google не раскрывает точный объем вычислительных ресурсов, затраченных на работу. Компания отмечает, что масштабирование этой технологии на другие программные продукты остается долгосрочной задачей, требующей дальнейших исследований.
Исследователь DeepMind Сварат Чоудхури подчеркнул, что текущий результат является лишь этапом на пути к глобальному внедрению метода. В своей работе команда опиралась на предыдущие наработки в области формальной верификации, выполненные без участия ИИ.
