Код шифрования Signal проверил ИИ DeepMind за четыре недели

Что такое формальная верификация кода?

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

Как это работает?

Система называется AlphaProof Code и объединяет несколько ИИ-моделей с экспертами-людьми. Исследователи DeepMind и модели перевели цели безопасности Signal в формальные спецификации, а эксперты проверили каждую. Агенты на базе Gemini Carbon написали доказательства: более шести миллионов строк на Lean, языке, который позволяет компьютеру автоматически проверять доказательства. Затем агенты провели аудит собственной работы и отметили примерно 1% кодовой базы, которому нужна повторная проверка человеком. Доказательства охватывают, например, защиту сообщений до и после временной компрометации устройства.

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

Всё мобильное приложение Signal проект не охватывал. Wired отмечает, что у DeepMind было преимущество благодаря прежней формальной верификации, которую проводил фонд Signal Foundation. Технический директор Signal Эрен Крет заявил, что прежняя работа «фокусировалась на меньших фрагментах кода», а подход DeepMind «позволяет значительно расширить охват».

Исследователи не хотят схемы, где ИИ пишет и цели, и доказательства. «Нам не нужен мир, где ИИ генерирует цели, ИИ генерирует доказательства и по сути сдаёт экзамены, которые сам же написал», сказал Сварат Чаудхури из DeepMind. Поэтому спецификации и отмеченные участки проверяли люди.

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