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

Google DeepMind представила AlphaProof Code — мультиагентную ИИ-систему для формальной верификации, то есть математического доказательства того, что программа делает именно то, что записано в её спецификации. Первым крупным испытанием стала libsignal — эталонная реализация протокола Signal, который защищает переписку в Signal, Google Messages и других приложениях.

Что доказано

• Эксперты вместе с ИИ-моделями записали формальные спецификации целей безопасности Signal и проверили каждую из них.
• Затем агенты-доказчики (по словам DeepMind, на базе Gemini Carbon) создали около 6,5 млн строк доказательств на языке Lean, опирающихся примерно на 26 тыс. строк доверенных спецификаций и формальной модели машинного кода AArch64.
• Доказательства охватывают постквантовое рукопожатие PQXDH и Triple Ratchet: прямую секретность, аутентификацию, безопасность после компрометации и секретность рукопожатия — для скомпилированного машинного кода немодифицированной libsignal v0.105.4, а не только для схемы протокола.
• Работа заняла четыре недели. Для проверки команда вернула в изолированную копию две реальные, давно исправленные ошибки — и система доказала, что такие версии небезопасны.

Ограничения

Криптографические примитивы и несколько библиотечных функций считались доверенными и не проверялись. Мобильное приложение Signal целиком не верифицировалось, новых уязвимостей не найдено. WIRED отмечает, что пока неясно, насколько такая проверка будет практичной и доступной по цене в больших масштабах; стоимость Google не раскрыла. Доказательства на Lean опубликованы в открытом доступе.