摘要
智能合约是运行在区块链上的计算机程序,在扩展区块链功能、实现复杂应用的同时,其潜在的安全漏洞也带来巨大风险.基于符号执行的安全漏洞检测方法具有精确度高、可生成能复现漏洞的测试用例等优势.然而,随着代码规模的增大,符号执行技术容易受到路径爆炸、约束求解开销过大等问题的影响.为此,提出一种基于目标制导符号执行的智能合约安全漏洞检测方法,首先将静态分析工具或人工标注的漏洞语句作为目标,分析目标依赖语句,补充事务序列以添加相关变量的符号约束.然后,基于智能合约字节码构建控制流图,定位目标语句以及目标依赖语句所在的基本块,剪枝控制流图以生成制导信息.最后,根据制导信息优化符号执行的路径探索策略,减少需要分析的基本块数量以及求解路径条件的时间,最终高效地检测目标语句是否存在安全漏洞,并输出可复现漏洞的测试用例.基于上述思路实现Smart-Target原型工具,在SB Curated数据集上与符号执行工具Mythril进行对比.实验结果表明Smart-Target在安全漏洞检测和漏洞复现场景分别减少60.76%和92.16%的时间开销,大幅提高符号执行效率.此外,Smart-Target通过分析目标依赖语句使其多检测到22.02%的安全漏洞,有效提升了漏洞检测能力.
Smart contracts are computer programs running on blockchain platforms,which extend the functionality of the blockchain and enable complex applications.However,the potential security vulnerabilities of smart contracts can lead to significant financial losses.Symbolic execution-based security vulnerability detection methods offer advantages such as high accuracy and the ability to generate test cases that can reproduce vulnerabilities.Nevertheless,as the code size increases,symbolic execution faces challenges such as path explosion and excessive constraint-solving overhead.To address those issues,a novel approach for detecting smart contract security vulnerabilities through target-guided symbolic execution is proposed.First,vulnerable statements identified by static analysis tools or manually are treated as targets.The statements that depend on these target statements are analyzed,and the transaction sequence is augmented with symbolic constraints for the relevant variables.Second,the control flow graph(CFG)is constructed based on the bytecode of smart contracts,with the basic blocks containing the target statements and the dependentstatements located.The CFG is then pruned to generate guidance information.Third,path exploration in symbolic execution is optimized by reducing the number of basic blocks to be analyzed and reducing the time required for solving path constraints.With the guidance information,vulnerabilities are efficiently detected,and test cases capable of reproducing the vulnerabilities are generated.Based on this approach,a prototype tool named Smart-Target is developed.Experiments conducted on the SB Curated dataset in comparison with the symbolic execution tool,Mythril,demonstrate that Smart-Target reduces time overheads by 60.76%and 92.16%in vulnerability detection and replication scenarios,respectively.In addition,the analysis of target statementdependencies enhances vulnerability detection capability by identifying 22.02%more security vulnerabilities.
作者
杨慧文
崔展齐
陈翔
郑丽伟
刘建宾
YANG Hui-Wen;CUI Zhan-Qi;CHEN Xiang;ZHENG Li-Wei;LIU Jian-Bin(Computer School,Beijing Information Science and Technology University,Beijing 100101,China;School of Information Science and Technology,Nantong University,Nantong 226019,China)
出处
《软件学报》
北大核心
2025年第12期5755-5779,共25页
Journal of Software
基金
江苏省前沿引领技术基础研究专项(BK202002001)
北京信息科技大学“勤信人才”培育计划(QXTCP B202406)
北京控制工程研究所高可信嵌入式软件工程技术实验室开放基金(LHCESET202307)。
关键词
智能合约
符号执行
目标制导测试
安全漏洞检测
安全漏洞复现
smart contract
symbolic execution
target-guided testing
security vulnerability detection
security vulnerability reproduction
