Vitalik Buterin weist KI-Cybersicherheits-Untergangsbehauptung zurück

Buterin schrieb in seinem Beitrag vom 17. September auf X, dass er die zunehmend verbreitete Ansicht ablehne, dass „KI-Hacking bedeutet, dass die Cybersicherheit dem Untergang geweiht ist“. Er sagte, dass Menschen, die weiterhin Kryptowährungen halten, implizit darauf wetten, dass sichere digitale Systeme stärkere automatisierte Angriffe überstehen können, und fügte hinzu, dass etwa 90 % seines eigenen Nettovermögens weiterhin in Krypto stecken.

Sein Argument dreht sich um formale Verifikation, eine Technik, die mathematische Spezifikationen und Beweise verwendet, um festzustellen, ob sich Software gemäß vordefinierten Eigenschaften verhält. Buterin verwendete fortgeschrittenes mathematisches Theorembeweisen als Analogie und sagte, dass ausreichend leistungsfähige KI helfen könne zu beweisen, dass „dieses Programm sicher ist“, selbst wenn die Software selbst komplex ist.

Buterin sagt, formale Verifikation kann Verteidiger begünstigen

Buterins Argument behandelt KI-Sicherheit nicht als ein Wettrennen, bei dem defensive Forscher einfach Fehler vor Angreifern finden. Sein Beitrag beschreibt stattdessen ein Modell, bei dem Entwickler die Eigenschaften definieren, die ein System erfüllen muss, und dann automatisierte Beweiswerkzeuge verwenden, um festzustellen, dass die Implementierung diesen gehorcht.

Ethereums eigene Dokumentation zur formalen Verifikation beschreibt die Technik in engeren Begriffen. Sie besagt, dass formale Verifikation mathematisch beweisen kann, dass ein Smart Contract einer formalen Spezifikation entspricht, und bietet stärkere Garantien als gewöhnliche Tests für die in dieser Spezifikation enthaltenen Eigenschaften.

Dieselbe Ethereum-Dokumentation identifiziert eine wichtige Einschränkung hinter Buterins Kommentaren. Ein Beweis stellt fest, dass Software die geprüfte Spezifikation erfüllt; er beweist nicht automatisch, dass Entwickler jede Sicherheitseigenschaft korrekt definiert haben. Schlecht gewählte oder unvollständige Spezifikationen können Verhalten außerhalb des Beweises lassen.

Buterin machte dieselbe Unterscheidung in seinem Beitrag. Er argumentierte, dass eine zu enge Definition von „Sicherheit“ Angriffspfade auslassen kann, die Bereiche wie Protokolle, Server, Datenbanken, Netzwerkschichten, Caches oder andere unterstützende Komponenten betreffen. Seine vorgeschlagene Richtung ist daher, mehr vom gesamten System zu verifizieren, anstatt eine kleine Gruppe von Modulen als sicherheitskritisch zu kennzeichnen.

Buterin hatte KI-unterstützte formale Verifikation bereits als mögliche „Endform“ der Softwareentwicklung beschrieben. Seine früheren Kommentare wandten den Ansatz auf Bereiche wie Ethereum-Konsens, Zero-Knowledge-Systeme und quantenresistente Kryptographie an.

Ethereum testet bereits KI-unterstützte Sicherheit

Ethereum-Forscher verwenden KI bereits in der Sicherheitsarbeit, obwohl aktuelle Systeme noch weit von einem automatischen Beweis der Gesamtsystemsicherheit entfernt sind.

Das Protocol-Security-Team der Ethereum Foundation berichtete im Juli, dass koordinierte KI-Agenten echte Fehler in von Ethereum verwendeten Systemen gefunden hatten. Ein bestätigter Fund betraf einen aus der Ferne erreichbaren Absturz in der Gossipsub-Netzwerkimplementierung von Rust libp2p.

Der Fehler wurde zu CVE-2026-34219. Der Datensatz der U.S. National Vulnerability Database besagt, dass Versionen vor 0.49.4 aus der Ferne durch eine manipulierte PRUNE-Nachricht zum Absturz gebracht werden konnten, die einen arithmetischen Überlauf während der Gossipsub-Backoff-Behandlung auslöste. Version 0.49.4 behob das Problem.

Das Sicherheitsteam der Foundation sagte, dass die Entdeckung von Schwachstellen nicht der schwierigste Teil des KI-Workflows war. Forscher stellten fest, dass KI-Agenten häufig überzeugende Berichte über unerreichbare Ausführungspfade, nur im Debug-Modus auftretende Fehler oder formale Beweise erzeugten, die technisch bestanden, aber eine schwächere Eigenschaft als beabsichtigt bewiesen.

Unabhängige Reproduktion blieb eine Anforderung, bevor das Team einen Fund akzeptierte. Die Foundation sagte, dass automatisierte Prüfungen und menschliche Überprüfung erforderlich seien, weil ein Agent einen gültig aussehenden Beweis erzeugen könne, der das Softwareverhalten, das Forscher tatsächlich testen wollten, nicht einschränkte.

Die Erfahrung der Foundation wurde als Triage-Problem beschrieben: KI konnte eine große Anzahl von Kandidaten-Schwachstellen erzeugen, aber Forscher mussten immer noch feststellen, ob jedes Problem in der Produktion erreichbar und bedeutsam war.

