Google DeepMind проверила безопасность Signal с помощью AlphaProof Code

Что доказывать, решали люди

Сначала команда с помощью разных моделей превратила цели безопасности Signal в математическую спецификацию, проверенную людьми. Затем агенты Gemini Carbon сгенерировали код на Lean, доказывающий корректность libsignal. Объём составил 6,5 млн строк; после этого провели аудит и отметили фрагменты, требующие проверки человеком.

Результат теоретический: он предполагает идеальную криптографию и не гарантирует вычислительную секретность байтов. Тем не менее это значимое подтверждение корректности. Работа — шаг к задаче, которую в апреле поставил фонд Beneficial AI Foundation: формально верифицировать протокол и приложение Signal в Lean.

«Это система, изначально созданная для сотрудничества человека и ИИ», — сказал Сварат Чаудхури, научный сотрудник Google DeepMind и профессор Техасского университета в Остине. По его словам, масштабировать верификацию теперь можно, а главный вопрос — что именно верифицировать.

Стоимость и планы

Раньше формальная верификация требовала героических усилий: микроядро seL4 заняло 20 человеко-лет, компилятор CompCert C — шесть лет. Проект по Signal занял у команды из пяти человек четыре недели и, как отмечают авторы, «немало токенов».

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