ИИ DeepMind доказал, что код шифрования Signal выполняет главные обещания безопасности

Google DeepMind заявила, что её ИИ-агенты математически доказали: код шифрования Signal для личных чатов выполняет свои главные обещания по безопасности. Работу, представленную 10 ноября, сделали с помощью новой системы AlphaProof Code, и проверяли в ней саму скомпилированную программу, то есть код, который реально исполняется. По словам DeepMind, это первый случай, когда реализацию широко используемого криптографического протокола формально проверили хоть каким-то способом, с ИИ или без. Новых уязвимостей в проверенных частях не нашлось.

Что именно доказали

Формальная верификация - это когда свойство безопасности записывают как математическое утверждение и доказывают, что программа выполняет его всегда, а не только на тестовых примерах. Обычно протоколы вроде Signal проверяют на уровне схемы. DeepMind спустилась до машинного кода: команда взяла libsignal версии 0.105.4 и библиотеку spqr, собрала их под 64-битный ARM Linux обычным компилятором Rust и доказывала свойства уже готового исполняемого файла, говорится в техническом описании.

Сначала исследователи вместе с несколькими ИИ-моделями перевели цели безопасности Signal в формальные спецификации, и каждую проверил человек. Затем агенты на модели Gemini Carbon написали доказательства на Lean - языке, в котором каждый шаг проверяется автоматически. Получилось около 6,5 млн строк. Примерно 1% из них агенты отметили для проверки людьми, а весь проект занял четыре недели. Среди десяти доказанных теорем есть прямая секретность, которая защищает старые сообщения, если ключ утечёт позже, и восстановление после взлома, которое возвращает защиту после того, как устройство временно было скомпрометировано.

Чтобы убедиться, что система отличает правильный код от ошибочного, команда вернула в изолированную копию кода две настоящие ошибки Signal, давно исправленные. В обоих случаях AlphaProof Code выдала проверенное машиной доказательство того, что версия с ошибкой небезопасна.

Что осталось за рамками

Ограничения в описании перечислены подробно. Мобильные приложения напрямую не проверяли, и авторы лишь ожидают, что результат на них перенесётся, если приложения исполняют код протокола без изменений. Групповые чаты оставлены на будущее. Сторонние каналы, например утечки по времени выполнения или энергопотреблению, в проверку не входили, как и генерация ключей и работа на нескольких устройствах. Кроме того, доказательства исходят из того, что базовые криптографические примитивы надёжны. Технический директор Signal Эрен Крет сказал, что работа «даёт ещё больше уверенности» в том, что код выполняет обещания о приватности.

В блоге DeepMind среди приложений на этом протоколе названы Signal и Google Messages. WhatsApp перешёл на протокол Signal много лет назад, но проверяли собственный код Signal, а не программы WhatsApp, поэтому о WhatsApp эта работа ничего нового не говорит. Отчасти она опиралась на прежнюю формальную проверку Signal, сделанную без ИИ. Метод к тому же дорогой: в Google сказали Wired, что он требует больших вычислений, а исследователь Сварат Чаудхури заметил, что «предстоит пройти ещё долгий путь», прежде чем так можно будет проверять всё программное обеспечение в мире, пишет 9to5Mac. DeepMind выложила доказательства на GitHub, так что их могут перепроверить сторонние специалисты.