Google DeepMind формально перевірила криптографічні гарантії протоколу Signal
За чотири тижні дослідники Google DeepMind за допомогою агентного ШІ математично підтвердили низку ключових властивостей протоколу Signal, що використовується у Signal, WhatsApp і Google Messages.
Google DeepMind повідомила про формальну верифікацію низки ключових криптографічних гарантій протоколу Signal — пілотний проєкт, виконаний за чотири тижні, що посилює незалежну валідацію шифрування в Signal, WhatsApp і Google Messages та демонструє можливості нового AI-фреймворку AlphaProof Code.
Що саме перевірили і чому це важливо
Формальна верифікація — це математичний доказ того, що протокол відповідає своїм заявленим властивостям за всіх умов, на відміну від традиційного тестування, яке лише шукає вразливості. У межах цього аналізу DeepMind не виявила нових проблем у перевірених частинах протоколу Signal.
Команда також застосувала AlphaProof Code до старіших версій Signal із відомими й давно виправленими вадами: інструмент коректно ідентифікував їх та позначив як такі, що не проходять формальну перевірку. Дослідники публікують специфікацію та доведення, створені під час аналізу, щоб підтримати подальшу роботу у сфері формальної верифікації.
Роль агентного ШІ та межі підходу
До ери ШІ підготовка специфікацій і математичних доказів була надзвичайно тривалою. Агентний ШІ суттєво скорочує цей цикл і відкриває шлях до перевірок такої складності, проте підхід є дуже ресурсоємним, і його масштабованість до великих масивів коду поки незрозуміла.
Що саме не перевіряли і на чому базувалися
Йдеться про перевірку криптографічних властивостей протоколу, а не всього мобільного застосунку Signal. Частину напрацювань базовано на попередніх (без використання ШІ) дослідженнях у галузі формальної верифікації. Масштаби обчислювальних ресурсів для цього проєкту не розкриваються.
Проміжний етап, але великий крок
Дослідники наголошують, що це лише одна з віх на довшому шляху. «Ми дуже раді цьому результату, але до масштабування на все програмне забезпечення світу ще довгий шлях», — сказав дослідник DeepMind Swarat Chaudhuri в коментарі для WIRED. Попри обмежений обсяг перевірки, результат називають знаковим для криптографії та ШІ: незалежна математична перевірка ще раз підтвердила стійкість протоколу, який захищає приватні комунікації на платформах типу Signal, Google Messages і WhatsApp (загалом — мільйони користувачів).
Фото: 9to5Mac
