Виталик Бутерин отверг утверждение, что всё более способные ИИ-хакеры сделают кибербезопасность фактически безнадёжной, заявив 17 сентября, что передовые инструменты верификации в конечном итоге могут дать защитникам структурное преимущество.
Краткое содержание
- 90% собственного капитала Бутерина остаётся в криптовалюте, согласно его заявлению от 17 сентября.
- Формальная верификация с помощью ИИ может помочь доказать, что программное обеспечение удовлетворяет заданным свойствам безопасности, согласно аргументу Бутерина.
- Команда безопасности Ethereum уже использует ИИ-агентов для проверки кода протокола и независимого воспроизведения уязвимостей.
- Исследователи Ethereum теперь рассматривают формальную верификацию как сквозной инструмент в нескольких долгосрочных направлениях исследования протокола.
- Anthropic заявляет, что передовой ИИ может ускорять атаки, в то время как её модели выявили тысячи уязвимостей.
Бутерин написал в своём посте от 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 отдельно сделал формальную верификацию частью своей текущей программы исследований протокола. В обновлении приоритетов протокола от 7 сентября Фонд заявил, что формальная верификация будет служить сквозным инструментом во всех его оставшихся многолетних исследовательских областях. Документ охватывает работу над конфиденциальностью, состоянием, разработкой zkEVM, постквантовой безопасностью и другими компонентами протокола до 2029 года.
Та же дорожная карта говорит, что разработка L1 zkEVM, как ожидается, продвинет инструменты формальной верификации, рабочие процессы и верифицированные криптографические компоненты. Исследователи Ethereum работают над системой, в которой валидаторы в конечном итоге проверяют сжатые доказательства выполнения вместо независимого повторного выполнения каждого блока.
Отдельный проект Фонда Ethereum, запущенный в августе, уже объединяет ИИ-агентов с машинно-проверяемыми доказательствами. Проект better.codes позволяет исследователям направлять ИИ-системы на проблему криптографической надёжности, формализованную в Lean, в то время как ядро Lean проверяет, удовлетворяют ли представленные доказательства фиксированной формулировке теоремы.
Отчёт Фонда о финансировании за второй квартал перечисляет дальнейшую работу, объединяющую большие языковые модели с формальными методами. Проекты включают ETHeorem для проверки реализаций клиентов Ethereum на соответствие спецификациям, SPECA и LeanAgent для автоматизированной работы по соблюдению протокола, а также формальную верификацию, связанную с инфраструктурой RISC-V zkVM.
Обновлённая техническая дорожная карта Ethereum отводит формальной верификации роль наряду с конфиденциальностью, доказательствами с нулевым разглашением и постквантовой защитой. Таким образом, комментарии Бутерина от 17 сентября продолжают существующее направление исследований, а не объявляют новое обновление или запланированный форк. В его посте не назван новый EIP, дата развёртывания или обязательное правило, требующее, чтобы каждая программа Ethereum проходила формальную верификацию.
Текущие данные об ИИ показывают и более сильные наступательные возможности
Недавние исследования в области кибербезопасности подтверждают опасения, что ИИ делает атакующих более способными, даже по мере расширения оборонительного использования. Anthropic заявила в своём сентябрьском отчёте о киберугрозах report, что наблюдала злоумышленников, использующих ИИ для автоматизации исследования уязвимостей, разработки эксплойтов и кампаний против множества целей. Компания заявила, что некоторые операторы поддерживали автоматизированные рабочие процессы, которые могли проводить исследование уязвимостей непрерывно.
Более раннее исследование Anthropic обнаружило аналогичные доказательства в масштабе. В её панели скоординированного раскрытия информации говорится, что по состоянию на 26 августа компания раскрыла 2300 уязвимостей, обнаруженных ИИ, в 392 проектах с открытым исходным кодом, при этом 421 была исправлена в upstream на тот момент.
Anthropic описывала ту же технологию как полезную для защиты. Её инициатива Project Glasswing сообщила об использовании передовых моделей совместно с компаниями по безопасности и поставщиками программного обеспечения для поиска уязвимостей высокой и критической степени серьёзности до того, как злоумышленники смогли бы их эксплуатировать.
Наступательная сторона остается измеримой. Июньское исследование Anthropic изучило 832 аккаунта, связанных с вредоносной кибердеятельностью, с марта 2025 года по март 2026 года, и обнаружило, что субъекты угроз используют ИИ на нескольких этапах киберопераций. Бутерин уже отверг отдельный аргумент о том, что риски безопасности, движимые ИИ, могут серьезно подорвать доверие к Bitcoin. Он сказал, что проблемы сетевого уровня часто можно решить с помощью обновлений программного обеспечения и инфраструктуры майнинга, при этом описав реальные взломы хешей Bitcoin или механизма proof-of-work как крайне маловероятные.
В сентябрьском отчете Anthropic говорилось, что его следователи выявили операторов, использующих созданные с помощью ИИ конвейеры эксплойтов против устройств безопасности и правительственных целей, причем некоторые кампании приводили к появлению ранее неизвестных уязвимостей, которые злоумышленники проверяли в своих собственных тестовых средах.
