Research

Blockchains support execution of smart contracts: programs encoding complex transaction protocols between distrusting parties. Due to their distributed nature, blockchains rely on third-party miners to execute and validate transactions. Miners are compensated by charging users with gas based on the execution cost of the transaction. To compute the exact gas cost, blockchains track gas cost dynamically creating its own overhead. This paper presents a static exact gas-cost analysis technique that can be employed to eliminate dynamic gas tracking. This approach presents further benefits such as providing miners with a trusted gas bound that can be verified in linear time, and eliminating out-of-gas exceptions. To handle recursion and unbounded computation, we propose a novel amortization technique that stores gas inside data structures. We have implemented our analysis technique in a tool called GasBoX that takes a contract as input and infers the gas cost of its functions automatically. We have evaluated GasBoX on 13 standard smart contracts borrowed from real-world blockchain projects. Our soundness theorem proves that the gas bound inferred by GasBoX exactly matches the gas cost at runtime and no dynamic gas tracking is necessary.