关键词:
区块链
智能合约
漏洞检测
模型检测
形式化验证
摘要:
区块链技术具备分布式特点,而且数据无法被修改,因此,智能合约一旦部署便难以修改,这可能引发严重的安全风险.重点研究区块链环境下的智能合约安全问题,建立了一个区块链智能合约的漏洞检测模型.该模型将智能合约的行为模式转换成Promela形式化建模语言,并融合了区块链交易序列的随机性及Gas费用机制的约束状况,用线性时序逻辑LTL来描述安全性需求和公平性标准,最后借助SPIN工具执行自动化验证.实验结果显示,该模型可以准确找出重入攻击、整数溢出、权限控制等方面的安全漏洞,为提升区块链智能合约的安全性给予了关键的理论支撑和实际参照.