Von Grigore Rosu, Everett Hildenbrandt, Daejun Park, Shuvendu Lahiri
„Tests zeigen das Vorhandensein, nicht das Fehlen von Fehlern“ (Dijkstra, 1969). Obwohl in den letzten 50 Jahren bemerkenswerte Fortschritte im Testen erzielt wurden, ist umfassendes Testen in den meisten Fällen nach wie vor unpraktisch, und wir haben manchmal auf die harte Tour gelernt, dass verbleibende Fehler katastrophale Folgen haben können.
Die Natur der Blockchain, bei der Code, der auf einen gemeinsamen Zustand zugreift, öffentlich ist und von jedem von überall aus aufgerufen werden kann, verstärkt sowohl die Geschwindigkeit, mit der Hacker Fehler finden, als auch die Konsequenzen ihrer Ausnutzung. Testen ist daher hier einfach unzureichend. Die formale Verifikation ist die einzige bekannte praktikable Alternative.
Dieser Vortrag wird erklären, was formale Verifikation im Kontext von Blockchain-Smart Contracts, Tokens und Protokollen ist, warum sie zunehmend kritisch wird, wie sie durchgeführt wird und welche Werkzeuge zur Verfügung stehen. Es werden mehrere Ansätze behandelt, von automatisierten und leichten, die Fehler finden, bis hin zu interaktiven und umfassenden, die alle Verhaltensweisen analysieren, von hochgradigem Quellcode, den Entwickler schreiben und verstehen, bis hin zu niedriggradigem Bytecode, der von Knoten-Clients ausgeführt wird.
Dieser Vortrag zielt auch darauf ab, das Bewusstsein zu schärfen, dass, entgegen dem weit verbreiteten Missverständnis, bei dem formale Verifikation mit Code-Audits verwechselt wird, es erheblich mehr Aufwand erfordert, ein Programm formal zu verifizieren, als das Programm zunächst zu schreiben. Denken Sie an das 9-fache! Tatsächlich besagt eine Faustregel bei NASA, dass 20 % des Budgets eines Projekts in das Schreiben von Code fließen und 80 % in Verifikation und Validierung; und NASA-Code ist nicht öffentlich und niemand außer NASA kann ihn nach der Bereitstellung aufrufen.