微信服务号

微信订阅号

2025年5月1日 21:21 星期四
首页 > 过刊浏览>2024年第35卷第9期 >4193-4217. DOI:10.13328/j.cnki.jos.007133
PDF HTML阅读 XML下载 导出引用 引用提醒
基于形式化方法的区块链系统漏洞检测模型
作者:
作者简介:

陈锦富(1978－), 男, 博士, 教授, 博士生导师, CCF杰出会员, 主要研究领域为软件测试, 软件安全, 可信软件;冯乔伟(1998－), 男, 硕士生, CCF学生会员, 主要研究领域为软件安全测试, 区块链漏洞检测. ;蔡赛华(1990－), 男, 博士, 讲师, CCF专业会员, 主要研究领域为恶意流量检测, 异常数据检测, 软件安全测试;施登洲(1997－), 男, 硕士, 主要研究领域为软件安全测试, 区块链漏洞检测. ;Rexford Nii Ayitey SOSU(1986－), 男, 博士生, 主要研究领域区块链漏洞检测, 人工智能, 物联网, 云计算.

通讯作者:

蔡赛华, E-mail: caisaih@ujs.edu.cn

基金项目:

国家重点研发计划(2020YFB1005501); 国家自然科学基金(62172194, 62202206, U1836116); 江苏省自然科学基金(BK20220515); 中国博士后科学基金(2023T160275); 江苏省自然科学基金前沿技术项目(BK20202001); 江苏省青蓝工程


