AlphaProof Code от Google DeepMind формально верифицировал криптографический протокол Signal

Google DeepMind заявляет, что достигла вехи в области безопасности программного обеспечения, давно считавшейся грандиозной задачей: её исследователи направляли ИИ-агентов к математическому доказательству ключевых свойств безопасности реального кода, лежащего в основе протокола Signal, — технологии, защищающей миллиарды приватных разговоров в таких приложениях, как Signal и Google Messages, за счёт сквозного шифрования сообщений, когда прочитать их могут только отправитель и адресат. Объявление опубликовано в блоге Google DeepMind авторами Pushmeet Kohli и Swarat Chaudhuri.

Результат был достигнут с помощью AlphaProof Code — нового агентного фреймворка для формальной верификации на беспрецедентной глубине, сочетающего экспертизу людей с ИИ-агентами. Формальная верификация — математическое доказательство того, что код работает корректно и без изъянов, — является высшим стандартом гарантий безопасности, но она сложна и зачастую трудоёмка. Традиционное тестирование лишь выбирает примеры поведения программы; формальное доказательство исключает изъяны во всех возможных вариантах исполнения — уровень гарантий настолько затратный в получении, что он редко доходил до широко развёрнутого программного обеспечения.

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

Как Google DeepMind верифицировала Signal

AlphaProof Code — это много-LLM агентный фреймворк, который распределяет работу по формальной верификации так, как это делала бы исследовательская команда: эксперты-люди вместе с ИИ решают, что доказывать, а группа ИИ-агентов выполняет доказательства.

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

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

Доказательство безопасности вплоть до исполняемого кода

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

Агенты Google DeepMind пошли дальше, доказав, что скомпилированный код удовлетворяет ключевым свойствам безопасности — таким как защита сообщений до и после временной компрометации устройства, — гарантии, которые криптографы называют прямой секретностью (forward secrecy) и защитой после компрометации (post-compromise security), — вплоть до точного кода, исполняемого на устройствах. Реальные уязвимости часто скрываются в разрыве между дизайном и реализацией, и преодоление этого разрыва делает подобные доказательства значительно более сложными.

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

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

В AlphaProof Code ИИ-агенты помогают пользователям написать спецификацию, а затем автономно доказывают, что реализация ей соответствует. Каждое доказательство проверяется Lean для контроля работы агентов.

Реакция Signal

"Если прежняя формальная верификация охватывала лишь меньшие части кода, подход Google DeepMind позволяет существенно расширить её масштабы", — сказал Эрен Крет (Ehren Kret), технический директор Signal. "Использование ИИ-агентов для перевода живого кода в валидные теоремы Lean — крупный прорыв. По мере роста угроз безопасности, driven ИИ, строгая верификация реализации протокола Signal даёт нам ещё большую уверенность в гарантиях приватности нашего кода."

Будущее безопасности

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

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

Google DeepMind открывает код артефактов формальной верификации для использования сообществом; они размещены на google-deepmind.github.io/code-verification. Полный технический документ доступен в формате PDF. Для сообщества исследователей безопасности эта публикация даёт возможность напрямую изучить проверенные машиной доказательства и методологию — а то, насколько широко верификация на такой глубине распространится за пределы Signal, на медицинские, промышленные и инфраструктурные системы, названные компанией, станет следующим ключевым событием, за которым стоит следить.

Благодарности

Исследование было выполнено Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton и Pushmeet Kohli.

Команда поблагодарила Eric Wieser за помощь с открытием кода, Owen Jones за поддержку в управлении программой, а также Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko и George Tsoukalas за полезные обсуждения. Исследователи также поблагодарили Rolfe Schmidt, Michael Rosenberg и Ehren Kret из Signal за отзывы о методологии, а также Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis и Sundar Pichai за поддержку проекта.