Skip to Main content Skip to Navigation
Conference papers

Termination of Ethereum’s Smart Contracts

Thomas Genet 1 Thomas Jensen 1 Justine Sauvage 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Ethereum is a decentralized blockchain technology equipped with so-called Smart Contracts. Acontract is a program whose code is public, which can be triggered by any user, and whose actualexecution is performed by miners participating in Ethereum. Miners execute the contract on theEthereum Virtual Machine (EVM) and apply its effect by adding new blocks to the blockchain.A contract that takes too much time to be processed by the miners of the network may resultinto delays or a denial of service in the Ethereum system. To prevent this scenario, termination ofEthereum’s Smart Contracts is ensured using a gas mechanism. Roughly, the EVM consumes gasto process each instruction of a contract and the gas provided to run a contract is limited. Thistechnique could make termination of contracts easy to prove but the way the official definition ofthe EVM specifies gas usage makes the proof of this property non-trivial. EVM implementationsand formal analysis techniques of EVM’s Smart Contracts use termination of contracts as anassumption, so having a formal proof of termination of contracts is crucial. This paper presents amechanized, formal, and general proof of termination of Smart Contracts based on a measure ofEVM call stacks.
Complete list of metadata
Contributor : Thomas Genet Connect in order to contact the contributor
Submitted on : Tuesday, January 26, 2021 - 5:52:26 PM
Last modification on : Wednesday, November 3, 2021 - 6:36:01 AM
Long-term archiving on: : Tuesday, April 27, 2021 - 7:30:19 PM


Files produced by the author(s)



Thomas Genet, Thomas Jensen, Justine Sauvage. Termination of Ethereum’s Smart Contracts. SECRYPT 2020 - 17th International Conference on Security and Cryptography, Jul 2020, Lieusaint - Paris / Virtual, France. pp.39-51, ⟨10.5220/0009564100390051⟩. ⟨hal-03122008⟩



Les métriques sont temporairement indisponibles