DeepMind проверил безопасность криптобиблиотеки Signal с помощью ИИ

Компания Google DeepMind проверила четыре свойства безопасности в криптографической библиотеке libsignal — реализации протокола Signal, варианты которого используются в Signal, Google Messages и WhatsApp, — на уровне машинного кода с помощью системы AlphaProof Code.

В ходе проверки были подтверждены такие свойства, как forward secrecy (прямая секретность), аутентификация, post-compromise security (безопасность после компрометации) и секретность начального обмена ключами (handshake secrecy). Проверка охватывала два компонента библиотеки — постквантовый протокол начального согласования ключей и механизм обновления ключей сообщений Triple Ratchet.

Процесс проверки включал несколько этапов: человек с помощью агента составлял спецификацию на языке Lean, выполнение машинного кода описывалось формальной моделью, а ядро Lean проверяло доказательство, составленное агентом, на соответствие спецификации. Для подтверждения работоспособности системы в изолированную версию кода Signal повторно внедрили две ранее исправленные ошибки — система корректно их выявила.

При этом ряд свойств безопасности остался за пределами проверки. Например, криптографическая отрицаемость (deniability), управление сессиями на нескольких устройствах и некоторые другие функции не были охвачены верификацией. Символические доказательства предполагают идеальную криптографию; вычислительные ограничивают вероятность успешной атаки при допущениях о стойкости криптографических алгоритмов и не охватывают квантовых противников.

DeepMind опубликовала материалы верификации, включая спецификации и доказательства. По словам представителей компании, подход позволяет перейти от проверки на уровне проектирования к анализу реализации — именно в разрыве между ними часто скрываются уязвимости.

Ранее по теме: Искусственный интеллект находит уязвимости в смарт-контрактах и объясняет их

Источник: Tech Insider