Vulnerability Detection Model for Blockchain Systems Based on Formal Method
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [60]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    随着区块链技术在各行各业的广泛应用, 区块链系统的架构变得越来越复杂, 这也增加了安全问题的数量. 目前, 在区块链系统中采用了模糊测试、符号执行等传统的漏洞检测方法, 但这些技术无法有效检测出未知的漏洞. 为了提高区块链系统的安全性, 提出基于形式化方法的区块链系统漏洞检测模型VDMBS (vulnerability detection model for blockchain systems), 所提模型综合系统迁移状态、安全规约和节点间信任关系等多种安全因素, 同时提供基于业务流程执行语言BPEL (business process execution language)的漏洞模型构建方法. 最后, 用NuSMV在基于区块链的电子投票选举系统上验证所提出的漏洞检测模型的有效性, 实验结果表明, 与现有的5种形式化测试工具相比, 所提出的VDMBS模型能够检测出更多的区块链系统业务逻辑漏洞和智能合约漏洞.

    Abstract:

    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.

    参考文献
    [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, 2022, 181: 274–283.
    [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, 2022, 22(15): 5921.
    [3] Taylor PJ, Dargahi T, Dehghantanha A, Parizi RM, Choo KKR. A systematic literature review of blockchain cyber security. Digital Communications and Networks, 2020, 6(2): 147–156.
    [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, 2019, 7: 47615–47643.
    [5] Vasek M, Thornton M, Moore T. Empirical analysis of denial-of-service attacks in the Bitcoin ecosystem. In: Proc. of the 2014 Financial Cryptography and Data Security: FC 2014 Workshops, BITCOIN and WAHC 2014. Christ Church: Springer, 2014. 57–71. [doi: 10.1007/978-3-662-44774-1_5]
    [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, 2021, 9: 61048–61073.
    [7] Khan MA, Salah K. IoT security: Review, blockchain solutions, and open challenges. Future Generation Computer Systems, 2018, 82: 395–411.
    [8] Tsankov P, Dan A, Drachsler-Cohen D, Gervais A, Buenzli F, Vechev M. Securify: Practical security analysis of smart contracts. In: Proc. of the 2018 ACM SIGSAC Conf. on Computer and Communications Security. Toronto: ACM, 2018. 67–82.
    [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: 7817614.
    [10] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In: Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security. Vienna: ACM, 2016. 254–269. [doi: 10.1145/2976749.2978309]
    [11] Li PR, Li SS, Ding MJ, Yu JP, Zhang H, Zhou X, Li JY. A vulnerability detection framework for hyperledger fabric smart contracts based on dynamic and static analysis. In: Proc. of the 26th Int’l Conf. on Evaluation and Assessment in Software Engineering. Gothenburg: ACM, 2022. 366–374. [doi: 10.1145/3530019.3531342]
    [12] Li JX, Wu JG, Chen L. Block-secure: Blockchain based scheme for secure P2P cloud storage. Information Sciences, 2018, 465: 219–231.
    [13] Alharbi T. Deployment of blockchain technology in software defined networks: A survey. IEEE Access, 2020, 8: 9146–9156.
    [14] Fung CJ, Zhang J, Aib I, Boutaba R. Dirichlet-based trust management for effective collaborative intrusion detection networks. IEEE Trans. on Network and Service Management, 2011, 8(2): 79–91.
    [15] Zhuang Y, Liu ZG, Qian P, Liu Q, Wang X, He QM. Smart contract vulnerability detection using graph neural networks. In: Proc. of the 29th Int’l Joint Conf. on Artificial Intelligence. Yokohama, 2020. 3283–3290.
    [16] Afzaal H, Imran M, Janjua MU, Gochhayat SP. Formal modeling and verification of a blockchain-based crowdsourcing consensus protocol. IEEE Access, 2022, 10: 8163–8183.
    [17] Ribeiro M, Ad?o P, Mateus P. Formal verification of Ethereum smart contracts using Isabelle/HOL. In: Logic, Language, and Security: Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday. Switzerland: Springer Int’l Publishing, 2020. 71–97. [doi: 10.1007/978-3-030-62077-6_7]
    [18] Grishchenko I, Maffei M, Schneidewind C. A semantic framework for the security analysis of Ethereum smart contracts. In: Proc. of the 7th Int’l Conf. on Principles of Security and Trust. Thessaloniki: Springer, 2018. 243–269. [doi: 10.1007/978-3-319-89722-6_10]
    [19] Krupp J, Rossow C. TEETHER: Gnawing at Ethereum to automatically exploit smart contracts. In: Proc. of the 27th USENIX Conf. on Security Symp. Baltimore: USENIX Association, 2018. 1317–1333.
    [20] Feist J, Grieco G, Groce A. Slither: A static analysis framework for smart contracts. In: Proc. of the 2nd IEEE/ACM Int’l Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). Montreal: IEEE, 2019. 8–15.
    [21] Jiang B, Liu Y, Chan WK. ContractFuzzer: Fuzzing smart contracts for vulnerability detection. In: Proc. of the 33rd ACM/IEEE Int’l Conf. on Automated Software Engineering. Montpellier: ACM, 2018. 259–269. [doi: 10.1145/3238147.3238177]
    [22] Wang W, Song JJ, Xu GQ, Li YD, Wang H, Su CH. ContractWard: Automated vulnerability detection models for Ethereum smart contracts. IEEE Trans. on Network Science and Engineering, 2021, 8(2): 1133–1144.
    [23] Norta A, Matulevi?ius R, Leiding B. Safeguarding a formalized blockchain-enabled identity-authentication protocol by applying security risk-oriented patterns. Computers & Security, 2019, 86: 253–269.
    [24] Matsuo SI. How formal analysis and verification add security to blockchain-based systems. In: Proc. of the 2017 Formal Methods in Computer Aided Design (FMCAD). Vienna: IEEE, 2017. 1–4. [doi: 10.23919/FMCAD.2017.8102228]
    [25] Chaudhary KC, Chand V, Fehnker A. Double-spending analysis of bitcoin. In: Proc. of the 24th Pacific Asia Conf. on Information Systems. Dubai, 2020. 210.
    [26] Kalra S, Goel S, Dhawan M, Sharma S. Zeus: Analyzing safety of smart contracts. In: Proc. of the 2018 Network and Distributed Systems Security (NDSS) Symp. San Diego, 2018. 1–12.
    [27] Geatti L, Gianola A, Gigante N. Linear temporal logic modulo theories over finite traces. In: Proc. of the 31st Int’l Joint Conf. on Artificial Intelligence. Vienna, 2022. 2641–2647.
    [28] Ye X, Shi JQ, Huang YH, Li Q, Wei HS, Chen XY. Parallel computational tree logic model-checking on pushdown systems. Concurrency and Computation: Practice and Experience, 2022, 34(23): e7173.
    [29] Doostali S, Babamir SM, Javani M. Using a process algebra interface for verification and validation of UML statecharts. Computer Standards & Interfaces, 2023, 86: 103739.
    [30] Walkinshaw N, Hierons RM. Modelling second-order uncertainty in state machines. IEEE Trans. on Software Engineering, 2023, 49(5): 3261–3276.
    [31] Grossman S, Abraham I, Golan-Gueta G, Michalevsky Y, Rinetzky N, Sagiv M, Zohar Y. Online detection of effectively callback free objects with applications to smart contracts. Proc. of the ACM on Programming Languages, 2017, 2: 48.
    [32] Schneidewind C, Grishchenko I, Scherer M, Maffei M. eThor: Practical and provably sound static analysis of Ethereum smart contracts. In: Proc. of the 2020 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2020. 621–640. [doi: 10.1145/3372297.3417250]
    [33] Shaikh E, Al-Ali AR, Muhammad S, Mohammad N, Aloul F. Security analysis of a digital twin framework using probabilistic model checking. IEEE Access, 2023, 11: 26358–26374.
    [34] Waldmann U, Tourret S, Robillard S, Blanchette J. A comprehensive framework for saturation theorem proving. Journal of Automated Reasoning, 2022, 66(4): 499–539.
    [35] Tempel S, Herdt V, Drechsler R. Specification-based symbolic execution for stateful network protocol implementations in IoT. IEEE Internet of Things Journal, 2023, 10(11): 9544–9555.
    [36] Wang D, Dou WS, Gao Y, Wu CN, Wei J, Huang T. Model checking guided testing for distributed systems. In: Proc. of the 18th European Conf. on Computer Systems. Rome: ACM, 2023. 127–143. [doi: 10.1145/3552326.3587442]
    [37] Khan KM, Arshad J, Khan MM. Empirical analysis of transaction malleability within blockchain-based e-voting. Computers & Security, 2021, 100: 102081.
    [38] Zhang SJ, Lee JH. Double-spending with a Sybil attack in the Bitcoin decentralized network. IEEE Trans. on Industrial Informatics, 2019, 15(10): 5715–5722.
    [39] Shah Z, Ullah I, Li HL, Levula A, Khurshid K. Blockchain based solutions to mitigate distributed denial of service (DDoS) attacks in the Internet of Things (IoT): A survey. Sensors, 2022, 22(3): 1094.
    [40] Sahay R, Geethakumari G, Mitra B. A novel blockchain based framework to secure IoT-LLNs against routing attacks. Computing, 2020, 102(11): 2445–2470.
    [41] Tran M, Shenoi A, Kang MS. On the routing-aware peering against network-eclipse attacks in Bitcoin. In: Proc. of the 30th USENIX Security Symp. (USENIX Security 2021). 2021. 1253–1270.
    [42] Du Y, Wang Z, Li J, Shi L, Jayakody DNK, Chen Q, Chen W, Han Z. Blockchain-aided edge computing market: Smart contract and consensus mechanisms. IEEE Trans. on Mobile Computing, 2023, 22(6): 3193–3208.
    [43] Wang JL, Liu Q, Song BY. Blockchain-based multi-malicious double-spending attack blacklist management model. The Journal of Supercomputing, 2022, 78(12): 14726–14755.
    [44] Hafid A, Hafid AS, Samih M. A tractable probabilistic approach to analyze Sybil attacks in sharding-based blockchain protocols. IEEE Trans. on Emerging Topics in Computing, 2023, 11(1): 126–136.
    [45] Piantadosi V, Rosa G, Placella D, Scalabrino S, Oliveto R. Detecting functional and security-related issues in smart contracts: A systematic literature review. Software: Practice and Experience, 2023, 53(2): 465–495.
    [46] 钱鹏, 刘振广, 何钦铭, 黄步添, 田端正, 王勋. 智能合约安全漏洞检测技术研究综述. 软件学报, 2022, 33(8): 3059–3085. http://www.jos.org.cn/1000-9825/6375.htm
    Qian P, Liu ZG, He QM, Huang BT, Tian DZ, Wang X. Smart contract vulnerability detection technique: A survey. Ruan Jian Xue Bao/Journal of Software, 2022, 33(8): 3059–3085 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6375.htm
    [47] 董伟良, 刘哲, 刘逵, 黎立, 葛春鹏, 黄志球. 智能合约漏洞检测技术综述. 软件学报, 2024, 35(1): 38–62. http://www.jos.org.cn/1000-9825/6810.htm
    Dong WL, Liu Z, Liu K, Li L, Ge CP, Huang ZQ. Survey on vulnerability detection technology of smart contracts. Ruan Jian Xue Bao/Journal of Software, 2024, 35(1): 38–62 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6810.htm
    [48] 韩璇, 袁勇, 王飞跃. 区块链安全问题: 研究现状与展望. 自动化学报, 2019, 45(1): 206–225.
    Han X, Yuan Y, Wang FY. Security problems on blockchain: The state of the art and future trends. Acta Automatica Sinica, 2019, 45(1): 206–225 (in Chinese with English abstract).
    [49] 冯萍慧, 连一峰, 戴英侠, 鲍旭华. 基于可靠性理论的分布式系统脆弱性模型. 软件学报, 2006, 17(7): 1633–1640. http://www.jos.org.cn/1000-9825/17/1633.htm
    Feng PH, Lian YF, Dai YX, Bao XH. A vulnerability model of distributed systems based on reliability theory. Ruan Jian Xue Bao/Journal of Software, 2006, 17(7): 1633–1640 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/1633.htm
    [50] Gao HH, Zhang YD, Miao HK, Barroso RJD, Yang XX. SDTIOA: Modeling the timed privacy requirements of IoT service composition: A user interaction perspective for automatic transformation from BPEL to timed automata. Mobile Networks and Applications, 2021, 26(6): 2272–2297.
    [51] Cimatti A, Clarke E, Giunchiglia F, Roveri M. NuSMV: A new symbolic model checker. Int’l Journal on Software Tools for Technology Transfer, 2000, 2(4): 410–425.
    [52] Hjálmarsson FT, Hreiearsson GK, Hamdaqa M, Hjálmtysson G. Blockchain-based e-voting system. In: Proc. of the 11th IEEE Int’l Conf. on Cloud Computing (CLOUD). San Francisco: IEEE, 2018. 983–986. [doi: 10.1109/CLOUD.2018.00151]
    [53] Marcilla B. Polygon-NFT-marketplace. 2022. https://github.com/ikcoin/Polygon-NFT-marketplace
    [54] Lobo K. AuthentiFi. 2022. https://github.com/kylelobo/AuthentiFi
    [55] Atraura Blockchain. scts. 2017. https://github.com/AtrauraBlockchain/scts
    [56] yashverma9. AI blockchain electronic health records management system. 2020. https://github.com/yashverma9/AI-Blockchain-Electronic-Health-Records-Management-System
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

陈锦富,冯乔伟,蔡赛华,施登洲,Rexford Nii Ayitey SOSU.基于形式化方法的区块链系统漏洞检测模型.软件学报,2024,35(9):4193-4217

复制
分享
文章指标
  • 点击次数:930
  • 下载次数: 3145
  • HTML阅读次数: 1018
  • 引用次数: 0
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 在线发布日期: 2024-01-05
  • 出版日期: 2024-09-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19894438位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号