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