Specification Mining for Smart Contracts with Automatic Abstraction Tuning

Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development, auditing, and the post-mortem analysis of attacks.

In this talk, I will present the first specification mining technique for smart contracts. Our technique extracts the possible behaviors of smart contracts from executions recorded on a blockchain and expresses them as automata. A novel dependency analysis allows us to separate independent interactions with a contract. Our technique tunes the abstractions for the automata construction automatically based on configurable metrics, for instance, to maximize readability or precision. We implemented our technique for the Ethereum blockchain and evaluated its usability on several real-world contracts.

Maria Christakis is a tenure-track faculty member of the Max Planck Institute for Software Systems (MPI-SWS) in Germany, where she leads the “Practical Formal Methods” Group since October 2017. She was previously a lecturer (assistant professor) at the University of Kent, England and a post-doctoral researcher at Microsoft Research Redmond, USA. She received her Ph.D. from the Department of Computer Science of ETH Zurich, Switzerland in 2015. Maria has been awarded with a Facebook Faculty Research Award, the EAPLS Best PhD Dissertation Award, and the ETH medal for her doctoral thesis.