Albert Albiol, Elvira MaríaCorreas, JesúsGordillo Alguacil, PabloRomán-Díez, GuillermoRubio, Albert2024-01-302024-01-302021-02-260164-1212https://hdl.handle.net/20.500.14352/96471Gas is a measurement unit of the computational effort that it will take to execute every single replicated operation that takes part in the Ethereum blockchain platform. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised and its execution is interrupted. One of the main open problems in the analysis of Ethereum smart contracts is the inference of sound bounds on their gas consumption. We present, to the best of our knowledge, the first static analysis that is able to infer sound parametric (i.e., non-constant) gas bounds for smart contracts. The inferred bounds can be parametric on the sizes of the input parameters for the functions, but also they can be parametric on the contract state, or blockchain data. Our gas analysis is developed at EVM bytecode level, in which Ethereum gas model is defined. Our analysis is implemented in a tool named Gastap, Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract and automatically infers sound gas upper-bounds for its public functions. Gastap has been applied over 318,093 functions fetched from the Ethereum blockchain, and succeeded to obtain gas bounds for 90.24% of them.engAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/journal articlehttps://www.sciencedirect.com/science/article/pii/S0164121221000200restricted accessInformática (Informática)1203.17 Informática