TY - GEN
T1 - Securing smart contracts in blockchain
AU - Kongmanee, Jaturong
AU - Kijsanayothin, Phongphun
AU - Hewett, Rattikorn
N1 - Publisher Copyright:
© 2019 IEEE.
PY - 2019/11
Y1 - 2019/11
N2 - 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.
AB - 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.
KW - Blockchain
KW - Formal methods
KW - Model checking
KW - Smart contract
UR - http://www.scopus.com/inward/record.url?scp=85079287739&partnerID=8YFLogxK
U2 - 10.1109/ASEW.2019.00032
DO - 10.1109/ASEW.2019.00032
M3 - Conference contribution
AN - SCOPUS:85079287739
T3 - Proceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019
SP - 69
EP - 76
BT - Proceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 34th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW 2019
Y2 - 10 November 2019 through 15 November 2019
ER -