Шифрование Signal прошло ИИ-доказательство на 6,5 млн строк кода

У кода шифрования Signal появилось то, чем может похвастаться почти никакое широко используемое программное обеспечение: математическое доказательство того, что он делает именно то, что обещает. Команда ИИ-агентов проверила libsignal — библиотеку, на которой работает протокол Signal, — и доказала, что переписка один на один остаётся секретной, позволяет удостовериться, кто находится на другом конце диалога, и снова защищает от злоумышленника после кражи ключа. Новых уязвимостей исследователи не обнаружили.

Значение этой работы выходит далеко за пределы аудитории Signal. Протокол стал мировым стандартом для обмена сообщениями со сквозным шифрованием, а его варианты защищают переписку в WhatsApp, Messenger и Google Messages. Раньше столь глубокая проверка реального, уже выпущенного кода занимала так много времени, что за неё почти никто не брался: на один из крупнейших успехов в этой области — верификацию ядра операционной системы — ушло двадцать человеко-лет. Здесь на всё потребовалось четыре недели.

Инструмент Google DeepMind называется AlphaProof Code. Сначала специалисты и модели ИИ сформулировали цели безопасности Signal на языке Lean — языке программирования, созданном для математических доказательств, — а человек проверил каждое утверждение. Затем команды из 40–80 агентов на базе Gemini Carbon создавали доказательства, работая по 24–72 часа подряд на одной машине. В результате получилось около 6,5 миллиона строк кода на Lean.

Доверять этим миллионам строк не нужно. Ядро Lean проверяет каждый шаг и отбрасывает любое несостоятельное доказательство, поэтому неважно, какая модель его написала и сколько ошибок она допустила по пути. Доверия требует лишь гораздо меньшая часть системы: около 26 000 строк спецификаций и модель того, как процессор ARM выполняет код.

Доказательства охватывают компоненты Signal, отвечающие за безопасность переписки: рукопожатие PQXDH, которое устанавливает соединение, и Triple Ratchet, меняющий ключ для каждого сообщения, в том числе постквантовый слой, призванный противостоять будущим квантовым компьютерам. На практике это означает, что кража текущих ключей телефона не откроет доступ к старым сообщениям, а вор снова лишится доступа, как только собеседники обменяются новыми ключами.

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

Ограничения у работы вполне конкретные. Доказательство касается только сессий один на один, а DeepMind относит групповые чаты к будущим направлениям исследований. Оно применимо к libsignal версии 0.105.4, скомпилированной стандартным компилятором Rust для ARM Linux внутри небольшой тестовой программы, но не к полноценным приложениям Signal для iPhone, Android и компьютеров. Предполагается, что низкоуровневые криптографические компоненты надёжны, но сами они не доказаны. Ошибка в спецификациях, одобренных людьми, ослабила бы гарантию; кроме того, WhatsApp и другие приложения используют собственные версии протокола, поэтому результат нельзя автоматически распространить и на них. Google также отказалась сообщить Wired стоимость анализа и рассказать, планирует ли предлагать его как услугу.

Signal приветствовала результат. «По мере роста угроз безопасности, связанных с ИИ, строгая проверка реализации протокола Signal придаёт нам ещё больше уверенности в гарантиях конфиденциальности нашего кода», — заявил технический директор Signal Эрен Крет (Ehren Kret). Научный сотрудник DeepMind Сварат Чаудхури (Swarat Chaudhuri) высказался осторожнее: в разговоре с Wired он сказал, что до масштабирования метода «на всё программное обеспечение мира» ещё «очень далеко».

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

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

Чаудхури также обозначил предел того, какую часть работы стоит поручать машинам. «Мы не хотим оказаться в таком мире, где ИИ генерирует цели, а ИИ генерирует доказательства», — сказал он Wired. Люди по-прежнему решают, что считать безопасным, а ИИ лишь доказывает это.

Теги: кибербезопасность, Google DeepMind, AlphaProof Code, libsignal, Signal, сквозное шифрование