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