Luca Negrini
Logo

Luca Negrini

static-analysis  abstract-interpretation  evm  cfg-reconstruction

Towards a Sound Construction of EVM Bytecode Control-flow Graphs

Authors: Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, Enea Zaffanella
Formal Techniques for Java-like Programs (FTfJP 2024)
Wien, Austria, September 16, 2024
Workshop paper

Abstract

Ethereum enables the creation and execution of decentralized applications through smart contracts, that are compiled to Ethereum Virtual Machine (EVM) bytecode. Once deployed in the blockchain, the bytecode is immutable; hence, ensuring that smart contracts are bug-free before their deployment is of utmost importance. A crucial preliminary step for any effective static analysis of EVM bytecode is the extraction of the control-flow graph (CFG): this presents significant challenges due to dynamically computed jump destinations. In this paper we present a novel approach, based on abstract intepretation, aiming at building a sound CFG from EVM bytecode smart contracts. Our analysis, which is implemented in our static analyzer EVMLiSA, is based on a parametric abstract domain that approximates concrete execution stacks at each program point as a $l$-sized set of abstract stacks of maximal height $h$; the results of the analysis are then used to resolve the jump destinations at jump nodes. On our preliminary experiments, by fine-tuning the analysis parameters, EVMLiSA achives sound CFGs for all smart contracts where permantent storage-related opcodes do not influence jump destinations.

Manuscript: PDF
Associated project: LiSA
Conference page: Link
ACM page: Link