ИИ-агенты Google DeepMind математически проверили безопасность шифрования Signal на уровне машинного кода
Исследователи Google DeepMind разработали систему искусственного интеллекта AlphaProof Code, которая позволила математически подтвердить ключевые свойства безопасности программной реализации криптографического протокола Signal. В отличие от традиционных исследований, ограничивающихся теоретическим описанием алгоритмов, новая система проверяла непосредственно скомпилированный машинный код. По заявлению разработчиков, это первая формальная проверка такого масштаба для действующей реализации широко используемого криптографического протокола.
Для эксперимента специалисты использовали библиотеку libsignal версии 0.105.4 и компонент SPQR версии 1.6.0, предназначенные для защищённого обмена сообщениями. Исходный код на Rust скомпилировали стандартными средствами для архитектуры AArch64, после чего проверили механизмы установления защищённого соединения PQXDH и обновления ключей Triple Ratchet. Исследователи доказали ряд свойств, включая аутентификацию, защиту ранее переданных сообщений при раскрытии текущих ключей и восстановление конфиденциальности после определённых сценариев компрометации.
Главную работу выполняли несколько групп ИИ-агентов на основе Gemini. Они преобразовывали требования безопасности в математические утверждения и составляли доказательства на языке Lean, которые затем автоматически проверялись специальным программным средством. В общей сложности система подготовила около 6,5 миллиона строк формально проверенных доказательств, опирающихся примерно на 26 тысяч строк доверенных спецификаций и описания машинных инструкций.
Весь исследовательский проект занял четыре недели. Для дополнительной проверки специалисты вернули в отдельную экспериментальную версию библиотеки две реальные ошибки, ранее устранённые разработчиками Signal. В обоих случаях система смогла математически установить, что изменённая программа нарушает соответствующие требования безопасности.
Существенное отличие AlphaProof Code заключается в разделении обязанностей человека и искусственного интеллекта. Исследователи определяли, какие свойства необходимо доказать, проверяли математические спецификации и контролировали допущения, тогда как агенты самостоятельно строили доказательства. Их правильность проверяло ядро Lean, поэтому ошибочные рассуждения нейросети не могли быть приняты только на основании её собственного заключения.
При этом результаты не означают, что весь мессенджер Signal признан абсолютно безопасным. Проверка охватывала определённую сборку кода и конкретные свойства протокола для переписки между двумя участниками, но не все режимы приложения, групповые чаты и возможные атаки. Некоторые криптографические свойства и компоненты системы также рассматривались на основе явно заданных предположений. Авторы опубликовали технический отчёт и материалы доказательств, позволяющие другим специалистам изучить результаты; независимая проверка полного набора доказательств пока не подтверждена. Работа показывает возможность применения ИИ для математического анализа сложного промышленного программного обеспечения, хотя эффективность подхода на других системах ещё предстоит установить.