Искусственный интеллект математически подтвердил безопасность шифрования Signal
Исследователи Google DeepMind разработали систему искусственного интеллекта AlphaProof Code, которая впервые позволила провести математическую проверку ключевых механизмов шифрования, используемых в мессенджере Signal. Результаты исследования опубликованы 10 ноября на сайте Google DeepMind.
В отличие от традиционного тестирования программного обеспечения, при котором специалисты ищут уязвимости и ошибки, новая технология позволяет математически доказать, что программный код соответствует заданным требованиям безопасности. Проверка проводилась непосредственно на уровне машинного кода, а не только теоретической модели криптографического протокола.
Исследователи использовали группу ИИ-агентов на основе моделей Gemini, которые подготовили около 6,5 миллиона строк математических доказательств. Их правильность автоматически проверялась с помощью системы Lean, предназначенной для формальной проверки математических утверждений.
Вся работа заняла четыре недели. По оценке разработчиков, выполнение аналогичной задачи традиционными методами могло потребовать нескольких лет работы специалистов.
Проверка охватывала основные механизмы криптографического протокола Signal, включая защиту переписки при компрометации отдельных ключей и обеспечение безопасности последующих сообщений даже после временного получения злоумышленником доступа к устройству. В исследовании рассматривались и механизмы защиты от некоторых угроз, связанных с развитием квантовых вычислений.
Для проверки эффективности AlphaProof Code ученые намеренно вернули в исследуемый код две ранее обнаруженные и уже исправленные ошибки. Система успешно выявила нарушения требований безопасности в обеих случаях.
Криптографический протокол Signal применяется не только в одноименном мессенджере, но и в других популярных сервисах обмена сообщениями, включая WhatsApp и Google Messages. Поэтому результаты исследования имеют значение для защиты переписки миллиардов пользователей.
При этом разработчики подчеркивают, что исследование не доказывает абсолютную защищенность мессенджера Signal от любых атак. Проверялись определенные криптографические свойства конкретной версии программного кода. Работа не охватывала все компоненты приложения, групповые чаты и некоторые сценарии атак.
Технический директор Signal Эрен Крет назвал результаты важным достижением, которое существенно расширяет возможности формальной проверки криптографических систем.
Исследователи Google DeepMind опубликовали программный код и математические доказательства в открытом доступе, чтобы независимые специалисты могли изучить и проверить результаты. В перспективе технология может применяться для анализа безопасности банковских систем, медицинского оборудования, энергетической инфраструктуры и другого критически важного программного обеспечения.
