Formal Verification of Smart Contracts Made Easy (Devcon5)
By Petar Tsankov, Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf
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.
Support this Site
Article comments