VeriSol von Microsoft Azure – Verifizierung von Solidity Smart Contracts
Microsoft kündigt die Einführung von VeriSol an. Die Open Source Software ist ein Prüfungs-System für Ethereums Solidity. Damit soll nicht nur die Anwendung von Smart Contracts gestärkt, sondern auch eine Vervollständigung des Blockchain-Ökosystems gefördert werden.
Smart Contracts prüfen für mehr Sicherheit
Smart Contracts sind zum wesentlichen Bestandteil der Blockchain geworden und kommen auf sehr unterschiedliche Weise zum Einsatz. Wie jeder Code muss auch ein Smart Contract sorgfältig geprüft werden, bevor er zum Einsatz kommt. Schließlich würde man auch keine Fahrzeuge über eine neue Brücke fahren lassen oder ein Gebäude einweihen, ohne vorher die Stabilität und Sicherheitsbedingungen ausgiebig zu testen.
Die Folge davon sind Probleme wie Hacking Angriffe auf Exchanges und andere Kryptowährungs-Diebstählen. Microsoft hat sich mit Azure diesen Problemen angenommen. Azure st ein von Microsoft entwickelter Cloud-Computing-Dienst zum Erstellen, Testen, Bereitstellen und Verwalten von Anwendungen und Diensten auf der Blockchain. Die angebotene Softwarelösung heißt VeriSol.
Smart Contracts wurden auch früher schon wie jeder andere reguläre Code überprüft. Das traditionelle Audit eines Codes beruhte auf der Fähigkeit der Entwickler, genau vorhersagen zu können, wie ihr Produkt später verwendet wird. Das Problem dabei sind jedoch die Grenzen der menschlichen Logik und Abstraktionsfähigkeit. Häufig werden dabei Testfälle und Szenarien übersehen, weil es schlicht zu viele Möglichkeiten gibt.
Ein so umfangreicher Test des Codes würde außerdem viel zu lange dauern und enorme Kosten verursachen. Daher gibt es meist ein vorgefertigtes Protokoll, mit dem Entwickler die anfälligeren Stellen des Codes kontrollieren können. Es handelt sich dabei jedoch nur um eine Lösung, die die wichtigsten Punkte abdeckt.
Microsoft Azure VeriSol – Verifier for Solidity
VeriSol ist ein Open Source Tool, die von der Azure Blockchain in Zusammenarbeit mit den Forschern von Microsoft Research entwickelt wurde. Microsoft Research befasste sich bereits mit fortschrittlichen Techniken, um die Korrektheit von Softwareprogrammen zu verifizieren. Der Name des Tools ist eine Zusammensetzung aus Verifier for Solidity. Solidity ist die Programmiersprache, in der die Smart Contracts in Ethereum erstellt werden. Sie ist die beliebteste und am häufigsten genutzte Sprache, um Smart Contracts zu erstellen.
Um das Tool zu nutzen schreiben Entwickler die Spezifikationen ihres Smart Contracts in einer Zwischensprache. VeriSol überprüft diese Spezifikationen dann mithilfe von mathematischen Logikmechanismen. Bei dieser Form der formalen Überprüfung werden alle nur möglichen Fälle automatisch durchgerechnet. Für Entwickler und Kunden bedeutet das ein bisher noch nie dagewesenes Maß an Sicherheit bei der Anwendung von Smart Contracts.
Derzeit ist VeriSol noch ein Prototyp. Das Entwicker-Team hat das Tool bereits auf einige Smart Contracts zu unterschiedlichen Anwendungsszenarien auf der Azure Blockchain angewendet. Das Team hat höhere Ziele und möchte andere zur Zusammenarbeit ermutigen. Denn das Open Source Tool soll nicht nur den Entwicklern und Kunden der Azure Blockchain zugutekommen, sondern das gesamte Blockchain Ökosystem bereichern.
