Хочете будувати кар’єру в Data Science та AI? Vodafone Big Data Lab відкриває новий набір —>
Наталя ХандусенкоШІ
10 листопада 2026, 17:26
2026-11-10
ШІ від Google DeepMind уперше верифікував код протоколу захисту Signal: як це працює та чому це важливо
Дослідники з Google DeepMind провели формальну верифікацію системи безпеки месенджера Signal. Це перший у історії випадок, коли штучний інтелект допоміг створити математичний доказ, який пов’язує фундаментальні гарантії безпеки протоколу із його реальною криптографічною імплементацією.
Для цього команда DeepMind використала багатоагентну систему AlphaProof Code, побудовану на базі мови математичних доказів Lean та моделей Gemini Carbon.
Дослідники з Google DeepMind провели формальну верифікацію системи безпеки месенджера Signal. Це перший у історії випадок, коли штучний інтелект допоміг створити математичний доказ, який пов’язує фундаментальні гарантії безпеки протоколу із його реальною криптографічною імплементацією.
Для цього команда DeepMind використала багатоагентну систему AlphaProof Code, побудовану на базі мови математичних доказів Lean та моделей Gemini Carbon.
постквантовий рукокостискання PQXDH — перевірено захист від потенційних атак із використанням майбутніх квантових комп’ютерів;
Протокол Triple Ratchet — верифіковано гарантії прямильної секретності, автентифікації, захисту після компрометації та безпеки обміну ключами.
Під час дослідження ШІ-агенти згенерували 6,5 млн рядків коду Lean. Після цього система провела аудит і виділила ділянки, які потребували додаткового аналізу з боку людей.
Гібридний підхід: людина + ШІ
Особливість проєкту полягає у синергії дослідників та штучного інтелекту. Науковці сформулювали математичні специфікації цілей безпеки Signal, а агенти Gemini Carbon створили докази їхньої правильності для машинного коду.
«Це система, яка фундаментально створена для співпраці людини та ШІ. Раніше вважалося, що найскладніше у формальних методах — це сам процес верифікації. Завдяки ШІ ми навчилися це масштабувати. Тепер головне питання: що саме ми верифікуємо? І цей процес формалізації вимог залишається за людиною», — пояснив дослідник Google DeepMind та професор Техаського університету в Остіні Сварат Чаудхурі.
Чому це прорив для індустрії
Традиційна формальна верифікація складного ПЗ вимагала колосальних ресурсів. Наприклад, верифікація мікроядра seL4 тривала 20 людино-років, а розробка верифікованого компілятора CompCert C — 6 років.
Використання AlphaProof Code дозволило команді з п’яти осіб повністю перевірити криптографічний протокол Signal всього за чотири тижні.
У DeepMind зазначають, що на тлі стрімкого розвитку інструментів для кібератак (зокрема «наступального ШІ»), автоматизована перевірка коду стає критично важливою. Наступним кроком компанії стане застосування цієї технології ще на етапі проєктування програмного забезпечення — не лише для криптографії, а й для загального софту по всьому світу.
«Чи є у мене талант, якщо комп’ютер може імітувати мене?». Штучний інтелект пише книги авторам Amazon Kindle. The Verge поспілкувався з авторами та виявив багато цікавого
Письменники-романісти використовують штучний інтелект для створення своїх творів. Видання про технології The Verge поспілкувалося з письменницею Дженніфер Лепп, яка випускає нову книгу кожні дев’ять тижнів, й дізналося про те, як працює штучний інтелект для написання романів. Наводимо адаптований переклад статті.
Хочете повідомити важливу новину? Пишіть у Telegram-бот
Головні події та корисні посилання в нашому Telegram-каналі
