ИИ-агенты Google DeepMind математически проверили код шифрования Signal
Агенты Google DeepMind за четыре недели доказали, что рабочий код Signal выполняет главные гарантии защиты переписки. По словам компании, у экспертов на такое обычно уходят годы.
Google DeepMind представила AlphaProof Code — систему ИИ-агентов, которая за четыре недели математически доказала ключевые свойства защиты в рабочем коде протокола Signal. Этим протоколом шифруются миллиарды личных переписок в Signal, Google Messages и других приложениях.
Почему это важно: криптографические протоколы формально проверяют уже десятилетиями, но обычно только на уровне замысла. При этом настоящие уязвимости часто прячутся там, где замысел превращается в код. DeepMind утверждает, что реализацию настолько массового протокола формально проверили впервые — любым способом, с ИИ или без.
Как это работает: формальная проверка не прогоняет тесты, а доказывает, как теорему, что программа делает ровно то, что обещано. Исследователи вместе с несколькими моделями перевели цели защиты Signal в математические требования, и каждое из них прочитали эксперты. Сами доказательства писали агенты на модели Gemini Carbon. Получилось более шести миллионов строк на Lean — языке, в котором каждый шаг рассуждения проверяет компьютер.
Читать миллионы строк людям не пришлось. Агенты сами просмотрели доказательства и отметили места, которые стоит перепроверить человеку, — около 1% кода доказательств. Остальное автоматически проверяет Lean.
Детали: доказательства доходят до скомпилированного кода, то есть до тех команд, которые выполняет устройство. Для этого машинный код запускали на модели процессора, описанной на Lean. Одно из доказанных свойств касается временного взлома устройства: ключи, которые взломщик успел украсть, не открывают перехваченную раньше переписку. А защита новых сообщений возвращается, как только стороны сменят ключи на те, которых взломщик не знает.
Чтобы убедиться, что система отличает правильный код от ошибочного, исследователи вернули в отдельную копию кода Signal две настоящие ошибки, которые в Signal давно исправили. Оба раза система выдала проверенное компьютером доказательство того, что такая версия небезопасна.
Что говорят: «Прежние формальные проверки охватывали меньшие части кода, а подход Google DeepMind позволяет заметно расширить охват», — сказал технический директор Signal Эрен Крет. Сотрудники Signal оценивали методику проверки.
Но: как пишет Wired, в проверенных частях новых уязвимостей не нашлось, а приложение Signal целиком не проверяли — только ядро шифрования. В самой DeepMind признают, что применять метод шире можно будет только после новых исследований. Сколько стоила работа и станет ли она платной услугой, Google не говорит.
Что дальше: DeepMind выкладывает материалы проверки в открытый доступ. Компания считает, что работа закладывает основу для проверки других важных систем — от прошивок медицинских приборов до программ, которые управляют энергосетями. Такие доказательства она предлагает сочетать с агентом CodeMender1.
Имя AlphaProof DeepMind уже давала системе, которая решила три задачи Международной математической олимпиады2 2024 года. Результата уровня серебряной медали она добилась вместе с AlphaGeometry 2: та решила ещё одну задачу, геометрическую. Доказательства AlphaProof тоже писала на Lean.