Proving conditional termination for smart contracts

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

doi:10.1145/3205230.3205239

Proving conditional termination for smart contracts

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 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 language	English
Title of host publication	BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018
Publisher	Association for Computing Machinery, Inc
Pages	57-59
Number of pages	3
ISBN (Electronic)	9781450357586
DOIs	https://doi.org/10.1145/3205230.3205239
State	Published - May 22 2018
Event	2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018 - Incheon, Korea, Republic of Duration: Jun 4 2018 → …

Publication series

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

Conference

Conference	2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018
Country/Territory	Korea, Republic of
City	Incheon
Period	06/4/18 → …

Keywords

Blockchain
Non-termination
Smart contracts
Termination

Access to Document

10.1145/3205230.3205239

Cite this

Le, T. C., Xu, L., Chen, L., & Shi, W. (2018). Proving conditional termination for smart contracts. In BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018 (pp. 57-59). (BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018). Association for Computing Machinery, Inc. https://doi.org/10.1145/3205230.3205239

Le, Ton Chanh ; Xu, Lei ; Chen, Lin et al. / Proving conditional termination for smart contracts. BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018. Association for Computing Machinery, Inc, 2018. pp. 57-59 (BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018).

@inproceedings{d271c2cfa57a49fa99d4c50a17099acf,

title = "Proving conditional termination for smart contracts",

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.",

keywords = "Blockchain, Non-termination, Smart contracts, Termination",

author = "Le, {Ton Chanh} and Lei Xu and Lin Chen and Weidong Shi",

note = "Publisher Copyright: {\textcopyright} 2018 Association for Computing Machinery.; 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018 ; Conference date: 04-06-2018",

year = "2018",

month = may,

day = "22",

doi = "10.1145/3205230.3205239",

language = "English",

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

publisher = "Association for Computing Machinery, Inc",

pages = "57--59",

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

}

Le, TC, Xu, L, Chen, L & Shi, W 2018, Proving conditional termination for smart contracts. in BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018. BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018, Association for Computing Machinery, Inc, pp. 57-59, 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018, Incheon, Korea, Republic of, 06/4/18. https://doi.org/10.1145/3205230.3205239

Proving conditional termination for smart contracts. / Le, Ton Chanh; Xu, Lei; Chen, Lin et al.
BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018. Association for Computing Machinery, Inc, 2018. p. 57-59 (BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Proving conditional termination for smart contracts

AU - Le, Ton Chanh

AU - Xu, Lei

AU - Chen, Lin

AU - Shi, Weidong

PY - 2018/5/22

Y1 - 2018/5/22

N2 - 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.

AB - 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.

KW - Blockchain

KW - Non-termination

KW - Smart contracts

KW - Termination

UR - http://www.scopus.com/inward/record.url?scp=85049414584&partnerID=8YFLogxK

U2 - 10.1145/3205230.3205239

DO - 10.1145/3205230.3205239

M3 - Conference contribution

AN - SCOPUS:85049414584

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

SP - 57

EP - 59

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

PB - Association for Computing Machinery, Inc

T2 - 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, BCC 2018

Y2 - 4 June 2018

ER -

Le TC, Xu L, Chen L, Shi W. Proving conditional termination for smart contracts. In BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018. Association for Computing Machinery, Inc. 2018. p. 57-59. (BCC 2018 - Proceedings of the 2nd ACM Workshop on Blockchains, Cryptocurrencies, and Contracts, Co-located with ASIA CCS 2018). doi: 10.1145/3205230.3205239

Proving conditional termination for smart contracts

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this