Google DeepMind с помощью ИИ доказала безопасность отдельных механизмов протокола Signal
Изображение: OpenAI
Исследователи Google DeepMind с помощью ИИ доказали, что несколько ключевых механизмов защиты протокола Signal работают как задумано, пишет WIRED. Они использовали новый инструмент AlphaProof Code, но проверка не охватывала мобильное приложение Signal целиком.
Исследовательский проект занял четыре недели. Команда опиралась на предыдущие работы Signal Foundation по формальной верификации — математической проверке того, что программа работает в соответствии с заданными требованиями. По словам технического директора Signal Ehren Kret, прежняя верификация охватывала небольшие части кода, а подход DeepMind позволяет значительно её расширить.
Протокол Signal защищает переписку в популярных приложениях: Signal, Google Messages и WhatsApp (мессенджер, принадлежит запрещённой в России и признанной экстремистской американской корпорации Meta).
Новых уязвимостей в проверенных частях протокола команда не нашла. При испытании на старых версиях Signal AlphaProof Code выявил известные и давно исправленные уязвимости и показал, что математически подтвердить безопасность этих версий нельзя.
Исследователи публикуют спецификацию и доказательство, чтобы их могли использовать в других работах по формальной верификации.
В разработанном DeepMind процессе ИИ-агенты участвуют почти на всех этапах проверки и могут исправлять собственные ошибки. На ключевых этапах люди проверяют их работу и дают указания.
Пока неясно, удастся ли применять такие проверки в широком масштабе и при приемлемой стоимости. Google не раскрыла затраты на исследовательский проект и отказалась комментировать планы по выпуску коммерческого продукта или сервиса для формальной верификации.
