Исследователи Google DeepMind использовали агентный ИИ для математического доказательства нескольких ключевых криптографических гарантий протокола Signal. Эта работа, выполненная в виде пилотного проекта за четыре недели, основана на новой платформе ИИ под названием AlphaProof Code.
Протокол Signal обеспечивает шифрование коммуникаций не только в одноимённом приложении, но также, по данным источника, в Google Messages и WhatsApp. Для статьи эта демонстрация представляет собой новую независимую валидацию данной криптографии, защищающей огромный объём сообщений по всему миру. Она также иллюстрирует возможности Google DeepMind в области формальной верификации.
Формальная верификация — это использование математики для проверки того, что программное обеспечение работает как задумано, то есть не содержит критических уязвимостей. Её сторонники давно считают её Святым Граалем программной безопасности. Однако её широкомасштабное применение остаётся под вопросом, как и её эффективность при работе с большими объёмами кода.
Целевой анализ
До эпохи ИИ требовалось значительное время, чтобы описать характеристики ПО, преобразовать эти описания в формулы, а затем разработать доказательство. По словам источника, агентный ИИ может существенно сократить продолжительность последнего этапа. Однако масштаб анализа остаётся ограниченным: он, например, не провёл формальную верификацию всего мобильного приложения Signal.
В исследованных частях протокола исследователи не обнаружили новых уязвимостей. С другой стороны, когда они применили AlphaProof Code к старым версиям Signal, содержащим давно известные и исправленные уязвимости, инструмент правильно их идентифицировал и показал, что протокол не может быть формально верифицирован в этих версиях. Исследователи публикуют спецификацию и доказательство, разработанные для анализа протокола Signal, чтобы облегчить дальнейшие работы по формальной верификации.
Скорость выполнения проекта частично обусловлена предыдущими работами Signal Foundation в этой области, как отмечают исследователи DeepMind. «В то время как предыдущая формальная верификация охватывала более ограниченные части кода, подход Google DeepMind позволяет значительно расширить масштаб», — заявил технический директор Signal Эрен Крет в пресс-релизе. «В условиях роста угроз безопасности, связанных с ИИ, тщательная проверка реализации протокола Signal даёт нам ещё большую уверенность в гарантиях конфиденциальности нашего кода».
Вопрос стоимости и масштабирования
Для критически важных сервисов, используемых в высокорисковых контекстах, возможность формально верифицировать каждую кодовую базу и все цепочки поставок ПО стала бы, по словам Пушмита Коли, директора по науке Google Cloud и вице-президента по исследованиям в DeepMind, серьёзным прорывом. «Если теперь можно проверить корректность этих реализаций, можно спать спокойно. Представьте себе банки и все другие компании, которые полагаются на гарантии и беспокоятся об ошибках, теперь способные заявить: « Я могу доказать эти свойства »», — говорит он.
Остаётся открытым для всей технологической отрасли вопрос о способности автоматизированной формальной верификации с помощью ИИ действительно масштабироваться при разумной стоимости. DeepMind провёл анализ Signal бесплатно, в рамках исследовательского проекта, и Google не пожелал раскрывать его стоимость. Компания также не уточнила, планирует ли она коммерциализировать продукт или услугу формальной верификации.
Исследователи считают, что некоторые из их ключевых достижений связаны с «процессом сотрудничества человека и ИИ», как выразился Сварат Чаудхури, научный сотрудник DeepMind. Этот процесс позволяет агентам вносить вклад и корректировать себя практически на каждом этапе, при этом запрашивая человеческое мнение и валидацию в ключевые моменты. «Мы не хотим этого мира атмосферы, где ИИ ставит цели, ИИ создаёт доказательства, и мы проходим тесты, которые он сам написал. Существует золотая середина».
