Что именно проверили

Google DeepMind сообщила, что её исследователи с помощью агентной системы AlphaProof Code математически доказали ключевые свойства безопасности кода, лежащего в основе протокола Signal. Компания называет эту работу первым случаем столь глубокой формальной проверки широко используемого криптографического протокола с помощью ИИ, а также первым случаем формальной проверки реализации такого протокола любым методом.

В отличие от анализа только проектной схемы, проверка затронула скомпилированный код вплоть до того, который работает на устройствах. DeepMind говорит, что исследователи задали свойства, которые нужно доказать, а агенты проверили, соответствует ли им реализация. Среди примеров — защита сообщений до и после временной компрометации устройства.

Как работала AlphaProof Code

AlphaProof Code — система из нескольких языковых моделей и ИИ-агентов. Исследователи вместе с моделями переводили цели безопасности Signal в математические спецификации, а эксперты проверяли каждую из них. Затем агенты на базе Gemini Carbon создали более шести миллионов строк кода на Lean — языке, предназначенном для математической проверки доказательств.

Система также проверяла доказательства и отмечала места, требующие дополнительного внимания человека. По данным DeepMind, таких участков было около 1% кодовой базы; остальную часть проверял Lean. Весь процесс занял четыре недели — компания сравнивает этот срок с годами работы, которые исторически могли требоваться экспертным командам.

Проверка на ошибках и открытые материалы

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

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