ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 13:30 - 14:30 at S4 (HCVS) - III Chair(s): John P. Gallagher

The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics.

This tutorial will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust, a framework for the static analysis of Ethereum smart contracts that we recently introduced, which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first static analysis for EVM bytecode, based on Horn clause resolution, that comes with a proof of soundness.

slides (ETAPS19.pdf)12.37MiB

Sun 7 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:30
IIIHCVS at S4 (HCVS)
Chair(s): John P. Gallagher Roskilde University
13:30
60m
Invited Talk: Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
HCVS
File Attached
14:30
30m
Talk
Coinduction in Uniform: what's next?
HCVS
Henning Basold CNRS & ENS Lyon, Ekaterina Komendantskaya Heriot-Watt University, UK
Link to publication
15:00
30m
Full-paper
Ultimate TreeAutomizer
HCVS
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Jochen Hoenicke Universität Freiburg, Alexander Nutz University of Freiburg, Germany, Andreas Podelski University of Freiburg, Germany