Buterin ist überzeugt, dass letztlich das Gegenteil eintreten könnte: KI könnte Verteidigern die Werkzeuge an die Hand geben, die erforderlich sind, um Software von Anfang an deutlich schwerer angreifbar zu machen.
"Es ist eine immer häufiger vertretene Ansicht, dass KI-Hacking bedeutet, die Cybersicherheit ist dem Untergang geweiht. Ich widerspreche," schrieb Buterin am Mittwoch in einem ausführlichen und charakteristisch gehaltvollen Beitrag auf dem sozialen Netzwerk X.
Dem Ethereum-Mitbegründer zufolge sollte die Cybersicherheit ganz natürlich die Verteidiger bevorzugen, sobald Entwickler beginnen, den vollen Nutzen aus der formalen Verifikation zu ziehen.
Buterin verband diesen Glauben auch direkt mit seiner eigenen Erfahrung im Bereich der Kryptowährung und offenbarte, dass etwa 90% seines Nettovermögens weiterhin in Krypto investiert sind.
Jeder, der weiterhin beträchtliche Mengen an Kryptowährung hält, setzt seiner Ansicht nach implizit darauf, dass ausreichend sichere digitale Systeme gebaut werden können, trotz immer ausgefeilterer Angreifer.
"Wenn KI Navier-Stokes und FLT beweisen kann, dann kann KI auch die Aussage 'Dieses Programm ist sicher' als mathematisches Theorem beweisen," schrieb Buterin mit Bezug auf das Navier-Stokes-Problem und Fermats letzten Satz.
Sein Argument basiert auf formaler Verifikation, einer Methode, um mathematisch zu zeigen, dass Software bestimmte Eigenschaften erfüllt.
Buterin untersuchte die gleiche Idee ausführlich in seinem Essay vom Mai, in dem er KI-unterstützte formale Verifikation als ein enorm transformierendes Werkzeug für sicherheitskritische Software beschrieb. Allerdings könnte sich der Nachweis, dass solche Software wirklich sicher ist, als herausfordernd erweisen.
Das Definitionsproblem
Buterin nutzte die verschlüsselte Messaging-App Signal als Beispiel, um zu zeigen, warum dies schwierig sein könnte.
Ein Angreifer könnte versuchen, Nachrichten zu fälschen, sie an der Zustellung zu hindern, alte Nachrichten erneut zu senden, einen Server zu kompromittieren, den Prozess zur Entdeckung eines öffentlichen Schlüssels eines anderen Nutzers zu manipulieren oder eine Schwachstelle im Betriebssystem auszunutzen.
Weitere Probleme könnten durch beschädigte Datenbanken, bösartige Bibliotheken, Compiler oder sogar Informationslecks auf Hardware-Ebene entstehen.
Selbst wenn der Inhalt einer Unterhaltung verschlüsselt bleibt, könnte ein Angreifer trotzdem erfahren, wer miteinander kommuniziert. Folglich könnte die mathematische Definition dessen, was "sicher" eigentlich bedeutet, extrem komplex werden.
"Also ... selbst Definitionen können über tausend Codezeilen umfassen und benötigen eine gründliche, sorgfältige Überlegung, um sie zu verstehen," schrieb Buterin.
Angreifer und Verteidiger
Ohne Zweifel könnten leistungsfähigere KI-Systeme das Auffinden von Schwachstellen erleichtern.
Jedoch könnte derselbe Fortschritt im maschinellen Schlussfolgern auch die Kosten für die formale Beweisführung, dass Software den sorgfältig erstellten Sicherheitsvorgaben entspricht, drastisch senken.
Beide Seiten werden KI haben.
