Vitalik Buterin odrzucił twierdzenie, że coraz bardziej zdolni hakerzy AI sprawią, iż cyberbezpieczeństwo stanie się praktycznie nie do wygrania, argumentując 17 września, że zaawansowane narzędzia weryfikacji mogą ostatecznie dać obrońcom przewagę strukturalną.
Podsumowanie
- 90% majątku netto Buterina pozostaje w kryptowalutach, zgodnie z jego własnym oświadczeniem z 17 września.
- Wspomagana przez AI weryfikacja formalna mogłaby pomóc udowodnić, że oprogramowanie spełnia zdefiniowane właściwości bezpieczeństwa, zgodnie z argumentacją Buterina.
- Zespół ds. bezpieczeństwa Ethereum już wykorzystuje agentów AI do inspekcji kodu protokołu i niezależnego odtwarzania podatności.
- Badacze Ethereum traktują obecnie weryfikację formalną jako narzędzie przekrojowe w kilku długoterminowych ścieżkach badawczych nad protokołem.
- Anthropic twierdzi, że frontier AI może przyspieszać ataki, podczas gdy jego modele zidentyfikowały tysiące błędów.
Buterin napisał w swoim poście na X z 17 września, że nie zgadza się z coraz powszechniejszym poglądem, iż „haking za pomocą AI oznacza, że cyberbezpieczeństwo jest skazane na porażkę”. Powiedział, że osoby, które nadal posiadają kryptowaluty, domyślnie zakładają, że bezpieczne systemy cyfrowe mogą przetrwać silniejsze zautomatyzowane ataki, dodając, że około 90% jego własnego majątku netto pozostaje w kryptowalutach.
Jego argumentacja koncentruje się na weryfikacji formalnej, technice wykorzystującej matematyczne specyfikacje i dowody do ustalenia, czy oprogramowanie zachowuje się zgodnie z predefiniowanymi właściwościami. Buterin użył zaawansowanego dowodzenia twierdzeń matematycznych jako analogii, mówiąc, że wystarczająco zdolna AI mogłaby pomóc udowodnić, że „ten program jest bezpieczny”, nawet gdy samo oprogramowanie jest złożone.
Buterin twierdzi, że weryfikacja formalna może faworyzować obrońców
Argumentacja Buterina nie traktuje bezpieczeństwa AI jako wyścigu, w którym badacze po stronie obrony po prostu znajdują błędy przed atakującymi. Jego post opisuje natomiast model, w którym deweloperzy definiują właściwości, które system musi spełniać, a następnie używają zautomatyzowanych narzędzi dowodowych, aby ustalić, że implementacja jest z nimi zgodna.
Własna dokumentacja weryfikacji formalnej Ethereum opisuje tę technikę w węższych kategoriach. Mówi, że weryfikacja formalna może matematycznie udowodnić, że inteligentny kontrakt jest zgodny z formalną specyfikacją, oferując silniejsze gwarancje niż zwykłe testowanie dla właściwości zawartych w tej specyfikacji.
Ta sama dokumentacja Ethereum wskazuje na ważne ograniczenie leżące u podstaw komentarzy Buterina. Dowód ustala, że oprogramowanie spełnia sprawdzaną specyfikację; nie dowodzi automatycznie, że deweloperzy poprawnie zdefiniowali każdą właściwość bezpieczeństwa. Źle wybrane lub niekompletne specyfikacje mogą pozostawić zachowanie poza dowodem.
Buterin dokonał tego samego rozróżnienia w swoim poście. Argumentował, że zbyt wąskie zdefiniowanie „bezpieczeństwa” może pominąć ścieżki ataku obejmujące obszary takie jak protokoły, serwery, bazy danych, warstwy sieciowe, pamięci podręczne lub inne komponenty wspierające. Jego proponowany kierunek polega zatem na weryfikacji większej części całego systemu, zamiast oznaczania małej grupy modułów jako krytycznych dla bezpieczeństwa.
Buterin już wcześniej opisał wspomaganą przez AI weryfikację formalną jako możliwą „ostateczną formę” tworzenia oprogramowania. Jego wcześniejsze komentarze stosowały to podejście do obszarów takich jak konsensus Ethereum, systemy zero-knowledge i kryptografia odporna na komputery kwantowe.
Ethereum już testuje bezpieczeństwo wspomagane przez AI
Badacze Ethereum już wykorzystują AI w pracy nad bezpieczeństwem, choć obecne systemy są wciąż dalekie od automatycznego dowodu bezpieczeństwa całego systemu.
Zespół ds. bezpieczeństwa protokołu Ethereum Foundation poinformował w lipcu, że skoordynowane agenty AI znalazły rzeczywiste defekty w systemach używanych przez Ethereum. Jedno potwierdzone odkrycie dotyczyło zdalnie osiągalnej awarii w implementacji sieciowej Gossipsub w Rust libp2p.
Ta luka stała się CVE-2026-34219. Wpis w amerykańskiej Narodowej Bazie Danych Podatności mówi, że wersje przed 0.49.4 mogły być zdalnie zawieszane przez spreparowaną wiadomość PRUNE, która wywoływała przepełnienie arytmetyczne podczas obsługi backoffu Gossipsub. Wersja 0.49.4 naprawiła ten problem.
Zespół ds. bezpieczeństwa Fundacji powiedział, że wykrycie podatności nie było najtrudniejszą częścią przepływu pracy AI. Badacze odkryli, że agenci AI często generowali przekonujące raporty dotyczące nieosiągalnych ścieżek wykonania, awarii występujących tylko w trybie debugowania lub formalnych dowodów, które technicznie przechodziły, dowodząc słabszej właściwości niż zamierzano.
Niezależne odtworzenie pozostawało wymogiem, zanim zespół zaakceptował zgłoszenie. Fundacja stwierdziła, że potrzebne były automatyczne kontrole i przegląd ludzki, ponieważ agent mógł wygenerować wyglądający na poprawny dowód, który nie ograniczał zachowania oprogramowania, które badacze faktycznie chcieli przetestować.
Doświadczenie Fundacji zostało opisane jako problem segregacji: AI mogło generować duże liczby kandydatów na podatności, ale badacze nadal musieli ustalić, czy każdy problem był osiągalny i istotny w środowisku produkcyjnym.
Weryfikacja formalna wchodzi do planu rozwoju protokołu Ethereum
Fundacja Ethereum osobno uczyniła weryfikację formalną częścią swojego obecnego programu badawczego nad protokołem. W swoim aktualizacji priorytetów protokołu z 7 września Fundacja stwierdziła, że weryfikacja formalna będzie służyć jako narzędzie przekrojowe we wszystkich pozostałych wieloletnich obszarach badawczych. Dokument obejmuje prace nad prywatnością, stanem, rozwojem zkEVM, bezpieczeństwem postkwantowym i innymi komponentami protokołu do 2029 roku.
Ten sam plan rozwoju mówi, że rozwój zkEVM warstwy L1 ma przyczynić się do postępu w narzędziach weryfikacji formalnej, przepływach pracy i zweryfikowanych komponentach kryptograficznych. Badacze Ethereum pracują nad systemem, w którym walidatorzy ostatecznie weryfikują zwięzłe dowody wykonania zamiast niezależnie ponownie wykonywać każdy blok.
Osobny projekt Fundacji Ethereum uruchomiony w sierpniu już łączy agentów AI z dowodami sprawdzanymi maszynowo. Projekt better.codes pozwala badaczom kierować systemy AI na problem poprawności kryptograficznej sformalizowany w Lean, podczas gdy jądro Lean sprawdza, czy przesłane dowody spełniają ustalone twierdzenie.
Raport finansowania Fundacji za drugi kwartał wymienia dalsze prace łączące duże modele językowe z metodami formalnymi. Projekty obejmują ETHeorem do sprawdzania implementacji klientów Ethereum względem specyfikacji, SPECA i LeanAgent do zautomatyzowanych prac nad zgodnością z protokołem oraz weryfikację formalną obejmującą infrastrukturę RISC-V zkVM.
Zaktualizowany plan techniczny Ethereum przypisuje weryfikacji formalnej rolę obok prywatności, dowodów zerowej wiedzy i ochrony postkwantowej. Komentarze Buterina z 17 września kontynuują zatem istniejący kierunek badawczy, a nie ogłaszają nową aktualizację ani zaplanowany fork. Jego wpis nie wymienia nowego EIP, daty wdrożenia ani obowiązkowej reguły wymagającej, aby każdy program Ethereum przechodził weryfikację formalną.
Obecne dowody dotyczące AI pokazują również silniejsze zdolności ofensywne
Najnowsze badania w dziedzinie cyberbezpieczeństwa potwierdzają obawę, że AI zwiększa zdolności atakujących, nawet gdy zastosowania defensywne się rozszerzają. Anthropic powiedział w swoimraporcie wywiadu zagrożeń z września report, że zaobserwował złośliwych aktorów wykorzystujących AI do automatyzacji badań nad podatnościami, tworzenia exploitów i kampanii wielocelowych. Firma stwierdziła, że niektórzy operatorzy utrzymywali zautomatyzowane przepływy pracy, które mogły prowadzić badania nad podatnościami w sposób ciągły.
Wcześniejsze badania Anthropic znalazły podobne dowody na dużą skalę. Jej panel skoordynowanego ujawniania podał, że do 26 sierpnia firma ujawniła 2300 podatności odkrytych przez AI w 392 projektach open source, z czego 421 zostało w tym momencie załatanych w projektach źródłowych.
Anthropic opisał tę samą technologię jako użyteczną do obrony. Jej inicjatywa Project Glasswing poinformowała o wykorzystaniu modeli frontier wraz z firmami zajmującymi się bezpieczeństwem i dostawcami oprogramowania do lokalizowania luk o wysokiej i krytycznej wadze, zanim złośliwi aktorzy mogliby je wykorzystać.
Strona ofensywna pozostaje mierzalna. Czerwcowe badanie Anthropic przeanalizowało 832 kont powiązanych ze złośliwą aktywnością cybernetyczną od marca 2025 do marca 2026 roku i wykazało, że aktorzy zagrożeń wykorzystują AI na wielu etapach operacji cybernetycznych. Buterin odrzucił już osobny argument, że ryzyka bezpieczeństwa napędzane przez AI mogą poważnie zaszkodzić zaufaniu do Bitcoina. Powiedział, że problemy na poziomie sieci często można rozwiązać poprzez aktualizacje oprogramowania i infrastruktury wydobywczej, jednocześnie opisując rzeczywiste złamanie hashy Bitcoina lub mechanizmu proof-of-work jako wysoce nieprawdopodobne.
Wrześniowy raport Anthropic stwierdził, że jego śledczy zidentyfikowali operatorów wykorzystujących zbudowane przez AI potoki exploitów przeciwko urządzeniom bezpieczeństwa i celom rządowym, przy czym niektóre kampanie generowały wcześniej nieznane luki w zabezpieczeniach, które atakujący walidowali we własnych środowiskach testowych.
