Blockchain Superoptimizer

TL;DR

This paper introduces a superoptimizer for Ethereum's EVM bytecode that uses SMT formulas and constraint solving to automatically generate more cost-efficient smart contract bytecode, demonstrated through large-scale evaluations.

Contribution

It presents a novel approach to optimize EVM bytecode by encoding its semantics as SMT formulas and applying constraint solving, which has not been done before.

Findings

Successfully optimized real-world EVM bytecode

Demonstrated significant cost reductions in bytecode execution

Implemented a scalable superoptimizer tool for Ethereum smart contracts

Abstract

In the blockchain-based, distributed computing platform Ethereum, programs called smart contracts are compiled to bytecode and executed on the Ethereum Virtual Machine (EVM). Executing EVM bytecode is subject to monetary fees---a clear optimization target. Our aim is to superoptimize EVM bytecode by encoding the operational semantics of EVM instructions as SMT formulas and leveraging a constraint solver to automatically find cheaper bytecode. We implement this approach in our EVM Bytecode SuperOptimizer ebso and perform two large scale evaluations on real-world data sets.