KI-gestützte formale Verifikation und Ethereum-Sicherheit

Vitalik Buterin wies in seinem Beitrag vom 17. September die Auffassung zurück, dass leistungsfähigere KI-Angreifer die Cybersicherheit grundlegend zerstören würden. Sein Kernargument verbindet die Geschwindigkeit der KI-Codegenerierung mit formaler Verifikation: mathematische Spezifikationen und mechanisch geprüfte Beweise, die zeigen können, dass eine Implementierung definierte Sicherheits-Eigenschaften erfüllt. Er stellte dies nicht als reines Wettrennen dar, bei dem Verteidiger Fehler schneller finden als Angreifer, sondern als strukturellen Ansatz, der Verteidigern einen Vorteil verschaffen kann, wenn er breit angenommen wird. Er erwähnte außerdem, dass rund 90 % seines Nettovermögens in Krypto gehalten werden, was sein Interesse an robusten Systemen persönlicher macht.

Buterin nannte konkrete Bereiche, in denen KI-unterstützte formale Methoden für Ethereum bedeutend sind: Konsens, Zero-Knowledge-Systeme und post-quantenresistente Kryptographie. Er verwies auf Theorembeweiser wie Lean und hob Projekte wie Arklib (eine formal verifizierte STARK-Implementierung) sowie evm-asm hervor, das die EVM formaler Analyse zugänglicher machen soll. Die Ethereum Foundation hat formale Verifikation in ihren Protokoll-Forschungsfahrplan aufgenommen: ein Update vom 7. September beschreibt Verifikation als bereichsübergreifendes Werkzeug für mehrjährige Forschungsfelder bis 2029 und erwartet, dass die Entwicklung einer L1 zkEVM verifizierte kryptographische Komponenten und Verifikations-Workflows voranbringt.

Die praktische Erfahrung ist ambivalent, aber lehrreich. Das Sicherheitsteam der Foundation berichtete, dass koordinierte KI-Agenten reale Fehler fanden, darunter einen fernaufrufbaren Absturz in Rust libp2p’s Gossipsub, der als CVE-2026-34219 aufgeführt wurde; Versionen vor 0.49.4 konnten durch eine manipulierte PRUNE-Nachricht zum Überlauf und Absturz gebracht werden, Version 0.49.4 behebt den Fehler. Zugleich stellten Forschende fest, dass Agenten oft überzeugende, aber irreführende Berichte erzeugen: unerreichbare Ausführungspfade, nur für Debugging relevante Fehler oder Beweise, die technisch akzeptabel sind, aber eine schwächere Eigenschaft nachweisen als gewollt. Das führte zu einem Triage-Problem, sodass unabhängige Reproduktionen, automatisierte Prüfungen und menschliche Begutachtung weiterhin erforderlich sind.

Parallel zu den Fortschritten der Verteidigung sind offensive Fähigkeiten messbar gewachsen. Anthropic berichtete, dass Frontier-Modelle die Entdeckung von Schwachstellen im großen Maßstab beschleunigten: Bis zum 26. August listete das koordinierte Disclosure-Dashboard 2.300 von KI entdeckte Schwachstellen in 392 Open-Source-Projekten, von denen 421 upstream gepatcht wurden. In weiteren Untersuchungen identifizierte Anthropic Akteure, die KI-gestützte Exploit-Pipelines über mehrere Phasen von Kampagnen einsetzen und dabei hunderte bis tausende Schwachstellen validierten.

Buterin erkannte zwei zentrale Einschränkungen an: Spezifikationsrisiko — ein Beweis garantiert nur, dass die Spezifikation erfüllt ist, und wenn die Spezifikation kritische Eigenschaften auslässt, ist der Beweis hohl — und Hardwarerisiko, da Prozessoren und physische Plattformen nicht mit derselben mathematischen Gewissheit wie Software verifiziert werden können. Die Ethereum-Forschung kombiniert dennoch KI mit maschinengeprüften Beweisen in Projekten wie better.codes, ETHeorem, SPECA, LeanAgent und RISC‑V zkVM-Verifikationsarbeiten. Dies unterstreicht eine Forschungsstrategie, die formale Verifikation als essentielles Werkzeug begreift, nicht als einmaligen Patch. Buterins Beitrag vom 17. September fasst daher eine bestehende Richtung zusammen: KI verstärkt sowohl offensive als auch defensive Fähigkeiten, doch gekoppelt mit rigorosen formalen Methoden kann sie Verteidigern ermöglichen, Systeme zu bauen, die auch gegen zunehmend automatisierte Angriffe widerstandsfähig bleiben.