Besuchen Sie
https://archive.devcon.org/, um auf die gesamte Bibliothek der Devcon-Vorträge zuzugreifen, mit der Möglichkeit zu filtern, Playlists, personalisierte Vorschläge, dezentralen Zugriff auf IPFS und mehr.
In diesem praktischen Workshop werden wir den Prozess der formalen Verifikation von Smart Contracts durchgehen. Die Teilnehmer lernen (1) wie man relevante funktionale Anforderungen von Ethereum-Verträgen formal spezifiziert, wie zum Beispiel "die Summe der Einzahlungen überschreitet niemals das Guthaben des Vertrags", und (2) wie man diese mit bestehenden Analysetools für Ethereum verifiziert.
Zuerst werden wir zeigen, wie man das beabsichtigte Verhalten von Smart Contracts formal spezifiziert. Wir werden uns näher mit sicherheitstechnischen temporalen Eigenschaften befassen, einer ausdrucksstarken Klasse von Eigenschaften, um festzuhalten, welche Sequenzen von Vertragszuständen als korrekt angesehen werden. Wir werden gängige Anforderungsidiome präsentieren, einschließlich Zugriffskontrolle, zustandsbasierte Eigenschaften, Multi-Vertragsinvarianten und andere.
Als Nächstes geben wir einen Überblick über bestehende Testwerkzeuge, wie Werkzeuge, die auf symbolischer Ausführung und Fuzzern basieren. Das Ziel ist es zu verstehen, wie sie verwendet werden können, um Verstöße gegen die formalisierten Eigenschaften zu identifizieren sowie ihre Einschränkungen bei der Bereitstellung unbegrenzter formaler Garantien.
Schließlich werden wir lernen, wie formale Verifikatoren über Tests hinausgehen und unbegrenzte formale Garantien (für jede Transaktionssequenz) bieten können. Wir werden einen genaueren Blick auf die Spezifikationssprache werfen, die von VerX verwendet wird, und auf die automatisierte Verifizierungsmethode, die einfach zu bedienen ist und kein tiefgehendes Wissen in formaler Verifikation erfordert.
Referent(en): Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf, Petar Tsankov
Fähigkeitsstufe: mittel
Track: Sicherheit
Stichwörter: technisch
Devcon ist die Ethereum-Konferenz für Entwickler, Forscher, Denker und Macher.
Devcon 5 fand vom 8. bis 11. Oktober 2019 in Osaka, Japan, statt.
Devcon wird von der Ethereum Foundation organisiert und präsentiert, mit Unterstützung unserer Sponsoren. Um mehr zu erfahren, besuchen Sie bitte
https://ethereum.foundation/