Es gibt ein neues Blockchain-Modewort, das rechtzeitig für den Herbst ankommt - formale Verifizierung.

Der Satz (der die Anwendung der Mathematik zur Überprüfung von Softwareprogrammen beschreibt) wurde bisher in der Presse nur spärlich erwähnt. Aber wenn die Konversation letzte Woche auf dem Developer Summit von Ethereum ein Hinweis war, könnte sie angesichts der Sicherheitsfragen, die Smart Contracts und Blockchains immer noch umgeben, eine zunehmende Rolle spielen.

Wie mehrere Vorträge zeigen, die dem Thema bei Devcon2 gewidmet sind, wird die Idee, dass Ethereum-Codern neue Zusicherungen gegeben werden können, von der Entwicklungsgemeinschaft weitgehend akzeptiert. Das Konzept wird bereits vorgeschlagen, um das gesamte Ethereum-Protokoll selbst und seine experimentelle Proof-of-Stock-Blockchain zu stärken.

Dass dies geschehen ist, ist vielleicht keine Überraschung angesichts des plötzlichen Zusammenbruchs von The DAO in diesem Sommer, dem bisher größten Smart-Vertrag, der auf der dezentralen Anwendungsentwicklungsplattform gestartet wurde.

Aber während die formale Verifikation vielschichtig klingt, kann das Konzept vielleicht kurz zusammengefasst werden, wenn es auf das Ethereum angewendet wird - Programmierer verwenden derzeit eine weitgehend neue Sprache (Solidität), um intelligente Verträge zu schreiben, Befehle zu schreiben, die dann in Bytecode übersetzt werden die Ethereum Virtual Machine (EVM) und zur Ausführung an die Netzwerkknoten verteilt.

In gewissem Sinne kann formale Verifizierung als ein objektiverer Weg angesehen werden, um sicherzustellen, dass, wenn verschiedene Komponententeile des Netzwerks diese Anweisungen erhalten, sie diese im Auftrag von Benutzern wie beabsichtigt ausführen.

Grant Passmore, Mitbegründer von Aesthetic Integration, ist ein Unternehmer, der eine Möglichkeit sieht, bei dieser Aufgabe mitzuhelfen und mit Devcon2 Imandra Contracts, eine formale Verifikationsplattform für Blockchain Smart Contracts, zu lancieren.

Auf der Veranstaltung erinnerte er an die Idee, dass Ethereum angesichts der Ziele seiner Gemeinschaft und der wesentlichen Verantwortlichkeiten, die es dem Code anvertrauen will, als "Paradies" für die formale Verifikation dienen könnte.

Passmore sagte CoinDesk:

"Die Ethereum-Community befindet sich in einer einzigartigen Position, wo wir nach The DAO verstehen, dass rigoroses Engineering notwendig ist. Sie können keinen intelligenten Vertrag wie eine Web-App schreiben."

Anderswo sprachen Redner wie Philip Daian von Cornell zu dem Interesse an der Methodik, indem sie den Zuhörern sagten, er glaube, dass formale Verifizierung dazu beitragen könne, wesentliche Probleme zu lösen.

"Es wird ein kritischer Teil des Gesamtbildes sein. Ich freue mich darauf, mit ätherum den Standard zu setzen und den Leuten zu zeigen, wie es gemacht wird", sagte er.

Trainingsräder

Angesichts der Tatsache, dass Finanzunternehmen in jüngster Zeit den Schwerpunkt auf die Erforschung intelligenter Vertragssprachen gelegt haben, war das Konzept der Anwendung formaler Verifikation auf Solidität das häufigste Diskussionsthema.

Solidity wurde für die Ethereum-Plattform entwickelt und stand vor der Kritik, dass es weitgehend unerprobt und schwer zu schreiben ist, vor allem, weil es so neu ist. Solche Probleme wurden wohl aufgrund von Problemen mit dem Compiler der Sprache, einem Mangel an öffentlichen Bibliotheken und dem Zusammenbruch von The DAO, der von namhaften Mitgliedern seiner Entwicklungsgemeinschaft überprüft wurde, verstärkt.

Vor diesem Hintergrund räumte Christian Reitweissner, der Erfinder von Solidity, ein, dass eine formale Verifizierung angestrebt wird, damit Fehler von den Ethereum-Codern besser erkannt werden können.

Reitweissner sagte CoinDesk, dass intelligente Vertragsentwickler eines Tages formale Verifikations-Tools verwenden könnten, um beispielsweise zu bestimmen, ob es unvorhergesehene Fehler in ihrer Arbeit gibt. Er wies darauf hin, dass ein solches Tool verwendet werden könnte, um zu bestimmen, ob das Ergebnis beim Hinzufügen von zwei Salden länger als das vom Compiler zugewiesene Feld verlängert wird.

