Виталик Бутерин: ИИ не уничтожит кибербезопасность, а поможет защитить криптовалюты

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

В новом посте в соцсети Бутерин связал этот прогноз со своими собственными деньгами. По его словам, около 90% его состояния находится в криптовалюте, поэтому, продолжая хранить цифровые активы, он сам делает ставку на то, что криптографические системы смогут выдержать новую эпоху автоматизированных атак.

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

Эту концепцию Бутерин разбирал ещё 18 мая 2026 года. Тогда он писал, что подобный подход уже набирает популярность среди исследователей Ethereum: код создаётся на низкоуровневых языках либо в Lean, после чего его корректность подтверждается автоматически проверяемыми математическими доказательствами.

Однако здесь начинается самое сложное. Доказать, что программа безопасна, можно только после того, как разработчики точно определили, что вообще означает безопасность.

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

Кроме того, содержимое сообщения может оставаться зашифрованным, но злоумышленник всё ещё способен получить метаданные: кто с кем общается, когда отправляются сообщения и с какими временными интервалами. Поэтому математическое определение слова «безопасность» само по себе может оказаться огромным и сложным документом.

И здесь Бутерин видит одну из главных задач разработчиков — сформулировать определение безопасности, которое будет одновременно достаточно полным для машинной проверки и понятным человеку.

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

Бутерин называет требования безопасности «аддитивными». Если одна команда считает важным условие A, а другая — условие B, разработчики могут доказать соответствие программы обоим условиям. С кодом всё работает иначе: достаточно одной критической ошибки в компоненте A или B, чтобы поставить под угрозу всю систему.

Ранее Бутерин подчёркивал, что формальная верификация особенно полезна там, где конечное требование значительно проще самой реализации. К таким областям он относит технологии, которые будут играть важную роль в дальнейшем развитии Ethereum: квантово-устойчивые подписи, STARK, алгоритмы консенсуса и ZK-EVM.

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

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