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