Google DeepMind с ИИ-агентами формально проверила код протокола Signal
Google DeepMind с помощью фреймворка AlphaProof Code математически доказала ключевые свойства безопасности реального кода протокола Signal, который защищает переписку в Signal и Google Messages. Процесс занял четыре недели, тогда как экспертным командам такая работа обычно требует лет.
Главное в цифрах
- Объём сгенерированного кода на Lean: более 6 миллионов строк
- Доля кодовой базы для ручной проверки: около 1%
- Время проверки: четыре недели
Исследователи DeepMind направляли ИИ-агентов, которые доказали ключевые свойства безопасности не только дизайна протокола, но и скомпилированного кода, работающего на устройствах. Спецификации формулировали люди: специалисты проверяли каждую из них, а сам перевод целей безопасности в формальные математические спецификации выполнялся совместно с набором моделей.
Доказательства строили агенты на базе Gemini Carbon. Они сгенерировали более шести миллионов строк на языке Lean, который проверяет корректность кода математически. Затем агенты проанализировали доказательства и отметили участки, которые нужно перепроверить человеку. Это около одного процента кодовой базы, остальное Lean проверяет автоматически.
Проверка без ошибок в коде
Чтобы убедиться, что система отличает корректный код от ошибочного, исследователи вернули в изолированную версию кода Signal две реальные уязвимости, которые уже были исправлены. В обоих случаях система выдала машинно проверяемое доказательство того, что версия с ошибкой небезопасна.
По словам компании, большинство проверок протоколов останавливается на уровне дизайна, а реальные уязвимости часто скрываются между спецификацией и реализацией. Именно поэтому доказательство для скомпилированного кода существенно сложнее.
Контекст
Технический директор Signal Эрен Крет назвал использование ИИ-агентов для перевода живого кода в теоремы Lean серьёзным прорывом. По его словам, проверка ядра протокола даёт большую уверенность в том, что код выполняет заявленные гарантии приватности, на фоне растущих ИИ-угроз.
DeepMind заявила, что откроет исходный код формальных артефактов проверки для сообщества.
