Исследователи Google DeepMind использовали ИИ-агентов для формальной проверки ключевых криптографических свойств Signal. Новый инструмент AlphaProof Code позволил математически подтвердить, что важные части реальной реализации протокола соответствуют заявленным требованиям безопасности. Работа заняла около четырёх недель, хотя подобные проекты при традиционном подходе могут требовать нескольких лет труда специалистов.
Речь идёт о формальной верификации — методе, при котором корректность определённых свойств программного обеспечения подтверждается математическим доказательством. Это принципиально отличается от обычного тестирования безопасности. При поиске уязвимостей специалисты пытаются обнаружить ошибки в различных сценариях, тогда как формальная проверка показывает, что в рамках заданной математической модели определённые свойства действительно выполняются.
Для проекта Google DeepMind разработала AlphaProof Code — многоагентную систему, объединяющую работу специалистов и искусственного интеллекта. Люди определяли, какие именно свойства необходимо доказать, проверяли формальные спецификации и контролировали наиболее важные этапы. После этого ИИ-агенты выполняли основную часть построения математических доказательств.
При проверке использовалась модель Gemini 4 Carbon. ИИ-агенты создали более 6 млн строк доказательств на языке Lean. Этот язык применяется для формального описания математических утверждений и автоматической проверки того, действительно ли последовательность рассуждений приводит к требуемому результату.
Важная особенность исследования заключается в том, что специалисты проверяли не только абстрактное описание криптографического протокола. AlphaProof Code анализировала код библиотеки libsignal и доказывала свойства реализации вплоть до машинного кода для архитектуры AArch64. Такой уровень проверки позволяет уменьшить разрыв между теоретически безопасным криптографическим алгоритмом и программой, которая фактически выполняется на устройстве пользователя.
Исследование охватило важные элементы современной криптографии Signal, включая механизм установления соединения PQXDH и протокол Triple Ratchet. В частности, проверялись свойства аутентификации, секретности обмена ключами, прямой секретности и способности системы восстанавливать защищённость последующих сообщений после временной компрометации устройства.
Подобные свойства особенно важны для защищённых мессенджеров. Например, прямая секретность означает, что получение злоумышленником текущих ключей не должно автоматически позволять расшифровать всю предыдущую переписку. Механизмы восстановления после компрометации, в свою очередь, предназначены для того, чтобы безопасность будущих сообщений могла восстановиться после обновления ключевого материала.
В проверенных компонентах исследователи не обнаружили новых уязвимостей. Чтобы убедиться, что AlphaProof Code действительно способна отличать безопасную реализацию от ошибочной, специалисты отдельно протестировали систему на версиях кода, в которые вернули две реальные уязвимости, исправленные ранее.
В обоих случаях система смогла математически показать, что изменённая реализация больше не удовлетворяет необходимым требованиям безопасности. Это стало дополнительной проверкой того, что инструмент не просто способен построить доказательство для корректной программы, но и распознаёт ситуации, когда такое доказательство невозможно из-за ошибки в коде.
Разработчики Signal ранее уже занимались формальной верификацией отдельных компонентов своей криптографической системы. Эта предыдущая работа помогла Google DeepMind быстрее провести новый эксперимент. Однако новый подход позволил существенно увеличить масштаб проверки и приблизиться непосредственно к коду, работающему на устройствах.
Технический директор Signal Эрен Крет отметил, что предыдущие проекты формальной проверки обычно охватывали более ограниченные части системы. Использование ИИ-агентов для преобразования реального программного кода в проверяемые математические утверждения позволяет значительно расширить объём анализа.
При этом результаты исследования не означают, что всё приложение Signal теперь математически доказано как полностью безопасное. Специалисты не проверяли целиком мобильные приложения, пользовательский интерфейс, серверную инфраструктуру и все остальные программные компоненты. Формальная верификация распространяется только на конкретные свойства и части криптографической реализации, которые были включены в исследование.
Поэтому результат нельзя интерпретировать как гарантию абсолютного отсутствия любых будущих уязвимостей в Signal. Ошибка теоретически может находиться в компоненте, который не проверялся, в операционной системе устройства, в сторонней библиотеке или в другой части программной инфраструктуры.
Тем не менее значение работы выходит далеко за пределы самого Signal. Его криптографические технологии используются не только одноимённым мессенджером. На принципах Signal Protocol построена защита сообщений и в других массовых сервисах, включая Google Messages и WhatsApp*.
Главным достижением Google DeepMind стало не столько подтверждение уже хорошо изученной криптографии Signal, сколько демонстрация возможностей ИИ в автоматизации чрезвычайно трудоёмкой формальной проверки программного обеспечения.
Раньше подобные проекты могли занимать годы и требовать команды высококвалифицированных специалистов. Например, формальная проверка некоторых известных систем в прошлом оценивалась в десятки человеко-лет работы. Это делало технологию слишком дорогой для большинства обычных программных продуктов.
ИИ-агенты потенциально способны существенно сократить этот объём ручной работы. В проекте Signal они самостоятельно создавали доказательства и одновременно анализировали собственные результаты, выделяя участки, которые требовали дополнительного внимания специалистов.
По данным Google DeepMind, после автоматической проверки людям потребовалось особенно внимательно изучить примерно 1% полученного материала. Остальные доказательства автоматически проверялись ядром Lean, которое не принимает математически некорректную последовательность шагов.
При этом роль человека по-прежнему остаётся принципиально важной. Исследователи специально не хотели создавать систему, в которой ИИ самостоятельно формулирует требования безопасности, затем сам их доказывает и после этого объявляет собственный результат правильным.
Специалисты участвовали в определении того, что именно должна гарантировать проверяемая программа, и утверждали исходные математические спецификации. Такой подход должен уменьшить риск ситуации, когда доказательство формально безошибочно, но относится не к тому свойству, которое действительно важно для безопасности реальной системы.
Google DeepMind собирается открыть созданные в рамках проекта формальные спецификации и доказательства. Благодаря этому независимые исследователи смогут изучить методику, проверить полученные результаты и использовать материалы для собственных проектов.
В дальнейшем подобный подход может применяться далеко не только к мессенджерам. Формальная верификация особенно ценна для программного обеспечения, ошибка в котором способна привести к серьёзным последствиям: банковских систем, медицинского оборудования, энергетической инфраструктуры, транспорта, криптографических библиотек и других критически важных технологий.
Однако до массового применения AlphaProof Code ещё далеко. Исследователям предстоит выяснить, насколько хорошо метод масштабируется на очень крупные программные проекты, сколько вычислительных ресурсов для этого потребуется и насколько экономически оправданным окажется такой подход.
Google не раскрыла стоимость четырёхнедельной проверки Signal и пока не объявляла о планах превратить AlphaProof Code в коммерческий сервис. Поэтому неизвестно, насколько доступной подобная технология окажется для обычных разработчиков.
Тем не менее эксперимент показывает потенциально важное направление применения искусственного интеллекта. Вместо того чтобы только писать новый код, ИИ может использоваться для математической проверки уже существующего программного обеспечения и подтверждения того, что критически важные механизмы действительно выполняют заявленные свойства.
Если такой подход удастся масштабировать, формальная верификация сможет стать значительно более распространённым инструментом разработки. В этом случае ИИ будет применяться не только для ускорения создания программ, но и для более строгой проверки их безопасности перед использованием в реальных системах.
*Meta признана экстремистской организацией и запрещена в России.