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.
Preventing Out-of-Gas Exceptions by Typing / Aceto, Luca; Gorla, Daniele; Lybech, Stian; Hamdaqa, Mohammad. - (2024). (Intervento presentato al convegno 18th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation tenutosi a Creta (GR)).
Preventing Out-of-Gas Exceptions by Typing
Daniele Gorla;
2024
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
