Floragasse 7 – 5th floor, 1040 Vienna
Subscribe to our Newsletter

Key Researcher Talk – Practical and Provably Sound Static Analysis of Ethereum Smart Contracts by Matteo Maffei (Remote)

November 30, 2020
2:00 pm - 3:00 pm

Join the 3nd edition of our Key Researcher Talk Series!

Practical and Provably Sound Static Analysis of Ethereum Smart Contracts

Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known.

In this talk, I will present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers.

This talk is based on a paper with the same title presented at CCS 2020.


14:00 -14:30: Talk by Matteo Maffei
14:30-15:00: Discussion


Matteo Maffei, Head of Research Unit, TU Wien

Matteo is Professor at the Institute of Logic and Computation at TU Wien and head of the Security and Privacy Group.

He studied Computer Science at the University of Venice (Italy), where he received the Laurea in 2002 and the Ph.D. in 2006. Between 2006 and 2017 he worked at Saarland University (Germany), first as research group leader and then as associate professor. In 2017, he joined TU Wien as full professor and head of the Security and Privacy Group. He is holder of a DFG Emmy Noether fellowship (2009) and an ERC Consolidator Grant (2018).

Free Registration

Please reach out to us at events@sba-reserarch.org if you would like to join.

hosted by Vienna ACM SIGSAC Chapter.