Preventing Out-of-Gas Exceptions by Typing

TL;DR

This paper develops a type system for TinySol, a simplified smart contract language, to prevent out-of-gas exceptions by ensuring contracts do not run out of gas during execution.

Contribution

It extends TinySol with exceptions and gas modeling, and introduces a type system that guarantees smart contracts will not exhaust gas at runtime.

Findings

Type system guarantees no out-of-gas runtime errors.

Gas mechanism models real Ethereum smart contract behavior.

Formal semantics for TinySol with gas and exceptions.

Abstract

We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.