"Das könnte passieren und das formale Verifikations-Tool [würde] das automatisch erkennen. Sie können es früh erkennen und darauf im Smart-Vertrag reagieren", erklärte er.

Laut Reitweissner hat das Solidity-Team bereits untersucht, wie die formale Verifikation auf seine Arbeit angewendet werden kann. Bereits im letzten Oktober gab es Prototypen dafür, wie ein Toolkit namens Why3 für diesen Zweck verwendet werden könnte, obwohl solche Angebote noch nicht für die gesamte Sprache verfügbar sind.

Proving Ground

Dieses Ethereum könnte verwendet werden, um zu testen, wie die formale Verifikation für die Finanzierung breiter angewendet werden könnte, war auch ein stark diskutiertes Thema während der Konferenz.

Passmore zum Beispiel sagte, Aesthetic Integration arbeite seit 2014 an formellen Verifizierungen in der Arbeit mit Finanzinstituten, und dass Kunden bisher versucht haben, sie in begrenzten Bereichen wie Dark Pools einzusetzen, wo Händler Sicherheit brauchen Gerechtigkeit.

In intelligenten Verträgen schlug Passmore vor, er sehe Ethereum als eine Gemeinschaft, die die Akzeptanz weiter vorantreiben könne.

"Viele unserer Bankkunden, als wir anfingen, mit ihnen zu arbeiten, hörten wir, dass sie sich für den Raum interessierten, aber dass sie sich Sorgen um die Korrektheit von intelligenten Verträgen machten", sagte er.

Der Fortschritt der formalen Verifikation hat Yoichi Hirai aus ähnlichen Gründen angezogen. Ein formeller Verifikationsingenieur, der jetzt bei der Ethereum Foundation angestellt ist, begann sein Interesse an dem Konzept als Forscher und in seiner früheren Anstellung bei dem Cyber-Security-Führer FireEye.

In einem Vortrag auf der Konferenz sprach Hirai über seine Frustration, indem er eine formale Verifikation in Umgebungen anwendete, in denen er keinen Zugriff auf den Quellcode hatte, oder die Aufgaben waren vielleicht zu weit gefasst, um das Konzept voranzutreiben.

"Ich habe Ethereum gefunden, ich habe das EVM gesehen, das gelbe Papier, die Spezifikation, es waren nur 32 Seiten und ich dachte, ich könnte es übersetzen und Beweise über intelligente Verträge schreiben", sagte er.

Im Gegensatz dazu bietet Ethereum, was er eine "kleinere Spezifikation" und ein "lösbares Problem" für Ingenieure nannte, an, wie sich Solidität am besten in Bytecode übersetzen lässt.

"Ich glaube, es kommen noch mehr formelle Verifikationsforscher", sagte er.

Keine Wunderwaffe

Doch trotz der Begeisterung werden Schritte unternommen, um zu warnen, wie viel formale Verifizierung erreichen könnte. Der Entwickler Alex Beregszaszi, der an Upgrades für das EVM arbeitet, sprach über die Notwendigkeit einer Reihe von Lösungen, die Entwicklern helfen sollen sicherzustellen, dass Smart Contract Code wie vorgesehen funktioniert.

Auch Passmore stellte fest, dass es schwierig ist zu sagen, ob sein neues System Probleme mit der DAO haben könnte, da formale Verifikations-Tools immer noch menschliche Eingaben erfordern.

"Sie können Probleme, die mit dem DAO aufgetreten sind, kodieren und sicherstellen, dass Sie diese nicht haben, aber Sie müssen wissen, wonach Sie suchen sollten", erklärte er.

Die Einschränkungen wurden von Reitweissner und Passmore bestätigt, die beide die Entwickler warnten, nicht an eine formale Verifikation als "Wunderwaffe" zu denken.

Reitweissner sieht jedoch die Methodik als eine Methode, die sich weiterentwickeln wird, da die Entwickler langsam besser darin sind, Probleme zu identifizieren und Repositories zu entwickeln, in denen das Wissen über gemeinsame Probleme zugänglich gemacht werden kann.

Auf diese Weise Passmore glaubt, dass es der Ethereum-Gemeinschaft gelingen wird, für das Konzept zu "evangelisieren", etwas, von dem er glaubt, dass es letztlich die Blockchain-Forschung voranbringen wird.

Passmore folgerte:

"Obwohl dies etwas ist, dem viele noch nie ausgesetzt waren, ist eine formale Verifikation das, was wir brauchen. Es ist eine Lernkurve, aber es muss angenommen werden, und das ist aufregend."

Bilder über Pete Rizzo für CoinDesk