Google DeepMind с помощью AI-агентов формально верифицировала код протокола Signal

Проверяли две части библиотеки libsignal: постквантовое рукопожатие PQXDH, с которого начинается защищённый сеанс, и Triple Ratchet, механизм постоянной смены ключей. Доказаны четыре свойства: секретность рукопожатия, аутентификация, forward secrecy (старые сообщения остаются закрытыми при утечке ключа) и post-compromise security (защита восстанавливается после временного взлома устройства). Обычно верификация протоколов останавливается на уровне дизайна. Здесь агенты дошли до скомпилированного кода, который исполняется на устройствах. По словам DeepMind, реализацию столь широко используемого протокола раньше не верифицировал никто, с AI или без него.

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

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

Масштаб экономии виден на классических примерах, которые авторы приводят в статье. Формальная верификация микроядра seL4 заняла 20 человеко-лет, а разработка верифицированного компилятора CompCert шла шесть лет. Работа над Signal потребовала четырёх недель, пяти человек и, по выражению авторов, «немало токенов».

У результата есть границы. Доказательство исходит из идеальной криптографии и не гарантирует вычислительную стойкость самих байтов. Мобильное приложение Signal целиком агенты не проверяли. Работа приближает к решению задачи, которую в апреле поставил Beneficial AI Foundation: формально верифицировать на Lean и протокол, и приложение Signal. Исследователь DeepMind Сварат Чаудхури говорит, что до верификации всего мирового софта ещё далеко, и что главным стал вопрос, что именно доказывать.