Yannis Smaragdakis: Decompiling Contracts, Detecting Gas-Focused Vulnerabilities

We're very happy to have Yannis Smaragdakis [1][2] from the University of Athens speak to us on two static analysis techniques on EVM bytecode: MadMax[3], which detects gas-focused vulnerabilities, and Gigahorse, which performs decompilation of EVM bytecode. Professor Smaragdakis' research focuses on program analysis, language mechanisms for abstraction, and languages and tools for systems. His abstract follows.

"MadMax[3] combines contract decompilation and declarative program-structure queries. The analysis captures high-level domain-specific concepts (such as “dynamic data structure storage” and “safely resumable loops”) and achieves high precision and scalability. MadMax analyzes the entirety of smart contracts in the current Ethereum blockchain in just 10 hours (with decompilation timeouts in 8% of the cases) and flags contracts with a current monetary value in the $B range. (Manual inspection of a sample of flagged contracts shows that 81% of the sampled warnings do indeed lead to vulnerabilities.)

"Gigahorse is a general-purpose decompiler for EVM bytecode, drastically improving over past approaches (including the decompilation techniques used in MadMax). Gigahorse turns EVM bytecode into a high-level 3-address code representation. The new intermediate representation of smart contracts makes implicit data- and control-flow dependencies of the EVM bytecode explicit. Gigahorse can decompile over 99.98% of deployed contracts and offers a full-featured toolchain for further analyses.

"Key to both MadMax and Gigahorse is the use of a declarative, logic-based specification for the analysis."

[1] https://yanniss.github.io/
[2] https://www.linkedin.com/in/yannis-smaragdakis-31a149/
[3] http://yanniss.github.io/eth-oopsla18.pdf