Віталік Бутерін відкинув твердження, що дедалі потужніші ШІ-хакери зроблять кібербезпеку фактично безнадійною, заявивши 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 року.
Та сама дорожня карта зазначає, що розробка zkEVM рівня L1, як очікується, сприятиме розвитку інструментів формальної верифікації, робочих процесів і верифікованих криптографічних компонентів. Дослідники 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 йдеться про те, що його слідчі виявили операторів, які використовують створені ШІ конвеєри експлойтів проти пристроїв безпеки та урядових цілей, причому деякі кампанії створювали раніше невідомі вразливості, які атакувальники перевіряли у власних тестових середовищах.
