Securing smart contracts in blockchain

Jaturong Kongmanee, Phongphun Kijsanayothin, Rattikorn Hewett

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

1 Scopus citations

Abstract

Blockchain is an emerging technology that underlies creation and exchange of the digital assets, including cryptocurrency such as Bitcoin and Ether, without the need for a central authority. It provides a public ledger for recording sequence of transactions in blocks that are linked as a chain. Smart contracts are computer programs governing participant agreements that are automatically enforced by consensus protocols in the blockchain. Together, blockchain and smart contracts revolutionize efficient transaction stores, services and workflows that work even among distrusting participants and without a trusted authority. Unfortunately, like most software, smart contracts are vulnerable as evidenced by a recent Decentralized Autonomous Organization (DAO) attack that lost cryptocurrency then-valued about $ 60 million. Correctness of executions alone is not sufficient to guarantee security of smart contracts. This paper addresses how we can apply model checking, a well-established formal verification technique, to help alleviate security issues in smart contract development. Most existing studies have focused on verification of smart contracts on a specific language and specific platform. Smart contracts may have hidden operational side effects that impact software behaviors. Thus, applying model checking to smart contracts is not necessarily straightforward. This paper presents a general technique for building the core functional models applicable for model checking to identify all possible executions that lead to security breaches. It also shows how resulting executions can be systematically analyzed to help identify security issues. The models are language and system independent in that they can represent any smart contract in any language or any platform. We illustrate and evaluate the technique with a widely used example of a smart contract in a financial system along with experimental results using a well-known model checker, NuSMV in various scenarios.

Original languageEnglish
Title of host publicationProceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages69-76
Number of pages8
ISBN (Electronic)9781728141367
DOIs
StatePublished - Nov 2019
Event34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019 - San Diego, United States
Duration: Nov 10 2019Nov 15 2019

Publication series

NameProceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019

Conference

Conference34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019
Country/TerritoryUnited States
CitySan Diego
Period11/10/1911/15/19

Keywords

  • Blockchain
  • Formal methods
  • Model checking
  • Smart contract

Fingerprint

Dive into the research topics of 'Securing smart contracts in blockchain'. Together they form a unique fingerprint.

Cite this