10 ноября Google DeepMind представила результаты формальной проверки ключевых свойств криптографического кода протокола Signal. ИИ-система AlphaProof Code выполнила основную часть работы за четыре недели — по оценке разработчика, у команды специалистов сопоставимая проверка могла бы занять годы.
Формальная верификация отличается от обычного тестирования: программа не просто запускается на наборе примеров. Исследователи формулируют требуемые свойства в виде математических утверждений, а затем доказывают, что конкретная реализация им соответствует. В проекте DeepMind проверялись, в частности, свойства, отвечающие за защиту сообщений до и после временной компрометации устройства.
Специалисты вместе с несколькими ИИ-моделями переводили цели безопасности Signal в формальные спецификации для проверки реализации протокола в коде, а не только его математической схемы; затем специалисты вручную проверяли каждую спецификацию. После этого агенты на базе Gemini Carbon строили доказательства и создали более 6 млн строк на Lean — языке, позволяющем машине проверять математические утверждения.
Читайте также
Lean автоматически проверял доказательства, а агенты выделяли участки доказательств и кода для дополнительной проверки людьми. По данным DeepMind, людям пришлось вернуться примерно к 1% исследованной кодовой базы.
Чтобы проверить, отличает ли система безопасный код от ошибочного, исследователи вернули две реальные, давно исправленные уязвимости в изолированную версию реализации. В обоих случаях AlphaProof Code сформировала машинно проверяемое доказательство того, что изменённый код не соответствует требованиям безопасности.
Новых уязвимостей в рассмотренных частях Signal команда не обнаружила. Однако это не означает, что математически проверено всё приложение или доказано отсутствие любых ошибок. WIRED отмечает, что проект охватил только часть реализации, а прежняя работа Signal Foundation над меньшими фрагментами кода дала исследователям фору.
AlphaProof Code пока остаётся исследовательской системой, а стоимость анализа не раскрыта. DeepMind открывает спецификации и доказательства проекта, чтобы другие команды могли проверить результаты и продолжить работу над методом.
