Google DeepMind формально проверила криптографический код Signal с помощью ИИ

Исследовательское подразделение Google применило новую агентную систему AlphaProof Code для проверки ключевых свойств libsignal — эталонной реализации протокола сквозного шифрования Signal. Доказательства охватывают механизмы PQXDH и Triple Ratchet на уровне машинного кода AArch64, но не всё приложение Signal.

Google DeepMind представила AlphaProof Code — агентную систему формальной верификации программного обеспечения. Специалисты формулируют и утверждают проверяемые свойства, после чего ИИ-агенты создают доказательства на языке Lean, а его ядро проверяет их корректность.

В технической работе описана проверка libsignal на уровне машинного кода. Доказательства охватывают постквантовый механизм согласования ключей PQXDH и Triple Ratchet, подтверждая заданные свойства прямой секретности, аутентификации, секретности рукопожатия и восстановления безопасности после компрометации устройства.

Агенты создали около 6,5 млн строк проверяемого Lean-кода, опираясь примерно на 26 тыс. строк доверенных спецификаций и описания семантики AArch64. По данным DeepMind, работа заняла четыре недели. Для испытания системы исследователи вернули в изолированную версию кода две реальные, ранее исправленные ошибки — AlphaProof Code смогла доказать небезопасность обеих версий.

Результат не означает формальной верификации всего мобильного приложения Signal: проверены конкретные свойства ядра криптографической реализации. DeepMind открыла спецификации и доказательства для независимого изучения и дальнейших исследований.