Buterin: Formale Verifikation mit KI könnte Sicherheits-Wettrüste

Vitalik Buterin hält die KI-gestützte formale Verifikation von Code für den entscheidenden Hebel, um die Sicherheitsrisiken zu neutralisieren, die Künstliche Intelligenz selbst schafft. In einem Blogbeitrag vom 18. Mai argumentiert der Ethereum-Mitgründer, dass dieser Ansatz Software hervorbringen könne, die robuster sei als rein menschlich geschriebener Code – und das ohne die Abhängigkeit von zentralisierten Prüfinstanzen.

Buterin reagiert damit direkt auf die wachsende Skepsis in der Krypto-Szene: Wenn KI das Auffinden von Sicherheitslücken automatisiert, ließe sich vertrauenswürdiger Code nur noch mit gigantischen Kontrollapparaten realisieren. Der Kern seiner Gegenthese: Das Problem sei temporär, nicht strukturell. Das langfristige Gleichgewicht, so Buterin, werde „günstiger für den Verteidiger sein, als wir es vorher hatten“.

Wie formale Verifikation funktioniert

Das Prinzip ist ebenso elegant wie anspruchsvoll: Ein KI-Modell schreibt Code in maschinennaher Assemblersprache, optimiert auf Geschwindigkeit. Gleichzeitig generiert es einen mathematischen Beweis, der die Übereinstimmung dieses Low-Level-Codes mit einer für Menschen lesbaren High-Level-Version belegt. Der Nutzer prüft diesen Beweis einmalig und kann anschließend die performante Version ausführen, ohne den Code selbst auditieren zu müssen.

Buterin verweist auf konkrete Projekte im Ethereum-Ökosystem, die diesen Ansatz bereits umsetzen: darunter evm-asm, eine formal verifizierte Implementation der Ethereum Virtual Machine (EVM) in Assembler, sowie Arklib, ein System für verifizierte STARK-Beweise. Die Stärke liege in der Ende-zu-Ende-Abdeckung: Fehler an Schnittstellen zwischen Subsystemen, eine klassische Fehlerquelle, würden eliminiert.

Die Grenzen des Ansatzes

Allerdings räumt Buterin selbst ein, dass formale Verifikation kein Allheilmittel ist. Sie beweist lediglich, dass der Code mathematische Eigenschaften erfüllt, die der Entwickler spezifiziert hat. Sind die Spezifikationen unvollständig, bleibt der Fehler unsichtbar. Auch Hardware-Angriffe wie Seitenkanalattacken per Stromverbrauchsanalyse lassen sich so nicht abdecken.

Dass KI-gestützte Angriffe real sind, zeigte sich erst kürzlich: Im Mai dokumentierte Googles Threat Intelligence Group den mutmaßlich ersten Zero-Day-Exploit, der mit Assistenz eines Sprachmodells entwickelt wurde. Im Februar verlor das DeFi-Protokoll Moonwell 1,7 Millionen US-Dollar, weil ein KI-generierter Smart Contract einen Token-Preis massiv falsch berechnete – und alle menschlichen Reviews passierte.

Zwei Diagnosen, ein Phänomen

Charles Guillemet, CTO des Hardware-Wallet-Herstellers Ledger, sieht die aktuellen Entwicklungen mit Sorge. KI senke die Einstiegshürde für Angreifer massiv: Aus einem Binärunterschied einen funktionsfähigen Exploit zu bauen, dauere heute Stunden statt Tage. Während die Industrie noch patche, sei der Schaden oft schon angerichtet.

Buterins und Guillemets Analysen zeichnen zwei unterschiedliche Bilder derselben Realität. Der Ethereum-Gründer wettet auf die mathematische Verteidigung, der Ledger-CTO warnt vor der Geschwindigkeit der Angreifer. Für Anleger im DACH-Raum bleibt die Frage relevant, wie sich diese Dynamik auf die Sicherheitsarchitektur von Blockchain-Projekten auswirkt – und ob regulatorische Vorgaben wie die MiCA-Verordnung künftig formale Verifikationspflichten vorsehen werden.