RT Journal Article
T1 Secure Optimizations on Ethereum Bytecode Jump-Free Sequences
A1 Kirchner, Daniel
A1 Albert Albiol, Elvira María
A1 Genaim, Samir
A1 Martín Martín, Enrique
AB Program optimization is a key factor for green software. In the context of the Ethereum blockchain, optimization is particularly relevant because there is a fee to pay for each EVM (Ethereum Virtual Machine) instruction executed and also there exist bytecode-size limitations for deploying the software on the blockchain. Still, optimization of EVM code is not as widely spread as one could imagine. This is at least partly due to the lack of trust in the correctness of the tools, as security is even more relevant than efficiency in the blockchain context in which bugs may cause huge economical losses. This article develops a formal verification framework using Coq to ensure the security of EVM optimizations performed on jump-free sequences of EVM bytecode. By means of Coq's theorem proving capabilities, we are able to automatically verify/certify that an optimized jump-free sequence of EVM opcodes is semantically equivalent to a given original one. We also present an extension to our framework that can handle inter-block optimizations that propagate global information across blocks. We have applied our tool to successfully prove the security of peephole optimizations performed by the standard Solidity compiler, and also to existing EVM superoptimization tools (namely GASOL and Superstack) in which we have found bugs that have been reported and fixed.
PB IEEE
YR 2025
FD 2025
LK https://hdl.handle.net/20.500.14352/132820
UL https://hdl.handle.net/20.500.14352/132820
LA eng
DS Docta Complutense
RD 26 feb 2026