Vitalik prognostiziert eine fehlerfreie Zukunft für Smart Contracts

Entwickler, die Sicherheit priorisieren, können damit rechnen, dass fehlerfreies Coding in den 2030er Jahren erreichbar wird, so der Co-Gründer von Ethereum, Vitalik Buterin. 

Nach dem umstrittenen Hard Fork von Gnosis Chain zur Rückgewinnung von 9,4 Millionen US-Dollar aus dem Balancer-Hack sagte der Ethereum-Co-Gründer Vitalik Buterin, der Glaube, dass „Bugs unvermeidbar sind und man keinen fehlerfreien Code schreiben kann“, werde in den 2030er Jahren nicht mehr zutreffen.

Was sagte Vitalik Buterin über Coding? 

Vitalik Buterin hat eine Vorhersage getroffen, dass fehlerfreier Code in den 2030er Jahren durch eine Interaktion auf der Social-Media-Plattform X Realität werden wird. 

Die Diskussion begann, als Gnosis Chain ankündigte, dass es am 22. Dezember einen Hard Fork durchführte, wie berichtete von Cryptopolitan berichtet. Der Hard Fork sicherte 9,4 Millionen US-Dollar zurück, die während des Balancer-Exploits im November 2024 gestohlen wurden, bei dem über 128 Millionen US-Dollar über mehrere Blockchains hinweg geleert wurden. Die Rückgewinnung erforderte, dass die meisten Validatoren neue Software annahmen, und diejenigen, die das Update nicht durchführten, stehen vor Strafen.

Dies stieß natürlich auf Widerstand von Blockchain-Befürwortern, die die Maßnahme kritisierten, da sie gegen das Prinzip der Unveränderlichkeit verstößt. Ein X-Nutzer mit dem Spitznamen „colluding node“ sagte, das eigentliche Problem liege darin, wie Blockchain-Anwendungen gebaut werden. Er argumentierte, dass die Verwendung von Smart Contracts in programmierbaren virtuellen Maschinen der falsche Ansatz sei. 

„Es gibt nur 7 Verträge, die es wert sind, geschrieben zu werden, und sie sollten in der Basisschicht verankert werden und Sicherheit durch Client-Diversität erhalten“, schrieb der Nutzer. 

Buterin dann antwortete durch die Klarstellung, dass formal verifiziert nicht gleichbedeutend mit nachweislich fehlerfrei ist. Er ging weiter und deutete an, dass nachweislich fehlerfreier Code möglicherweise sogar unmöglich sei.

„Ich würde sogar so weit gehen zu sagen, dass ‚nachweislich fehlerfrei‘ nicht möglich ist, denn ‚fehlerfrei‘ bedeutet ‚keine Lücke zwischen Absicht und Code-Ausführung‘, und unsere Absicht ist ein extrem komplexes Objekt, auf das wir nur begrenzten Zugriff haben.“ 

Formale Verifikation verwendet mathematische Methoden, um zu überprüfen, ob sicherheitskritische Systeme korrekt funktionieren. Die Technik wird seit den 1960er Jahren in Bereichen wie der Luft- und Raumfahrttechnik eingesetzt. 

Wenn sie in Smart Contracts verwendet wird, kann die formale Verifikation beweisen, dass die Geschäftslogik eines Vertrags eine vordefinierte Spezifikation erfüllt; jedoch trotz der Tatsache, dass Balancer-Verträge 11 Mal von vier separaten Sicherheitsfirmen überprüft wurden, schlüpfte ein kritischer Fehler dennoch durch. 

Ist eine Zukunft mit fehlerfreiem Code möglich? 

Buterin schlug vor, dass die Lösung in mehreren Schichten von Redundanz besteht, um Lücken zwischen Absicht und Ausführung herauszufiltern. Er verwies auf Typensysteme als eine Form der Redundanz und auf die formale Verifikation spezifischer Aussagen über Code als eine weitere Schicht.

Formale Verifikation kann Probleme wie Integer-Underflows und Overflows, Re-Entrancy und schlechte Gas-Optimierungen erkennen, die Auditoren und Testern entgehen könnten. Währenddessen kann traditionelles Testen nur das Vorhandensein von Fehlern überprüfen, nicht aber deren Abwesenheit.

Buterin bemerkte, dass einige Software weiterhin Bugs haben wird, da Funktionsgewinne in bestimmten Fällen wichtiger sind als Perfektion. Aber Entwickler, die Sicherheit priorisieren, werden die Werkzeuge haben, um wirklich fehlerfreien Code zu erreichen.