The talk will present two related static analysis techniques on Ethereum VM (EVM) bytecode: MadMax, which detects gas-focused vulnerabilities, and Gigahorse, which performs decompilation of EVM bytecode.

MadMax 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.

Research Interests: programming languages and software engineering

• Program analysis (static analysis, test generation, invariant inference, symbolic execution)
• Language mechanisms for abstraction (declarative languages, program generation, DSLs, modules and components, generics, extensible languages, multi-paradigm programming)
• Languages and tools for systems (programming models for concurrency, language support for distributed computing, memory management and program locality)