Formale Verifikation hält Einzug in Ethereums Protokoll-Roadmap

Die Ethereum Foundation hat formale Verifikation separat zu einem Teil ihres aktuellen Protokollforschungsprogramms gemacht. In ihrem Update zu den Protokollprioritäten vom 7. September sagte die Foundation, dass formale Verifikation als querschnittliches Werkzeug in ihren verbleibenden mehrjährigen Forschungsbereichen dienen werde. Das Dokument deckt Arbeiten zu Datenschutz, Zustand, zkEVM-Entwicklung, Post-Quanten-Sicherheit und anderen Protokollkomponenten bis 2029 ab.

Dieselbe Roadmap besagt, dass die Entwicklung eines L1-zkEVM voraussichtlich formale Verifikationswerkzeuge, Workflows und verifizierte kryptographische Komponenten voranbringen wird. Ethereum-Forscher arbeiten auf ein System hin, in dem Validierer schließlich kompakte Ausführungsbeweise verifizieren, anstatt jeden Block unabhängig erneut auszuführen.

Ein separates Projekt der Ethereum Foundation, das im August gestartet wurde, kombiniert bereits KI-Agenten mit maschinengeprüften Beweisen. Das Projekt better.codes ermöglicht es Forschern, KI-Systeme auf ein in Lean formalisiertes kryptographisches Korrektheitsproblem anzusetzen, während der Lean-Kernel prüft, ob eingereichte Beweise eine feste Theoremaussage erfüllen.

Der Finanzierungsbericht der Foundation für das zweite Quartal listet weitere Arbeiten auf, die große Sprachmodelle mit formalen Methoden kombinieren. Projekte umfassen ETHeorem zur Prüfung von Ethereum-Client-Implementierungen gegen Spezifikationen, SPECA und LeanAgent für automatisierte Protokollkonformitätsarbeit sowie formale Verifikation im Zusammenhang mit RISC-V-zkVM-Infrastruktur.

Ethereums aktualisierte technische Roadmap gibt der formalen Verifikation eine Rolle neben Datenschutz, Zero-Knowledge-Beweisen und Post-Quanten-Schutz. Buterins Kommentare vom 17. September setzen daher eine bestehende Forschungsrichtung fort, anstatt ein neues Upgrade oder einen geplanten Fork anzukündigen. Sein Beitrag nannte kein neues EIP, kein Bereitstellungsdatum und keine verbindliche Regel, die vorschreibt, dass jedes Ethereum-Programm einer formalen Verifikation unterzogen werden muss.

Aktuelle KI-Beweise zeigen auch stärkere offensive Fähigkeiten

Jüngste Cybersicherheitsforschung stützt die Besorgnis, dass KI Angreifer leistungsfähiger macht, selbst wenn die defensive Nutzung zunimmt. Anthropic sagte in seinem Threat-Intelligence-Bericht vom September, dass es böswillige Akteure beobachtet habe, die KI zur Automatisierung von Schwachstellenforschung, Exploit-Entwicklung und Multi-Target-Kampagnen einsetzen. Das Unternehmen sagte, dass einige Betreiber automatisierte Workflows unterhielten, die kontinuierlich Schwachstellenforschung betreiben könnten.

Frühere Forschung von Anthropic fand ähnliche Belege in großem Maßstab. Das Dashboard für koordinierte Offenlegung besagte, dass das Unternehmen bis zum 26. August 2.300 KI-entdeckte Schwachstellen in 392 Open-Source-Projekten offengelegt hatte, von denen zu diesem Zeitpunkt 421 upstream gepatcht waren.

Anthropic hat dieselbe Technologie als nützlich für die Verteidigung beschrieben. Die Initiative Project Glasswing berichtete, Frontier-Modelle mit Sicherheitsunternehmen und Softwareanbietern einzusetzen, um Schwachstellen mit hohem und kritischem Schweregrad zu finden, bevor böswillige Akteure sie ausnutzen können.

Die offensive Seite bleibt messbar. Anthropics Studie vom Juni untersuchte 832 Konten, die mit böswilliger Cyberaktivität von März 2025 bis März 2026 in Verbindung stehen, und stellte fest, dass Bedrohungsakteure KI in mehreren Phasen von Cyberoperationen einsetzen. Buterin hatte bereits ein separates Argument zurückgewiesen, dass KI-bedingte Sicherheitsrisiken das Vertrauen in Bitcoin schwer beschädigen könnten. Er sagte, dass Probleme auf Netzwerkebene oft durch Software- und Mining-Infrastruktur-Upgrades behoben werden könnten, während er tatsächliche Brüche von Bitcoins Hashes oder des Proof-of-Work-Mechanismus als höchst unwahrscheinlich bezeichnete.

Anthropics September-Bericht besagte, dass seine Ermittler Betreiber identifiziert hatten, die KI-gebaute Exploit-Pipelines gegen Sicherheits-Appliances und Regierungsziele einsetzten, wobei einige Kampagnen zuvor unbekannte Schwachstellen hervorbrachten, die Angreifer in ihren eigenen Testumgebungen validierten.