Дослідники з Google DeepMind вперше в історії використали штучний інтелект для формальної верифікації системи безпеки месенджера Signal. Це стало можливим завдяки математичному доказу, що пов'язує гарантії безпеки протоколу з його реальним криптографічним імплементацією.
Для цього команда DeepMind застосувала багатоагентну систему AlphaProof Code, що базується на мові математичних доказів Lean та моделях Gemini Carbon.
Що перевірив ШІ
AlphaProof Code проаналізував ключові криптографічні механізми Signal, зокрема:
- постквантовий рукокостискання PQXDH — перевірка захисту від атак з використанням квантових комп’ютерів;
- Протокол Triple Ratchet — верифікація гарантій секретності, автентифікації, захисту після компрометації та безпеки обміну ключами.
ШІ-агенти згенерували 6,5 млн рядків коду Lean, після чого система провела аудит та виділила ділянки для додаткового аналізу людьми.
Гібридний підхід: людина + ШІ
Проект демонструє синергію між дослідниками та ШІ. Науковці визначили математичні специфікації безпеки Signal, а агенти Gemini Carbon створили докази їхньої правильності для машинного коду. Сварат Чаудхурі з Google DeepMind зазначив, що нова система дозволяє масштабувати процес верифікації.
Прорив для індустрії
Традиційна формальна верифікація складного програмного забезпечення вимагала значних ресурсів. Наприклад, верифікація мікроядра seL4 тривала 20 років. Використання AlphaProof Code дозволило команді з п’яти осіб перевірити протокол Signal всього за чотири тижні. У DeepMind підкреслюють, що автоматизована перевірка коду стає критично важливою на фоні зростання кібератак. Наступним кроком буде застосування цієї технології на етапі проєктування програмного забезпечення.
Джерело: dev.ua (https://dev.ua/news/shi-vid-google-deepmind-upershe-veryfikuvav-kod-protokolu-zakhystu-signal-1794323786)