ИИ-агенты помогли DeepMind проверить часть кода Signal на уровне машинного кода
В исследовании AlphaProof Code команда описала доказательства для библиотеки libsignal; спецификации свойств безопасности предварительно проверяли специалисты.
Google DeepMind представила AlphaProof Code — систему, в которой ИИ-агенты помогают формально проверять программный код. Исследователи применили её к библиотеке libsignal, реализации протокола Signal, и описали доказательства для отдельных свойств безопасности скомпилированной программы.
Команда связала исходный Rust-код с формальной моделью машинного кода AArch64 в Lean. Сначала специалисты вместе с агентами подготовили и проверили спецификации — точные утверждения о том, какие свойства должны сохраняться. Затем агенты построили доказательства, которые проверяет ядро Lean. В технической статье говорится примерно о 6,5 миллиона строк доказательного кода.
Работа охватывала свойства механизмов PQXDH и Triple Ratchet, включая секретность сообщений и устойчивость после временной компрометации устройства. Авторы также вернули в изолированную копию два ранее исправленных дефекта: система доказала, что изменённые версии нарушают заданные свойства.
Здесь важно не только создание доказательств, но и их машинная проверка. Однако границы задаёт спецификация: исследователи определяют, что именно доказывать и какие допущения принять. Результат относится к конкретной библиотеке и формальной модели выполнения, а не автоматически ко всем приложениям Signal, устройствам и возможным угрозам.
Что пока неизвестно
Работа выполнена исследователями Google DeepMind и Google; независимая репликация результата в публикации не приводится. Доказательства охватывают указанные свойства libsignal в модели AArch64/Lean и опираются на спецификации, проверенные людьми, контракты для части криптографических примитивов и ограничения формальной модели. Это не доказательство абсолютной безопасности всех версий и приложений Signal. Около 6,5 миллиона строк — объём доказательного кода, а не исходного кода программы.
Источники
- Google DeepMind — Introducing AlphaProof Code
- Google DeepMind — AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level
Источник не открывается?
Оригинальная страница может быть временно недоступна. Попробуйте открыть её позже; название и дата источника сохранены выше.