软件学报

作者：陈锦富，冯乔伟，蔡赛华，施登洲，Rexford Nii Ayitey SOSU

单位：陈锦富，江苏大学 计算机科学与通信工程学院, 江苏 镇江 212013;江苏省工业网络安全技术重点实验室 (江苏大学), 江苏 镇江 21201311,冯乔伟，江苏大学 计算机科学与通信工程学院, 江苏 镇江 212013;江苏省工业网络安全技术重点实验室 (江苏大学), 江苏 镇江 21201302,蔡赛华，江苏大学 计算机科学与通信工程学院, 江苏 镇江 212013;江苏省工业网络安全技术重点实验室 (江苏大学), 江苏 镇江 21201303,施登洲，江苏大学 计算机科学与通信工程学院, 江苏 镇江 212013;江苏省工业网络安全技术重点实验室 (江苏大学), 江苏 镇江 21201304,Rexford Nii Ayitey SOSU，江苏大学 计算机科学与通信工程学院, 江苏 镇江 212013;Faculty of Computing and Information Systems, Ghana Communication Technology University, Accra 23321, Ghana05

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

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

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

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期