Mattia Merenda
Logo

Saverio Mattia Merenda

Master's Student
University of Parma, Italy

static-analysis  abstract-interpretation  blockchain  ethereum  smart-contract

Talk: Towards a Sound Construction of EVM Bytecode Control-flow Graphs

26th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2024)
Vienna, Austria, September 20, 2024, 2:00 PM - 2:30 PM CET
Conference presentation

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 an 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 builds sound CFGs for all smart contracts where permantent storage-related opcodes do not influence jump destinations.

Slides: PDF
Conference talk: Paper @ FTfJP 2024
Associated project: EVMLiSA
Conference page: Link
ACM page: Link
Linkedin post: Link
Attendance: PDF

FTfJP24_1.jpeg
FTfJP24_2.jpeg