Исследователи Google DeepMind с помощью ИИ провели формальную проверку безопасности протокола Signal, сообщает IT Home. Речь о математической проверке свойств сквозного шифрования в заданной модели, а не о полном аудите приложения Signal.
Формальная проверка отличается от поиска уязвимостей тестами: она позволяет доказать, что протокол отвечает заданным требованиям безопасности при всех условиях, предусмотренных моделью. Исследователи также проверили старые реализации протокола с известными уязвимостями. ИИ обнаружил проблемы и установил, что эти версии проверку не проходят.
Работа не начиналась с нуля: команда использовала результаты прежних формальных проверок, часть которых была выполнена без ИИ. Анализ занял около четырёх недель. Google не раскрыла объём затраченных вычислительных ресурсов и сообщила Wired, что пока не может оценить, насколько такой подход пригоден для широкого применения.
Источник: IT Home.
