Computing Exact Worst-Case Gas Consumption for Smart Contracts

Abstract:

The Ethereum platform is a public, distributed, blockchain-based database that is maintained by independent parties. A user interacts with Ethereum by writing programs and having miners execute them for a fee charged on-the-fly based on the complexity of the execution. The exact fee, measured in gas consumption, in general depends on the unknown Ethereum state, and predicting even its worst case is in principle undecidable. Uncertainty in gas consumption may result in inefficiency, loss of money, and, in extreme cases, in funds being locked for an indeterminate duration. This feasibility study presents two methods for determining the exact worst-case gas consumption of a bounded Ethereum execution using methods influenced by symbolic model checking. We give several concrete cases where gas consumption estimation is needed, and provide two approaches for determining gas consumption, one based on symbolically enumerating execution paths, and the other based on computing paths modularly based on the program structure.

BibTeX:

@inproceedings{marescotti_computing_2018,
    title = {{Computing Exact Worst-Case Gas Consumption for Smart Contracts}},
    author = {Marescotti, Matteo and Blicha, Martin and Hyvärinen, Antti E. J. and Asadi, Sepideh and Sharygina, Natasha},
    year = {2018},
    booktitle = {{Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice}},
    editor = {Margaria, Tiziana and Steffen, Bernhard},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-030-03427-6_33},
    isbn = {978-3-030-03427-6},
    pages = {450--465},
}

Proceedings paper