Visit the
https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
In this hands-on workshop, we will go through the process of formally verifying smart contracts. The attendees will learn (1) how to formally specify relevant functional requirements of Ethereum contracts, such as "the sum of deposits never exceeds the contract’s balance", and (2) how to verify these using existing analysis tools for Ethereum.
First, we will show how to formally specify the intended behavior of smart contracts. We will look closer at safety temporal properties, an expressive class of properties for capturing which sequences of contract states are considered correct. We will present common requirement idioms, including access control, state-based properties, multi-contract invariants, and others.
Next, we will provide an overview of existing testing tools, such as tools based on symbolic execution and fuzzers. The goal is to understand how they can be used to identify violations of the formalized properties as well as their limitations in providing unbounded formal guarantees.
Finally, we will learn how formal verifiers go beyond testing and can provide unbounded formal guarantees (for any sequence of transactions). We will take a closer look at the specification language used by VerX and its automated verification method, which is easy to use and does not require in-depth knowledge in formal verification.
Speaker(s): Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf, Petar Tsankov
Skill level: intermediate
Track: Security
Keywords: technical
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit
https://ethereum.foundation/