Running on Fumes

Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis
  • Elvira Albert
  • Pablo GordilloEmail author
  • Albert Rubio
  • Ilya Sergey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11847)


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 executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviors. We report on the design and implementation of Gastap, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities.


  1. 1.
  2. 2.
    Etherscan (2018).
  3. 3.
    Oyente: An Analysis Tool for Smart Contracts (2018).
  4. 4.
    Albert, E., et al.: SACO: static analyzer for concurrent objects. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 562–567. Springer, Heidelberg (2014). Scholar
  5. 5.
    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008). Scholar
  6. 6.
    Albert, E., Gordillo, P., Livshits, B., Rubio, A., Sergey, I.: EthIR: a framework for high-level analysis of ethereum bytecode. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 513–520. Springer, Cham (2018). Scholar
  7. 7.
    Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in Isabelle/HOL. In: CPP 2018, pp. 66–77. ACM (2018)Google Scholar
  8. 8.
    Bernani, T.: Oraclize (2016).
  9. 9.
    Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: PLAS 2016, pp. 91–96. ACM (2016)Google Scholar
  10. 10.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). Scholar
  11. 11.
    Chen, T., Li, X., Luo, X., Zhang, X.: Under-optimized smart contracts devour your money. In: SANER 2017, pp. 442–446. IEEE Computer Society (2017)Google Scholar
  12. 12.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of aprogram. In: POPL 1978, pp. 84–96 (1978)Google Scholar
  13. 13.
    Ethereum. Solidity (2018).
  14. 14.
    Ethereum. Vyper (2018).
  15. 15.
    Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275–295. Springer, Cham (2014). Scholar
  16. 16.
    Ethereum Foundation. Safety - Ethereum Wiki (2018). Accessed on 14 Nov 2018
  17. 17.
    Grech, N., Kong, M., Jurisevic, A., Brent, L., Scholz, B., Smaragdakis, Y.: Madmax: surviving out-of-gas conditions in ethereum smart contracts. In: PACMPL, 2(OOPSLA), pp. 116:1–116:27 (2018)CrossRefGoogle Scholar
  18. 18.
    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243–269. Springer, Cham (2018). Scholar
  19. 19.
    Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. In: PACMPL, 2(POPL), pp. 48:1–48:28 (2018)CrossRefGoogle Scholar
  20. 20.
    Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: NDSS 2018. The Internet Society (2018)Google Scholar
  21. 21.
    Kolluri, A., Nikolic, I., Sergey, I., Hobor, A., Saxena, P.: Exploiting The Laws of Order in Smart Contracts. CoRR, abs/1810.11605 (2018)Google Scholar
  22. 22.
    Krupp, J., Rossow, C.: Teether: Gnawing at ethereum to automatically exploit smart contracts. In: USENIX Security Symposium, pp. 1317–1333. USENIX Association (2018)Google Scholar
  23. 23.
    Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In CCS 2016, pp. 254–269. ACM (2016)Google Scholar
  24. 24.
    Marescotti, M., Blicha, M., Hyvärinen, A.E.J., Asadi, S., Sharygina, N.: Computing exact worst-case gas consumption for smart contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 450–465. Springer, Cham (2018). Scholar
  25. 25.
    Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: ACSAC 2018, pp. 653–663. ACM (2018)Google Scholar
  26. 26.
    Suiche, M.: Porosity: A Decompiler For Blockchain-Based Smart Contracts Bytecode (2017)Google Scholar
  27. 27.
    Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: CCS 2018, pp. 67–82. ACM (2018)Google Scholar
  28. 28.
    Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Wood, G.: Ethereum: A secure decentralised generalised transaction ledger (2014)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Elvira Albert
    • 1
  • Pablo Gordillo
    • 1
    Email author
  • Albert Rubio
    • 1
  • Ilya Sergey
    • 2
  1. 1.Complutense University of MadridMadridSpain
  2. 2.Yale-NUS College and School of ComputingNUSSingaporeSingapore

Personalised recommendations