Исследователи Google DeepMind с помощью агентного искусственного интеллекта математически подтвердили ряд ключевых криптографических свойств протокола Signal. Такой процесс называют формальной верификацией — проверкой корректности программных решений с помощью математических доказательств. Работа стала значимым этапом как для защиты цифровых сообщений, так и для развития инструментов искусственного интеллекта.
Проект был выполнен в формате экспериментальной проверки всего за четыре недели. Его результаты дополнительно подтвердили надёжность криптографии, применяемой для защиты большого объёма переписки в Signal, Google Messages и WhatsApp. Кроме того, исследование показало возможности новой системы Google DeepMind под названием AlphaProof Code.
Формальная верификация позволяет математически проверить, работает ли программное обеспечение так, как задумано, и не содержит ли критических уязвимостей. Раньше специалистам приходилось вручную описывать свойства программы, переводить эти описания в формулы и затем строить доказательство, что требовало значительного времени. Агентный искусственный интеллект способен заметно ускорить последний этап этой работы.
При этом проведённая проверка охватила только отдельные компоненты протокола Signal, а не всё мобильное приложение. Исследователи Google DeepMind подчеркнули, что рассматривают полученный результат лишь как один из этапов более масштабной работы. «Мы очень воодушевлены этим результатом, но до возможности масштабировать эту технологию на всё программное обеспечение в мире ещё очень далеко, и мы хотим этого добиться», — заявил научный сотрудник DeepMind Сварат Чаудхури в комментарии Ars Technica.
В проверенных фрагментах протокола новых уязвимостей не обнаружили. Когда AlphaProof Code применили к более ранним версиям Signal с известными и уже устранёнными проблемами, система правильно выявила эти недостатки и показала, что протокол не может пройти формальную верификацию. Разработанные спецификацию и доказательство для анализа Signal исследователи решили предоставить другим специалистам, работающим над формальной проверкой программного обеспечения.