Google DeepMind формально верифицировала протокол Signal ...

Исследователи Google DeepMind представили AlphaProof Code — новую систему на базе ИИ-агентов, которая позволила формально верифицировать код криптографического протокола Signal. Это технология, защищающая миллиарды частных бесед в таких приложениях, как Signal и Google Messages.

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

A workflow diagram illustrating a three-step system verification process: 1) Specification, where a Lean spec is drafted and approved; 2) Code, where compiled machine code runs on a Lean processor model; and 3) Proof, where a prover team generates proofs verified by a gatekeeper.

AlphaProof Code представляет собой мультимодельную агентную систему (multi-LLM agentic framework), которая разделяет работу так же, как это сделала бы исследовательская команда. Эксперты-люди в сотрудничестве с ИИ решают, что именно нужно доказать, переводя цели безопасности Signal в формальные математические спецификации. Затем группа ИИ-агентов на базе модели Gemini Carbon выполняет сами доказательства.

В ходе работы агенты сгенерировали более шести миллионов строк кода на Lean — компьютерном языке, предназначенном для математического доказательства точности программного обеспечения. После этого агенты провели аудит доказательств и выделили участки, требующие дополнительной проверки человеком. Это составило всего один процент от всей кодовой базы, что позволило экспертам сэкономить огромное количество времени и сосредоточиться только на тех участках, где критически важно человеческое суждение.

Большинство проверок криптографических протоколов обычно останавливается на уровне их архитектурного дизайна. Однако агенты DeepMind пошли дальше: они доказали, что скомпилированный код выполняет ключевые свойства безопасности вплоть до точных инструкций, выполняемых на устройствах. Это критически важно, поскольку реальные уязвимости часто скрываются именно в разрыве между изначальным дизайном и его практической реализацией.

Также по темеAnthropic научила модель Claude проектировать электронику от идеи до прототипа

A diagram illustrating a three-step formal verification workflow (Specification, Code, and Proof) using Lean, where specifications and compiled code are processed by an untrusted prover team and validated by a trusted gatekeeper to produce verified theorems and proofs.

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

Технический директор Signal Эрен Крет (Ehren Kret) отметил, что использование ИИ-агентов для автоматического перевода рабочего кода в валидные теоремы Lean является крупным прорывом, который позволяет значительно расширить масштабы формальной верификации.

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