Vitalik Buterin: KI könnte die Sicherheit von Kryptowährungen stärken

Vitalik Buterin, Mitbegründer von Ethereum, hat auf die wachsenden Bedenken reagiert, dass KI-gestützte Fehlersuche Entwickler überfordern und kontinuierliche Ausnutzungsmöglichkeiten auf Blockchains schaffen könnte.

Seiner Ansicht nach könnte der Einsatz dieser Technologie in naher Zukunft die Sicherheit von Kryptosystemen tatsächlich erhöhen. Er betont, dass KI-unterstützte formale Verifikation eine der stärksten Verteidigungen gegen Sicherheitslücken in der Krypto- und Internetinfrastruktur werden könnte.

KI könnte die Sicherheit stärken statt sie zu gefährden

Formale Verifikation ist die Praxis, mathematische Beweise über Software zu schreiben, die ein Computer automatisch überprüfen kann, anstatt dass Menschen sie manuell prüfen. Dieses Konzept existiert seit Jahrzehnten, hat sich jedoch nie durchgesetzt, da das manuelle Erstellen solcher Beweise für Softwareentwickler sehr mühsam war.

Buterin erklärt, dass KI diese Gleichung verändert hat. Anstatt dass Entwickler die Beweise selbst schreiben, können sie eine KI bitten, sowohl den Code als auch die begleitenden Beweise zu erstellen. Die Entwickler überprüfen dann lediglich, ob die endgültige Aussage tatsächlich das ist, was sie beweisen wollten.

Er beschreibt ein Szenario, in dem KI-Modelle mächtig genug werden, um automatisch Fehler im bestehenden Code zu finden, und fragt, was das für Systeme bedeuten würde, bei denen ein einziger Fehler den Nutzern alles kosten kann.

Seine Antwort ist, dass eine vollständige formale Verifikation es ermöglicht, mathematisch zu beweisen, dass ein Stück Code genau wie beabsichtigt funktioniert. Eine ausreichend leistungsfähige KI, die nach Fehlern sucht, würde also Code betrachten, der bereits als fehlerfrei bewiesen wurde.

Buterin nennt spezifische Ethereum-Infrastrukturprojekte, bei denen dieser Ansatz bereits versucht wird. Eines davon ist Arklib, das an einer vollständig formal verifizierten STARK-Implementierung arbeitet. Ein weiteres ist evm-asm, das eine EVM in Low-Level-RISC-V-Assembly schreibt und deren Korrektheit gegen eine menschenlesbare Referenzimplementierung überprüft.

Auf die Frage, welche KI-Modelle dafür tatsächlich nützlich sind, sagte Buterin, dass er Claude und Deepseek 4 Pro als ausreichend für das Schreiben von Lean-Beweisen empfindet.

Er hebt auch Leanstral hervor, ein kleineres Modell mit offenen Gewichten, das speziell für Lean feinabgestimmt wurde und lokal ausgeführt werden kann, während es größere allgemeine Modelle bei formalen Verifikationsbenchmarks übertrifft.

Aber es gibt Einschränkungen

Trotz seiner Begeisterung für formale Verifikation widmet Buterin einen erheblichen Teil seines Essays der Erklärung, wie diese in der Praxis versagt hat.

Dies umfasst Fehler in verifizierten Compilern, Bibliotheken, bei denen nur ein Teil des Codes bewiesen wurde und die unbewiesenen Teile das Problem darstellten, sowie Spezifikationen, die technisch bewiesen, aber nicht das erfassten, was der Entwickler tatsächlich garantieren wollte.

Sein allgemeiner Rahmen ist jedoch, dass formale Verifikation kein Ersatz für alle Sicherheitspraktiken ist, sondern ein mächtiges Werkzeug in einem längerfristigen Trend zu weniger Fehlern pro Codezeile.

Der Hintergrund ist relevant, da am Tag von Buterins Beitrag der Kryptosektor von einem dritten großen Exploit innerhalb von nur vier Tagen erschüttert wurde, nachdem ein Hacker mehr als $76 Millionen an Kryptowährungen von der Cross-Chain-Bridge des Echo-Protokolls erbeutete.

Wenige Tage zuvor gab es Berichte über einen Hack auf THORChain, der die Plattform mehr als $10 Millionen kostete.

Ein weiterer Angriff folgte darauf, der die Verus-Ethereum-Bridge betraf, bei dem ein Hacker die fehlende Validierungsprüfung ausnutzte, um $11,58 Millionen zu stehlen. Dies ist die Art von spezifischem, lokalisiertem Fehler, den eine formale Beweisprüfung möglicherweise hätte erkennen können.