FORMALE VERIFIKATION VON SMART CONTRACTS
Dr. Christian Reitwiessner
@ethchris
github.com/chriseth
IC3-Ethereum Crypto Boot Camp
2016-07-26
Problem:
Code korrekt zu schreiben ist schwierig!
Hauptziel: mentales Modell mit Maschinenmodell abgleichen
Gewünschtes Verhalten lässt sich leicht testen, Abwesenheit unerwünschten Verhaltens schwer überprüfen
Grund: Tests erfassen nur eine endliche Anzahl von Fällen
Das ist wichtig für Ethereum.
Wie bei einem Webdienst kann der Angreifer überall sein
Quellcode oft verfügbar (gut und schlecht)
Prominentes Beispiel: The DAO