Preventing Out-of-Gas Exceptions by Typing

2024/07/22 by Luca Aceto, Aceto, Luca, Daniele Gorla +5 · 1 citation
Engineering · #Combustion and Detonation Processes

paper · pdf · doi:10.48550/arxiv.2407.15676

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.

Cited by

• Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts

Related

• Running on Fumes--Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis
• Under-Optimized Smart Contracts Devour Your Money
• How to Save My Gas Fees: Understanding and Detecting Real-world Gas Issues in Solidity Programs
• Lazy Contracts: Alleviating High Gas Costs by Secure and Trustless Off-chain Execution of Smart Contracts
• Off-chain Execution and Verification of Computationally Intensive Smart\n Contracts