Proving conditional termination for smart contracts

Ton Chanh Le, Lei Xu, Lin Chen, Weidong Shi

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

9 Scopus citations

Abstract

Termination of smart contracts is crucial for any blockchain system's security and consistency, especially for those supporting Turing-complete smart contract languages. Resource-constrained blockchain systems, like Ethereum and Hyperledger Fabric, could prevent smart contracts from terminating properly when the preallocated resources are not sufficient. The Zen system utilizes the dependent type system of the programming language F to prove the termination of smart contracts for all inputs during compilation time. Since the smart contract execution usually depends on the current blockchain state and user inputs, this approach is not always successful. In this work, we propose a lazy approach by statically proving conditional termination and non-termination of a smart contract to determine input conditions under which the contract terminates or not. Prior to the execution of the smart contract, the proof-carrying blockchain system will check that its current state and the contract's input satisfy the termination conditions in order to determine if the contract is qualified (i.e., eventually terminating) to run on the chain.

Original languageEnglish
Title of host publicationBCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018
PublisherAssociation for Computing Machinery, Inc
Pages57-59
Number of pages3
ISBN (Electronic)9781450357586
DOIs
StatePublished - May 22 2018
Event2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018 - Incheon, Korea, Republic of
Duration: Jun 4 2018 → …

Publication series

NameBCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018

Conference

Conference2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018
Country/TerritoryKorea, Republic of
CityIncheon
Period06/4/18 → …

Keywords

  • Blockchain
  • Non-termination
  • Smart contracts
  • Termination

Fingerprint

Dive into the research topics of 'Proving conditional termination for smart contracts'. Together they form a unique fingerprint.

Cite this