Vulnerability Detection Model for Blockchain Systems Based on Formal Method

被引：0
|
作者：
Chen J.-F. [1 ,2 ]
Feng Q.-W. [1 ,2 ]
Cai S.-H. [1 ,2 ]
Shi D.-Z. [1 ,2 ]
Sosu R.N.A. [1 ,3 ]
机构：
[1] School of Computer Science and Communication Engineering, Jiangsu University, Zhenjiang
[2] Jiangsu Key Laboratory of Security Technology for Industrial Cyberspace (Jiangsu University), Zhenjiang
[3] Faculty of Computing and Information Systems, Ghana Communication Technology University, Accra
来源：
Ruan Jian Xue Bao/Journal of Software | 2024年 / 35卷 / 09期
关键词：
blockchain system; BPEL flow; formal verification; security factor; vulnerability detection model;
D O I：
10.13328/j.cnki.jos.007133
中图分类号：
学科分类号：
摘要：
As blockchain technology is widely employed in all walks of life, the architecture of blockchain systems becomes increasingly more complex, which raises the number of security issues. At present, traditional vulnerability detection methods such as fuzz testing and symbol execution are adopted in blockchain systems, but these techniques cannot detect unknown vulnerabilities effectively. To improve the security of blockchain systems, this study proposes a vulnerability detection model for blockchain systems (VDMBS) based on the formal method. This model integrates multiple security factors including system migration state, security property and trust relationship among nodes, and provides a vulnerability model building method based on business process execution language (BPEL). Finally, the effectiveness of the proposed vulnerability detection model is verified on a blockchain-based e-voting election system by NuSMV, and the experimental results show that compared with five existing formal testing tools, the proposed VDMBS model can detect more blockchain system logic vulnerabilities and smart contract vulnerabilities. © 2024 Chinese Academy of Sciences. All rights reserved.
引用
收藏
相关论文
共 56 条
  • [1] Latif SA, Wen FBX, Iwendi C, Wang LLF, Mohsin SM, Han ZY, Band SS., AI-empowered, blockchain and SDN integrated security architecture for IoT network of cyber physical systems, Computer Communications, 181, pp. 274-283, (2022)
  • [2] Kumar A, Singh AK, Ahmad I, Singh PK, Anushree, Verma PK, Alissa KA, Bajaj M, Rehman AU, Tag-Eldin E., A novel decentralized blockchain architecture for the preservation of privacy and data security against cyberattacks in healthcare, Sensors, 22, 15, (2022)
  • [3] Taylor PJ, Dargahi T, Dehghantanha A, Parizi RM, Choo KKR., A systematic literature review of blockchain cyber security, Digital Communications and Networks, 6, 2, pp. 147-156, (2020)
  • [4] Liu ZY, Luong NC, Wang WB, Niyato D, Wang P, Liang YC, Kim DI., A survey on blockchain: A game theoretical perspective, IEEE Access, 7, pp. 47615-47643, (2019)
  • [5] Vasek M, Thornton M, Moore T., Empirical analysis of denial-of-service attacks in the Bitcoin ecosystem, Proc. of the 2014 Financial Cryptography and Data Security: FC 2014 Workshops, BITCOIN and WAHC 2014, pp. 57-71, (2014)
  • [6] Bhutta MNM, Khwaja AA, Nadeem A, Ahmad HF, Khan MK, Hanif MA, Song HB, Alshamari M, Cao Y., A survey on blockchain technology: Evolution, architecture and security, IEEE Access, 9, pp. 61048-61073, (2021)
  • [7] Khan MA, Salah K., IoT security: Review, blockchain solutions, and open challenges, Future Generation Computer Systems, 82, pp. 395-411, (2018)
  • [8] Tsankov P, Dan A, Drachsler-Cohen D, Gervais A, Buenzli F, Vechev M., Securify: Practical security analysis of smart contracts, Proc. of the 2018 ACM SIGSAC Conf. on Computer and Communications Security, pp. 67-82, (2018)
  • [9] Qu C, Tao M, Zhang J, Hong XY, Yuan RF., Blockchain based credibility verification method for IoT entities, Security and Communication Networks, 2018, (2018)
  • [10] Luu L, Chu DH, Olickel H, Saxena P, Hobor A., Making smart contracts smarter, Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security, pp. 254-269, (2016)
123456