Новый ИИ-инструмент Google DeepMind доказал безопасность протокола Signal

Что проверили исследователи

Формальная проверка использует математику, чтобы установить, работает ли программа так, как задумано, и нет ли в ней критических уязвимостей. Google DeepMind применила для этого ИИ-агентов и AlphaProof Code — новый фреймворк компании.

Проект стал проверкой концепции и важен в двух отношениях. Независимый анализ дополнительно проверил криптографию, которая защищает огромный объём переписки в Signal, Google Messages и WhatsApp. Одновременно он показал, как Google DeepMind использует AlphaProof Code для формальной проверки.

Нынешний интерес к формальной проверке с помощью ИИ не снимает вопросов о том, насколько практичным окажется этот подход и сможет ли он надёжно проверять большие объёмы кода. Сторонники формальной проверки давно считают её одной из главных целей безопасности программного обеспечения: математика позволяет проверить, соответствует ли работа программы заданным требованиям.

До появления ИИ специалистам приходилось вручную описывать свойства программы, которые нужно доказать, переводить описания в формулы и затем строить доказательство. ИИ-агенты могут заметно ускорить последнюю часть этой работы.

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

Проверка старых версий

В изученных частях актуального протокола команда не обнаружила новых уязвимостей. Но исследователи также проверили старые версии Signal, в которых были известные и давно устранённые уязвимости. AlphaProof Code правильно указал на них и показал, что протокол в этих версиях нельзя формально подтвердить.

Спецификацию и доказательство, созданные для анализа Signal, команда публикует, чтобы ими могли воспользоваться другие исследователи формальной проверки.

Быстро провести проект помогли и предыдущие работы Signal Foundation: они уже формально проверяли отдельные части кода. Технический директор Signal Эрен Крет отметил, что подход Google DeepMind позволяет существенно расширить эту проверку. По его словам, строгая проверка реализации протокола укрепляет доверие к гарантиям конфиденциальности Signal на фоне роста угроз безопасности, связанных с ИИ.

Масштаб и цена проверки

Для критически важных сервисов было бы полезно формально проверять каждую кодовую базу и всю цепочку поставки программного обеспечения. Главный научный сотрудник Google Cloud и вице-президент по исследованиям DeepMind Пушмит Коли считает, что такая проверка позволила бы компаниям, включая банки, доказывать корректность свойств своих программ и увереннее полагаться на их работу.

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

Роль человека

Исследователи называют одним из ключевых результатов процесса совместную работу человека и ИИ. Агенты могут участвовать почти на каждом этапе и исправлять собственные ошибки, но в важных точках процесса сохраняются человеческая оценка и проверка.

Чаудхури подчеркнул, что DeepMind не стремится к ситуации, в которой ИИ сам задаёт цели, генерирует доказательства и проверяет себя по тестам, которые тоже создал сам. По его словам, возможен промежуточный вариант с участием людей.

По оценке Dataist, работа показывает, что ИИ-агенты могут ускорить формальную проверку конкретных частей протокола и обнаруживать заранее известные ошибки. Но проверка Signal не охватила всё приложение, а её стоимость и возможность коммерческого применения пока неясны. Это оставляет открытым вопрос, насколько далеко такой подход можно масштабировать за пределы исследовательского проекта.