5 papers
Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph
Elvira Albert, Jesús Correas, Pablo Gordillo +2
The EVM language is a simple stack-based language with words of 256 bits, with one significant difference between the EVM and other virtual machine languages (like Java Bytecode or…
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts
Elvira Albert, Jesús Correas, Pablo Gordillo +2
We present the main concepts, components, and usage of GASOL, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. GASOL offers a wide variety of cost models that all…
SAFEVM: A Safety Verifier for Ethereum Smart Contracts
Elvira Albert, Jesús Correas, Pablo Gordillo +2
Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents…
Running on Fumes--Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis
Elvira Albert, Pablo Gordillo, Albert Rubio +1
Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction exec…
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
Elvira Albert, Pablo Gordillo, Benjamin Livshits +2
Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores th…