Google DeepMind за допомогою ШІ довела безпеку шифрування Signal аж до машинного коду

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

Що саме перевірили

Інструмент отримав назву AlphaProof Code. Його застосували до libsignal — еталонної бібліотеки, на якій тримається наскрізне шифрування Signal. За даними CyberInsider, дослідники аналізували виконуваний файл версії 0.105.4, зібраний для 64-бітних процесорів Arm, і змоделювали роботу машинних інструкцій так, щоб твердження про програму можна було перевірити формально.

Під перевірку потрапили дві центральні частини протоколу:

• PQXDH — початкове «рукостискання», під час якого співрозмовники домовляються про спільний секрет;
• Triple Ratchet — механізм, що постійно оновлює ключі шифрування під час листування;
• властивості на кшталт прямої секретності (forward secrecy) та відновлення захисту для майбутніх повідомлень після обміну свіжими ключами;
• секретність рукостискання в моделі, де зловмисник згодом може зламати класичний обмін Діффі — Геллмана, що імітує загрозу з боку майбутніх квантових комп'ютерів.

Як працювали ШІ-агенти і люди

Доведення записані мовою Lean — це система, яка приймає доведення лише тоді, коли кожен його крок проходить автоматичну перевірку. Агенти на основі моделей Gemini, за даними CyberInsider, згенерували близько 6,5 мільйона рядків такого коду. Axios також пише про мільйони рядків машинно перевірених доведень.

Водночас роль людей залишалася ключовою. ШІ допомагав сформулювати кожну безпекову ціль у вигляді математичної специфікації, але ці специфікації переглядали експерти. Щоб переконатися, що інструмент не «доводить» будь-що, команда повернула в ізольовані копії коду дві давно виправлені помилки. В обох випадках система видала машинно перевірене доведення того, що змінений код порушує властивість безпеки.

За даними CyberInsider, технічний директор Signal Ерен Крет зазначив, що робота розширює масштаб попередніх перевірок протоколу й додає проєкту впевненості в його гарантіях приватності. Артефакти верифікації DeepMind оприлюднила на GitHub.

Межі результату

Важливо розуміти, чого ця робота не означає. Вона не доводить, що весь застосунок Signal бездоганний. Гарантії спираються на моделі зловмисника, які обрали дослідники, і на припущення, що базові криптографічні операції надійні. Поза межами перевірки залишилися атаки через побічні канали та решта коду месенджера — інтерфейс, зберігання даних, мережеві компоненти.

Нових вразливостей у поточній версії протоколу, за повідомленнями, не виявили. Тобто йдеться не про «знахідку» дірки в безпеці, а про підтвердження того, що реалізація робить саме те, що обіцяє її математична модель, — за чітко сформульованих умов.

Окремо варто наголосити на рівні перевірки. Більшість попередніх досліджень протоколу Signal аналізували або абстрактну модель, або вихідний код. Проте між кодом, який пише програміст, і інструкціями, які виконує процесор, стоїть компілятор, і теоретично помилка може виникнути саме на цьому етапі. Перевірка скомпільованої програми закриває цю прогалину для обраних властивостей.

Чому це важливо

Формальна верифікація давно вважається «золотим стандартом» у безпеці програмного забезпечення, але вона надзвичайно трудомістка: доведення для складних систем пишуть місяцями й роками, тому їх застосовують здебільшого в авіації, мікропроцесорах чи криптографічних бібліотеках. Якщо ШІ-агенти здатні за кілька тижнів довести властивості реального скомпільованого коду, це може зробити такий рівень перевірки доступним для значно ширшого кола проєктів.

Для користувачів месенджерів головний висновок простий: механізм, який захищає їхні повідомлення в Signal, тепер має ще одне незалежне математичне підтвердження. Для галузі — це сигнал, що ШІ може не лише писати код, а й перевіряти його надійність, причому з результатами, які можна відтворити й перевірити без довіри до самої моделі.