基于形式化方法的区块链系统漏洞检测模型  

Vulnerability Detection Model for Blockchain Systems Based on Formal Method

作　　者：陈锦富[1,2] 冯乔伟 蔡赛华 施登洲 Rexford Nii Ayitey SOSU CHEN Jin-Fu;FENG Qiao-Wei;CAI Sai-Hua;SHI Deng-Zhou;Rexford Nii Ayitey SOSU(School of Computer Science and Communication Engineering,Jiangsu University,Zhenjiang 212013,China;Jiangsu Key Laboratory of Security Technology for Industrial Cyberspace(Jiangsu University),Zhenjiang 212013,China;Faculty of Computing and Information Systems,Ghana Communication Technology University,Accra 23321,Ghana)

机构地区：[1]江苏大学计算机科学与通信工程学院,江苏镇江212013 [2]江苏省工业网络安全技术重点实验室(江苏大学),江苏镇江212013 [3]Faculty of Computing and Information Systems,Ghana Communication Technology University,Accra 23321,Ghana

出　　处：《软件学报》2024年第9期4193-4217,共25页Journal of Software

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

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

关 键 词：区块链系统 安全因素 漏洞检测模型 形式化验证 BPEL流程 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]