Google DeepMind формально верифікувала частину протоколу Signal — Ars Technica
Google DeepMind за допомогою агентного штучного інтелекту математично підтвердила низку ключових криптографічних гарантій протоколу Signal. Дослідницький проєкт, який тривав чотири тижні, мав демонстраційний характер і використовував новий ШІ-фреймворк AlphaProof Code, повідомляє Ars Technica.
Перевірка криптографічних властивостей
Формальна верифікація — це математична перевірка того, чи відповідає програмне забезпечення заданим властивостям і чи не має критичних вразливостей. До появи ШІ цей процес забирав багато часу: фахівцям потрібно було описати властивості програми, перетворити їх на формули та побудувати математичний доказ.
За даними видання, агентний ШІ здатен суттєво скоротити час, необхідний для створення такого доказу. Водночас дослідження DeepMind мало обмежений масштаб: воно не охоплювало весь мобільний застосунок Signal, а стосувалося окремих частин протоколу.
Під час аналізу дослідники не виявили нових вразливостей у перевірених частинах протоколу Signal. Коли AlphaProof Code застосували до старіших версій Signal із відомими та давно виправленими проблемами, система правильно виявила ці вразливості й показала, що за їхньої наявності протокол не можна формально верифікувати.
Більше актуальних новин читайте у Telegram-каналі UA.News.
Межі дослідження
У DeepMind наголосили, що результат є лише одним етапом ширшої роботи. Масштабування формальної верифікації за допомогою ШІ на великі обсяги програмного коду та всі програмні системи ще потребує подальшого розвитку.
Дослідники також зазначили, що швидшому проведенню аналізу сприяли попередні роботи Signal Foundation із формальної верифікації окремих частин коду. DeepMind оприлюднює специфікацію та доказ, створені для аналізу Signal, щоб їх можна було використати в інших дослідженнях формальної верифікації.
Компанія провела проєкт безоплатно як дослідницький, не розкривши його вартості. Google також не повідомила, чи планує запускати комерційний продукт або сервіс для формальної верифікації.
У DeepMind описали підхід як співпрацю людини й ШІ: агенти можуть допомагати на різних етапах і виправляти власну роботу, але на ключових етапах передбачені людський внесок і перевірка.
