Читайте в Telegram
|
Исследователи Google DeepMind с помощью ИИ-агентов формально доказали ряд ключевых криптографических гарантий протокола Signal, пишет Wired.
Формальная верификация — это математическое доказательство того, что программа или протокол выполняют заявленные свойства безопасности. Обычное тестирование ищет уязвимости, а верификация доказывает, что в рамках принятой модели эти свойства выполняются.
Протокол Signal используют не только в этом мессенджере, но и в Google Messages и WhatsApp (принадлежит Meta, признанной в России экстремистской организацией). Для проверки DeepMind применила новый инструмент AlphaProof Code. Работа заняла четыре недели и была пилотным проектом. Быстро провести проверку помогли прошлые работы Signal Foundation по формальной верификации.
Новых уязвимостей в проверенных частях протокола исследователи не нашли. Когда они запустили AlphaProof Code на старых версиях Signal с давно исправленными ошибками, инструмент нашёл их и показал, что такие версии формально верифицировать нельзя. Спецификацию и доказательство DeepMind выложит в открытый доступ.
Приложение Signal целиком не верифицировали. DeepMind провела анализ бесплатно как исследовательский проект, стоимость работы Google не раскрывает.
Научный сотрудник DeepMind Сварат Чаудхури сказал Wired, что команда очень рада результату, но «предстоит пройти долгий путь, прежде чем мы сможем масштабировать это на всё ПО в мире».
Технический директор Signal Эрен Крет заявил, что прошлые проверки охватывали небольшие части кода, а подход DeepMind позволяет значительно расширить их.
