Blockchain Superoptimizer
Julian Nagele, Maria A Schett

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBlockchain Technology Applications and Security · Cloud Computing and Resource Management · Advanced Data Storage Technologies
