Виталик Бутерин отвергает утверждение о гибели кибербезопасности из-за ИИ

Бутерин написал в своем посте от 17 сентября в X, что не согласен с все более распространенным мнением о том, что «взлом с помощью ИИ означает гибель кибербезопасности». Он сказал, что люди, продолжающие держать криптовалюту, неявно делают ставку на то, что защищенные цифровые системы смогут выдержать более сильные автоматизированные атаки, добавив, что примерно 90% его собственного состояния остается в криптовалюте.

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

Бутерин считает, что формальная верификация может дать преимущество защитникам

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

Собственная документация Ethereum по формальной верификации описывает этот метод более узко. В ней говорится, что формальная верификация может математически доказать, что смарт-контракт соответствует формальной спецификации, предлагая более сильные гарантии, чем обычное тестирование, для свойств, включенных в эту спецификацию.

Та же документация Ethereum указывает на важное ограничение, стоящее за комментариями Бутерина. Доказательство устанавливает, что программное обеспечение удовлетворяет проверяемой спецификации; оно не доказывает автоматически, что разработчики правильно определили все свойства безопасности. Неудачно выбранные или неполные спецификации могут оставить поведение за пределами доказательства.

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

Бутерин уже описывал формальную верификацию с помощью ИИ как возможную «конечную форму» разработки программного обеспечения. Его более ранние комментарии применяли этот подход к таким областям, как консенсус Ethereum, системы с нулевым разглашением и квантово-устойчивая криптография.

Ethereum уже тестирует безопасность с помощью ИИ

Исследователи Ethereum уже используют ИИ в работе по безопасности, хотя текущие системы все еще далеки от автоматического доказательства безопасности всей системы.

Команда безопасности протокола Ethereum Foundation сообщила в июле, что скоординированные агенты ИИ обнаружили реальные дефекты в системах, используемых Ethereum. Одно подтвержденное обнаружение касалось удаленно вызываемого сбоя в сетевой реализации Gossipsub в Rust libp2p.

Эта уязвимость получила идентификатор CVE-2026-34219. Запись в Национальной базе данных уязвимостей США гласит, что версии до 0.49.4 могли быть удаленно аварийно завершены с помощью специально созданного сообщения PRUNE, которое вызывало арифметическое переполнение при обработке отката Gossipsub. Версия 0.49.4 исправила эту проблему.

Команда безопасности Фонда заявила, что обнаружение уязвимостей было не самой сложной частью рабочего процесса ИИ. Исследователи обнаружили, что агенты ИИ часто генерировали убедительные отчеты, включающие недостижимые пути выполнения, сбои, проявляющиеся только при отладке, или формальные доказательства, которые технически проходили, но доказывали более слабое свойство, чем предполагалось.

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

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

Формальная верификация входит в дорожную карту протокола Ethereum

Ethereum Foundation отдельно сделал формальную верификацию частью своей текущей программы исследований протокола. В своем обновлении приоритетов протокола от 7 сентября Фонд заявил, что формальная верификация будет служить сквозным инструментарием в его оставшихся многолетних областях исследований. Документ охватывает работу над конфиденциальностью, состоянием, разработкой zkEVM, постквантовой безопасностью и другими компонентами протокола до 2029 года.

В той же дорожной карте говорится, что разработка L1 zkEVM, как ожидается, продвинет инструменты формальной верификации, рабочие процессы и проверенные криптографические компоненты. Исследователи Ethereum работают над системой, в которой валидаторы в конечном итоге проверяют краткие доказательства выполнения, а не независимо повторно выполняют каждый блок.

Отдельный проект Ethereum Foundation, запущенный в августе, уже сочетает агентов ИИ с машинно-проверяемыми доказательствами. Проект better.codes позволяет исследователям направлять системы ИИ на задачу криптографической надежности, формализованную в Lean, в то время как ядро Lean проверяет, удовлетворяют ли представленные доказательства фиксированной формулировке теоремы.

Отчет Фонда о финансировании за второй квартал перечисляет дальнейшую работу, сочетающую большие языковые модели с формальными методами. Проекты включают ETHeorem для проверки реализаций клиентов Ethereum на соответствие спецификациям, SPECA и LeanAgent для автоматизированной работы по соблюдению протокола, а также формальную верификацию, связанную с инфраструктурой RISC-V zkVM.

Обновленная техническая дорожная карта Ethereum отводит формальной верификации роль наряду с конфиденциальностью, доказательствами с нулевым разглашением и постквантовой защитой. Таким образом, комментарии Бутерина от 17 сентября продолжают существующее направление исследований, а не объявляют о новом обновлении или запланированном форке. Его пост не называл новый EIP, дату развертывания или обязательное правило, требующее, чтобы каждая программа Ethereum проходила формальную верификацию.

Текущие данные об ИИ показывают и более сильные наступательные возможности

Недавние исследования в области кибербезопасности подтверждают опасения, что ИИ делает злоумышленников более способными, даже несмотря на расширение использования в обороне. Anthropic заявила в своем сентябрьском отчете об анализе угроз, что наблюдала, как злоумышленники используют ИИ для автоматизации исследования уязвимостей, разработки эксплойтов и кампаний с несколькими целями. Компания сообщила, что некоторые операторы поддерживали автоматизированные рабочие процессы, которые могли непрерывно проводить исследование уязвимостей.

Более раннее исследование Anthropic обнаружило аналогичные свидетельства в большом масштабе. Ее панель скоординированного раскрытия информации показала, что к 26 августа компания раскрыла 2300 уязвимостей, обнаруженных ИИ, в 392 проектах с открытым исходным кодом, из которых 421 была исправлена в апстриме на тот момент.

Anthropic описывала ту же технологию как полезную для обороны. Ее инициатива Project Glasswing сообщила об использовании передовых моделей совместно с компаниями по безопасности и поставщиками программного обеспечения для обнаружения недостатков высокой и критической степени серьезности до того, как злоумышленники смогут их использовать.

Наступательная сторона остается измеримой. Июньское исследование Anthropic изучило 832 учетные записи, связанные со злонамеренной киберактивностью, с марта 2025 года по март 2026 года и обнаружило, что субъекты угроз используют ИИ на нескольких этапах киберопераций. Бутерин уже отверг отдельный аргумент о том, что риски безопасности, связанные с ИИ, могут серьезно подорвать доверие к биткоину. Он сказал, что проблемы сетевого уровня часто можно решить с помощью обновлений программного обеспечения и инфраструктуры майнинга, в то время как реальные взломы хэшей биткоина или механизма доказательства работы он назвал крайне маловероятными.

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