DeepMind математически доказал надежность протокола Signal

Исследователи лаборатории Google DeepMind представили систему AlphaProof Code. С ее помощью разработчики впервые математически доказали безопасность реального исходного кода криптографического протокола Signal.

Формальная верификация считается наивысшим стандартом надежности в разработке ПО. Традиционно этот процесс требует многолетней ручной работы экспертов и обычно ограничивается проверкой теоретических спецификаций, а не готового кода. 

Команда DeepMind объединила работу людей и автономных ИИ-агентов на базе модели Gemini Carbon. Специалисты перевели требования к безопасности Signal на язык строгих математических формул, после чего агенты написали более шести миллионов строк доказательств на языке Lean.

Весь процесс занял четыре недели вместо нескольких лет. Чтобы подтвердить точность системы, авторы добавили в изолированную копию протокола две реальные уязвимости из прошлых версий. AlphaProof Code выявил обе ошибки и сформировал машинные доказательства их небезопасности.

Технический директор Signal Эрен Крет назвал разработку важным прорывом. По его словам, переход от анализа небольших фрагментов к полной автоматической проверке рабочей кодовой базы значительно усиливает гарантии приватности для пользователей. 

Протокол Signal защищает личные сообщения миллиардов людей в приложениях Signal и Google Messages. Команда DeepMind уже опубликовала материалы исследования в открытом доступе и планирует применить систему для проверки другого критически важного софта.

Напомним, 10 ноября Google открыла доступ к Gemini 4 Carbon — флагманской модели искусственного интеллекта для сложных вычислений, кибербезопасности и разработки ПО.

Подписывайтесь на ForkLog в социальных сетях

Telegram (основной канал) Facebook X