Google DeepMind використовує агентний ШІ для формальної верифікації протоколу Signal

Дослідники Google DeepMind використали агентний ШІ, щоб математично довести, або формально перевірити, низку ключових криптографічних гарантій протоколу Signal у проєкті доказу концепції, завершеному за чотири тижні. Робота слугує додатковим незалежним підтвердженням криптографії, що захищає спілкування на таких платформах, як застосунок Signal, Google Messages і WhatsApp, і демонструє можливості DeepMind у формальній верифікації з використанням нового ШІ-фреймворку AlphaProof Code.

Що виявив аналіз

Аналіз DeepMind не виявив нових вразливостей у тих частинах протоколу Signal, які він перевіряв. Коли дослідники використали AlphaProof Code на старіших версіях Signal, що містять відомі й давно виправлені вразливості, він правильно їх виявив і показав, що протокол не міг бути формально перевірений. Аналіз не перевірив формально весь мобільний застосунок Signal, а дослідники DeepMind описують свої результати як одну віху в більшому процесі. Дослідники публікують специфікацію й доведення, які вони розробили для аналізу протоколу Signal, щоб допомогти іншій роботі з формальної верифікації.

Чому важлива формальна верифікація

Формальна верифікація використовує математику, щоб перевіряти й підтверджувати, що програмне забезпечення працює як задумано, тому прихильники давно називали її своєрідним святим Ґраалем безпеки програмного забезпечення. До ери ШІ людям було надзвичайно часозатратно описувати характеристики програмного забезпечення, яке вони хотіли довести, перетворювати ці описи на формули, а потім розробляти доведення. Агентний ШІ може значно скоротити час виконання останнього завдання, що робить можливими аналізи на кшталт оцінювання Signal від DeepMind. Ключові досягнення DeepMind включають процес співпраці людини й ШІ, який дає змогу агентам робити внесок і самостійно виправлятися майже на кожному етапі, водночас звертаючись до людського внеску й перевірки на ключових етапах. «Ми не хочемо такого світу вайбу, де ШІ генерує цілі, ШІ генерує доведення й по суті проходить тести, які сам написав», каже Swarat Chaudhuri, науковий співробітник DeepMind, в інтерв'ю WIRED. «Є серединний шлях.»

Відкриті питання щодо масштабу й вартості

Залишається незрозумілим, наскільки практичною буде формальна верифікація за допомогою ШІ для широкого використання й наскільки ефективною вона може бути для захисту великих обсягів коду. DeepMind провів аналіз Signal безкоштовно як дослідницький проєкт, а Google відмовився розкрити вартість аналізу або прокоментувати, чи має плани випустити комерційний продукт чи послугу формальної верифікації. Ehren Kret, головний технічний директор Signal, каже в заяві, що раніше формальна верифікація зосереджувалася на менших частинах коду, тоді як підхід Google DeepMind дає змогу значно розширити охоплення. «Оскільки загрози безпеці, спричинені ШІ, зростають, ретельна перевірка реалізації протоколу Signal дає нам ще більшу впевненість у гарантіях конфіденційності нашого коду», каже Kret. Pushmeet Kohli, головний науковець Google Cloud і віцепрезидент з досліджень DeepMind, каже, що якщо тепер можна перевірити правильність реалізацій, компанії, які покладаються на гарантії й переймаються помилками, можуть сказати, що можуть довести ці властивості. Chaudhuri каже, що DeepMind радіє результату, але до масштабування цього на все програмне забезпечення світу ще довгий шлях.

Джерела: Wired