TY - GEN
T1 - Formal verification of smart contracts from the perspective of concurrency
AU - Qu, Meixun
AU - Huang, Xin
AU - Chen, Xu
AU - Wang, Yi
AU - Ma, Xiaofeng
AU - Liu, Dawei
N1 - Publisher Copyright:
© 2018, Springer Nature Switzerland AG.
PY - 2018
Y1 - 2018
N2 - Blockchain is an emerging technology with broad applications. As an important application of the blockchain, smart contracts can formulate trading rules to manage thousands of virtual currencies. Nowadays, the IoT (Internet of Things) combined with blockchain has become a new trend and smart contract can implement different transaction demands for IoT-blockchain systems. Once there exits vulnerability in the smart contract program, the security of the virtual currency will not be guaranteed. However, ensuring the security of smart contracts is never an easy task. On the one hand, existing smart contracts cannot identify fake users or malicious programs, which is difficult to be regulated at present; on the other hand, smart contracts involving in multiple trading users are very similar to shared-memory concurrent programs. To deal with these problems, this study uses formal verification methods, adopting the Communicating Sequence Processes (CSP) theory to formally model concurrent programs. Then the FDR (Failure Divergence Refinement), a refinement checker or model checker for CSP, is utilized to successfully detect the vulnerability regarding concurrency in one smart contract public in Ethereum. The results show the potential advantage of using CSP and FDR tool to check the vulnerability in smart contracts especially from the perspective of concurrency.
AB - Blockchain is an emerging technology with broad applications. As an important application of the blockchain, smart contracts can formulate trading rules to manage thousands of virtual currencies. Nowadays, the IoT (Internet of Things) combined with blockchain has become a new trend and smart contract can implement different transaction demands for IoT-blockchain systems. Once there exits vulnerability in the smart contract program, the security of the virtual currency will not be guaranteed. However, ensuring the security of smart contracts is never an easy task. On the one hand, existing smart contracts cannot identify fake users or malicious programs, which is difficult to be regulated at present; on the other hand, smart contracts involving in multiple trading users are very similar to shared-memory concurrent programs. To deal with these problems, this study uses formal verification methods, adopting the Communicating Sequence Processes (CSP) theory to formally model concurrent programs. Then the FDR (Failure Divergence Refinement), a refinement checker or model checker for CSP, is utilized to successfully detect the vulnerability regarding concurrency in one smart contract public in Ethereum. The results show the potential advantage of using CSP and FDR tool to check the vulnerability in smart contracts especially from the perspective of concurrency.
KW - Blockchain
KW - CSP theory
KW - Concurrency
KW - FDR
KW - Smart contracts
UR - http://www.scopus.com/inward/record.url?scp=85058632425&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-05764-0_4
DO - 10.1007/978-3-030-05764-0_4
M3 - Conference Proceeding
AN - SCOPUS:85058632425
SN - 9783030057633
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 32
EP - 43
BT - Smart Blockchain - 1st International Conference, SmartBlock 2018, Proceedings
A2 - Qiu, Meikang
PB - Springer Verlag
T2 - 1st International Conference on Smart Blockchain, SmartBlock 2018
Y2 - 10 December 2018 through 12 December 2018
ER -