Исследователи Google DeepMind с помощью искусственного интеллекта доказали корректность ряда ключевых криптографических свойств протокола Signal. Для этого они применили агентный искусственный интеллект — систему, способную самостоятельно выполнять последовательность исследовательских задач, — и математическую формальную проверку. Разработка имеет значение как для оценки защиты мессенджера Signal, так и для дальнейшего применения ИИ в сфере безопасности программного обеспечения.
Проект провели примерно за четыре недели в рамках проверки концепции. Его результаты стали независимым подтверждением надежности шифрования, которое используется в Signal, Google Messages и WhatsApp. Кроме того, специалисты продемонстрировали возможности нового инструмента Google DeepMind под названием AlphaProof Code, предназначенного для формального доказательства свойств программ.
Формальная проверка позволяет математически установить, работает ли программа заданным образом и не содержит ли критических уязвимостей. Раньше подготовка описаний, перевод их в формулы и создание доказательств требовали от специалистов значительного времени. ИИ способен ускорить эту работу, однако проведенный анализ охватил только отдельные элементы протокола и не включал полную проверку мобильного приложения Signal.
Новых уязвимостей в изученных компонентах протокола исследователи не обнаружили. При проверке более ранних версий Signal, где присутствовали уже известные и исправленные проблемы, AlphaProof Code смог их выявить и показать невозможность формального доказательства корректности протокола. Разработчики также намерены предоставить спецификацию и созданное доказательство другим специалистам, занимающимся формальной проверкой.
По данным WIRED, дальнейшее развитие технологии зависит от того, сможет ли автоматизированная проверка работать с большими объемами программного кода и приемлемыми затратами. Исследование Signal проводилось бесплатно, а стоимость такой работы Google не раскрыла и не сообщила о планах выпуска коммерческого продукта. В Google DeepMind подчеркнули, что рассчитывают на совместную работу человека и ИИ: система может выполнять и перепроверять отдельные этапы, но ключевые решения и контроль должны оставаться за специалистами.