关键路径预搜索的符号执行智能合约漏洞检测.pdf

DOI:10.3969/297.2024.02.016Mar.2024Electronics and Information EngineeringJOURNALOF APPLIEDSCIENCES2024年3 月Vol.42No.2第42 卷第2 期应用科报学学关键路径预搜索的符号执行智能合约漏洞检测王泽旭包1,2,3，文斌1,31.海南师范大学数据科学与智慧教育教育部重点实验室，海南海口57 11582.中山大学软件工程学院，广东珠海519 0 8 23.海南师范大学信息科学技术学院，海南海口57 1158摘要：针对传统符号执行在不必要、不相关的路径上消耗大量时间与资源，效率低等问题，提出了利用静态检测预扫描智能合约关键路径优化符号执行验证，避免非必要路径搜索增加的资源消耗，实现基于关键路径预搜索的符号执行。该方法与现有主流检测工具进行对比实验，结果显示：Gas耗尽拒绝服务漏洞覆盖率达9 8%，检测准确度为8 4.3%，远高于均值37.2%；对存储覆盖漏洞合约的全覆盖，检测准确率为8 6.1%，验证了该方法的高效性与稳定性。关键词：智能合约；漏洞检测；符号执行；关键路径预搜索；区块链安全中图分类号：P751.1文章编号：0 2 55-8 2 9 7(2 0 2 4)0 2-0 36 4-11Smart Contract Vulnerability Detection of SymbolExecution with Critical Path Pre-searchingWANG Zexul,2,3,WEN Bin1,31.Key Laboratory of Data Science and Smart Education,Ministry of Education,Hainan Normal University,Haikou 571158,Hainan,China2.School of Software Engineering,Sun Yat-sen University,Zhuhai 519082,Guangdong,China3.School of Information Science and Technology,Hainan Normal University,Haikou571158,Hainan,ChinaAbstract:This paper proposes a pre-searching paths for symbolic execution method toguide the critical path symbol execution of scanning smart contract vulnerabilities throughstatic detection.This approach aims to avoid unnecessary resource consumption of pathsearch,thereby achieving accurate and fast smart contract vulnerability detection.Thismethod is compared with existing mainstream detection tools.The results show that theGas exhaustion denial of service vulnerability coverage reaches 98%,with a detection ac-curacy of 84.3%,which is far higher than the average value of 37.2%.Furthermore,the fullcoverage of storage coverage vulnerability contracts is realized with a detection accuracyof 86.1%,which validates the efficiency and stability of this method.收稿日期：2 0 2 2-0 8-14基金项目：国家自然科学基金（No.62362029）；海南省自然科学基金（No.623RC485）资助通信作者：文斌，教授，研究方向为区块链生态安全、数据安全。E-mail：b i n w e n h a i n n u.e d u.c n365第2 期王泽旭，等：关键路径预搜索的符号执行合约漏洞检测Keywords:smart contract,vulnerability detection,symbol execution,pre-search of criti-cal path,blockchain security智能合约的安全是影响区块链系统可靠性的重要因素 1，随着Defi、元宇宙等去中心化应用的普及，保证负责数字资产及权益分配的智能合约公平性至关重要 2-3 。智能合约的主要功能为在分布式运行环境中，实现公平、可靠的数字计算，完成链上状态的更新，它是整个分布式应用（decentralizedapplication，D A p p）的逻辑处理模块。由于区块链上数据具有公开透明等特点 4-5 ，DApp的数据处理逻辑完全暴露在区块链上，黑客利用合约漏洞盗取数字资产的攻击事件层出不穷，这严重影响软件的公平性。智能合约的代码安全漏洞检测是DApp开发中非常重要且不可或缺的环节 6 。目前对于智能合约的安全开发主要包含两部分重要工作：一是使用标准的智能合约代码库，例如OpenZepplin等；二是进行专业的安全漏洞的扫描。智能合约代码库由专业安全人员审计，可以在很大程度上避免攻击，但代码库的漏洞一旦被攻击，所带来的损失是不可计算的 7 。同时，使用代码库的合约也限制了智能合约的扩展和DApp应用功能的丰富性。因此，现存大部分DApp合约代码在合约代码库的基础上完善产品的功能设计，潜在增加了漏洞风险。另外，因受智能合约语言特性及专业安全审计要求高等因素影响，人工智能合约安全审计的费用较高。智能合约安全漏洞自动化检测的需求日益突出与迫切，是产业界和学术界一个重要的研究方向。Oyente8是最先使用符号执行进行漏洞检测的工具，由4个基本组件组成，包括CFG生成器、搜索器、核心分析和验证器模块。CFG生成器对智能合约进行初步分析，并建立了控制流程图。搜索器通过对每个基本块执行信息搜索，收集相关信息并用Z3求解器计算节点条件跳转，确定要分析的分支。核心分析利用搜索器收集的信息识别漏洞类型。最后，验证器会对核心分析模块的分析结果进行验证，消除假阳性的分析结果。总的来说，Oyente作为智能的漏洞检测工具，用字节码作为输入，动态探索程序控制流程图，并结合路径约束、变量等信息，来检测智能合约的漏洞。文献 9 提出了一种基于符号执行的新方法GasChecker来检测智能合约字节码中Gas效率低的编程模式，并将其定制为MapReduce编程模型来并行化，实现大量低Gas效率代码检测工作，提出了一种基于符号执行的智能合约字节码检测方法。通过将符号执行整合为MapReduce编程来并行化，并提出了一种新的基于反馈的负载平衡策略，以有效利用云资源。大量实验表明GasChecker具有良好的扩展性。实证研究表明，许多实时智能合约都包含各种低效代码。通过人工检验的方式，验证了在检测出的低效率代码中，误报只有2.5%，可靠性较强。现有检测方法存在的问题主要有：1）资源消耗过大智能合约的逻辑设计越来越复杂，代码行数增多，这导致符号执行检测工具面临资源过度消耗和路径爆炸等问题。2）创新性不足现有技术大多由传统软件漏洞检测领域的思想借鉴而来，缺乏针对性和创新性的智能合约安全漏洞检测工具，检测效果较差。3）单一技术能力不足智能合约是较新的语言，相关技术尚未成熟，产业闭环尚未建立，因此需要攻克众多技术难题，多技术融合的检测仍然需要很多工作。针对上述问题，本文提出一种针对区块链智能合约安全漏洞检测的符号执行改进方法，基于关键路径预搜索的符号执行（pre-searchingpaths for symbolic execution，PSSE），用静态检测对智能合约进行预搜索，确定出与检测漏洞相关的关键路径集合，在此基础上结合符第42 卷366应报学学科用号执行完成关键路径是否存在漏洞的验证工作。相比传统单一的符号执行方法，该方法可实现资源合理、有效的利用，具有良好的检测效果。1预搜索符号执行1.1符号执行符号执行是一种符号值代替程序的输入变量，用路径约束表示路径的方法 12-15 。若某一路径的路径约束有解，则确认该路径可抵达，验证漏洞是否存在。传统符号执行分为静态与动态符号执行，静态符号执行对程序的分支树进行分析，动态符号执行则是动态的执行搜索执行树的状态，两者主要的区别在于是否实际运行程序。检测策略源代码代码解析辅助分析符号执行输出结果代码建模约束求解漏洞分析过程图1符号执行检测漏洞流程Figure 1 Symbol execution vulnerability detection process结合源代码进行程序代码建模，生成具有不同程序特征的中间表示语言，如CFG、C G、ICFG等，这些中间语言的分支结构代表不同的执行路径。在此基础上，结合漏洞的检测策略实现动态符号执行，利用约束求解器求解路经约束的输入值，直到整个程序被遍历完成，获得整个执行树状态，完成漏洞检测的工作。1.2基于关键路径预搜索的符号执行本节主要借助混合符号执行 16 ，提出了PSSE，指导符号执行流程，避免不必要的无效路径搜索，提高检测效率、实现性能优化。PSSE将漏洞检测工作分为两个阶段：阶段I为关键路径搜索阶段；阶段II为验证阶段。阶段I关键路径搜索阶段主要采用静态检测的思想，在不运行程序的前提下，实现智能合约源代码的漏洞预扫描，减少时间消耗。如图2 中的阶段I部分所示，利用词法分析、语法分析、中间代码生成等结合区块链、智能合约等属性信息实现精确建模，生成中间语言SlithIR。在中间语言分析的基础上，恢复出一些高级的智能合约语义，如是否包含循环、循环内是否存在全局变量的读写等。结合智能合约漏洞的特点，编写漏洞的搜索策略。将漏洞检测工作分配为不同的任务Task，实现可以漏洞的初步扫描。最终，将漏洞类型、位置等信息整合生成符号执行的指导信息Result_A。阶段II结合指导信息进行测试，利用符号执行技术完成漏洞模式的匹配与检测。将阶段I产生的指导信息Result_A进行解析，生成相对应漏洞函数的调用信息传递给符号执行引擎。如图2 中的阶段II部分所示，符号执行会对漏洞函数的执行路径进行遍历并搜集路径约束，通过约束求解器寻找满足约束条件的输入值。若能在规定时间内找到输入值，则认定在满足特定属性约束条件下该漏洞路径可达，即漏洞存在，否则不存在。367第2 期王泽旭，关键路径预搜索合约漏洞检测CFG和CG变量写入和授权ContradTestIFunction/Statevariableswilten1Conditions onmsg sender1fooIlestmeTask_1工CFG和CG编译器指导信息电智能合约复杂语义合约存储状态是否继承漏洞1 function_1Task_2权限界定漏洞2-function_2漏洞n-function_n智能合约源码ASTSSA生成Result_A信息数据依赖关系数据依赖关系数据依赖关系Task_nFunctionfoo(uint256)FuncionTestfooluint256)执行策略搜素Variable/DependenciesIRSV_1(uint256)=*(ly_17)Expresson.2.vVIMExpression.Z=x计算关键路泾航入值IRS.ITestzTMP_2(DOO)=Z.1=X_1CONDITION TMP_2Funclion testme(utnt256,uint256)Expression:xy+10IRS.IVariable|DependenciesTMP_3(uint256)=y_1+10TMP_4(bOOD=X.1STMP_3CONDITIONTMP_4Expressiontrevertoo验证漏洞是否存在TestzIRS符号执行TMP_5(None)=SOUDITY_CALLrevertOO阶段I：搜索关键路径阶段I：验证阶段返回结果图2 PSSE漏洞检测流程Figure 2 PSSE vulnerability detection process2漏洞原理分析2.1Gas耗尽拒绝服务Gas耗尽拒绝服务的主要原因是当某个函数在实现对动态数组的遍历时，每一次循环都包含对全局状态变量更改等高消耗Gas操作，那么就存在攻击者恶意增加动态数组长度的情况，使得该函数所需的Gas超过区块的最大Gas消耗值，导致该函数无法被打包写入区块，出现拒绝服务的现象。在图3 所示的NavieBank合约中，applyInterest(）是一个public类型的函数，主要用来更新用户的利息，会对accounts|数组进行遍历，在遍历中计算用户本息和并更新用户余额。整个函数调用所需Gas的费用是不固定的，随着accountsll数组长度的增大而增加。当攻击者通过恶意攻击制造大量假用户，使得accountsl1数组长度过大，当银行合约在调用1pragmasolidity04.21;2contractNavieBankl3structAccountf4addressaddr:5uintbalance:)6Accountaccounts;7function applylnteresto public return(uint)8for(uinti=j=0.4.0;2contractU_storaget3uintpublicluckNum=52;structGuessf45address player;6uint num;)8Guessll publicguessHistory;9function guess(uint _num)public payablef10Guess newGuess;11newGuess.player=msg.sender;luckNum:52078.7507612newGuess.num=_num;13guessHistory.push(newGuess);14ifLnum=luckNum)(15msg.sender.transfer(msg.value*2);1617图4覆盖sloto位置上的值Figure 4 Override value at slotO position369第2 期王泽旭，关键路径预搜合约漏洞检测看到当玩家调用guess(52）函数参与游戏时，luckNum的值已经被覆盖为5 2 0 7 8.7 5 0 7 6，用户无法正常获得奖金。2.4存储覆盖漏洞检测方法在阶段I，使用静态检测方法进行分析时，主要借助Sliher的中间语言SlithIR进行。通过对智能合约中的Storage类型变量进行判断，确认是否存在Storage的变量在声明时没有被初始化，若存在则将该Storage变量和漏洞所在的函数信息整合为Result_A作为输出。在阶段I，进行符号执行时，将Result_A的信息进行解析为可疑函数的调用序列，借助符号分析引擎实现对漏洞所在路径的探索。因为阶段I已将可疑漏洞的函数名称等信息进行整合，在本阶段只需完成白盒测试工作，若在某个函数调用前后sloto位置上的值产生了改变，则认定漏洞存在并将最终结果输出。3实验与评估3.1实验数据对于Gas耗尽拒绝服务该类漏洞的数据集，主要从开源数据集中获取，共计10 0 0 份智能合约，平均每个函数有3.5 个循环结构，如图5 和6 所示。存储覆盖漏洞的数据集主要由3 万份链上智能合约源码整理而来（使用静态检测工具初步扫描，结合自动化脚本批量获取疑似存储覆盖漏洞合约），在此基础上通过人工标注的方式获取7 9 份存在存储覆盖漏洞的合约。6000康上号40002000060040060合约数量20020400合约中循环数量图5 循环结构、行数及合约数量分布情况Figure 5 Distribution of circulating structure700600500400300200100日：日011工工13579111315 1719212325合约中循环结构数目图6 循环结构分布密度Figure 6 Distribution density of circulation structure第42 卷370应用报学学科3.2实验环境设计实验操作系统版本为Ubuntu18.0464位，使用Smartbugs与其他检测工具进行对比实验，Shell及Python3进行数据集的处理及自动化批处理等工作，Matlab工具进行实验结果可视化，主要使用NodeJs、So l c-s e l e c t、Sl i t h e r 17 和Manticorel18等工具辅助实验，具体实验环境参数如表1所示。表1基本实验环境Table 1 Basic experimental environment名称版本处理器Inter I5-1135G7 2.40 GHz内存DDR4 16G操作系统Ubuntu18.04 64Python3.8Solc0.40.8Manticore0.1.5Slither0.8.7Nodejs12.18.0Docker20.10.7Smartbugs1.0.03.3实验结果与评估3.3.1时间消耗对比3.3.1.1Gas耗尽拒绝服务对于该漏洞的检测，阶段I产生的Result_A信息作为预警信息来处理。使用符号执行检测Gas耗尽导致拒绝服务的漏洞，需要消耗大量的时间来验证拒绝服务的结果。同时，该漏洞的危险等级为轻微，在批量化的实验中阶段I的结果对最终结果影响更重要。通过设置较低的Gas消耗阈值使得容易触发Gas耗尽等实现初步验证，旨在减少动态测试中过度的时间消耗导致的误报等。图7 为PSSE与另外5 种工具的结果对比图，大多数静态检测工具检测速度快，可支持的合约覆盖率高。动态检测工具检测速度慢，对合约的支持能力有限。如mythril19、mPr o 2 0 等这类工具多使用动态的方法进行检测，时间消耗较大，且对智能合约的覆盖度不足；PSSE实现动静态检测技术的结合，对智能合约预搜索（中间语言分析），搜索触发漏洞的关键路径，指导并优化符号执行的检测过程。对智能合约源码进行语义分析、数据流分析等，在此基础上进行信息搜集与遍历，通过符号执行确定：循环结构中是否存在消耗大量Gas的指令，判定是否存在被操纵的Gas漏洞。从时间对比可以看到，PSSE在实现动静态技术相结合的同时，时间消耗适中，可以满足批量自动化检测的需要。3.3.1.2存储覆盖漏洞将PSSE与Slither进行对比实验。从图8 所示的时间对比中可以看到PSSE与Slither在时间消耗上保持统一水平。这表明：结合路径预搜索的策略能够实现对符号执行过程的优371第2 期王泽旭，等：关键路径预搜索的符合约漏洞检测90Q800mPro1000Mythril700Slither960号SmartCheck600Securify500920LPSSE400880300040 80120160200100L10400.51.01.52.02.53.0时间消耗/s图7 时间消耗对比Figure 7 Time consumption comparison600SlitherPSSE500Su/4003002001000510152025303540智能合约序号图8 时间消耗对比Figure 88Time consumption comparison化，提高漏洞检测的效率。对于未初始化存储这类漏洞集的检测速度快，可实现自动化批量处理的漏洞检测。3.3.2检测结果对比分析3.3.2.1Gas耗尽拒绝服务如表2 所示，对比工具支持对大部分合约的检测，PSSE的检测结果真阳性数最高，可达843，而MPRO和MYTHRIL的真阳性数均为0；SLITHER的假阳性数为3，虽然与PSSE相同，但其假阴性的数远超过PSSE。本组实验对10 0 0 个包含被操纵的Gas漏洞智能合约进行检测，图9 中的蓝色条形代表无报错的合约数量，红色条形代表检测认定存在漏洞的合约数量，绿色条形代表假阴性（FN）和报错（ERROR）合约数量之和。从表2 漏洞检测的结果统计可知，实验数据均为包含被操纵的Gas漏洞智能合约源码，TN均为O。m Pr o 和Mythril针对SWC-128（D o SWi t h Blo c k G a s Li m i t）漏洞检测项并不能实现对被操纵的Gas漏洞检测，误报率最高；MadMax、Sl i t h e r 和Securify21虽然对第42 卷372应用报学科学表2 漏洞检测结果统计Table 2 Statistics of vulnerability detection results工具名称无报错合约TPFNFPTNMADMAX921418582790MPRO851010001490MYTHRIL87001.0001300SLITHER98125174930SMART CHECK100078721300SECURIFY5483086924520PSSE98184315730平均值878373627116010000.90.88000.70.6/鲁号6000.5盘0.44000.32000.20.100MadMaxmProMythrilSlither SmartCheck SecurifyOurs检测工具无报错合约数量检测到漏洞合约数量假阴性（FN）和报错（ERROR）成功检测合约占比图9 检测结果分析Figure 9Analysis of detection results智能合约的覆盖度较高，但误报的智能合约数量也比较多，假阳性过高也是静态检测智能合约漏洞的痛点；SmartCheck22工具与PSSE检测结果较接近，但PSSE成功检测合约占比更高。3.3.2.2存储覆盖漏洞该数据集共包括7 9 份智能合约，其中包括5 3 个漏洞合约。由表3 和图10 可知，Slither对其中的8 份合约进行扫描时报出solc版本不匹配错误，对7 1份智能合约进行扫描，正确检表3 与Slither对比检测结果比较Table 3 Comparison of detection results with Slither工具名称无报错合约TPFNFPTNSLITHER714324102PSSE795311015373第2 期王泽旭，等：关键路径预搜索的符合约漏洞检测测占比为5 5.7%；PSSE实现了对数据集的全部扫描和全覆盖，正确检测占比为8 6.1%。从图11ROC曲线可以看出本文的PSSE方法Auc值更高，检测效果更准确。140F1.0F1201000.8F800.660400.4200.2-Slither,auc=0.43SlitherOurs-Ours,auc=0.78检测工具无报错合约数量报错合约数量00.20.40.60.81.0口真阳性（TP）和真阴性（TN)假阳性比例图10 与Slither结果对比图11ROC对比Figure 10 Comparison with slither resultsFigure 11ROC Comparison3.4总结本文提出的PSSE方法，在与其他相关工具进行存储覆盖漏洞、Gas耗尽拒绝服务漏洞检测时，通过实验评估表现出理想的检测效果。利用静态预检测的方法生成符号执行的关键路径信息，指导符号执行完成漏洞检测的工作，理论上时间复杂度由传统的O(n）变为O(1)。结合静态检测，大大降低了符号执行中不必要的路径资源消耗，也避免了符号执行由于路径爆炸等问题带来的覆盖度不足等问题。通过效率与有效性两个维度的实验对比验证了PSSE方法的有效性与可靠性。4结语本文在传统符号执行工作的基础上，提出了利用静态检测指导符号执行关键路径的搜索方法，并结合Gas耗尽拒绝服务、覆盖存储两种漏洞原理分析及智能合约语言特点完成了实验评估与设计，实验结果证明了该方法的可行性与高效性。未来工作需要改进的方向：1）利用静态检测的生成信息指导符号执行测试时输入参数随机生成，会影响检测的速度与效率，可尝试结合启发式算法等实现输入参数生成的高效性；2）实现多漏洞的检测，对工具进行模块化的设计与函数的封装，实现对多种漏洞的覆盖；3）在进行智能合约漏洞检测时结合智能合约的区块链属性等特性细粒度建模，并设计精确的搜索策略保证结果的高效与可靠。参考文献：1 ZHENG Z B,XIE S A,DAI H N,et al.An overview of blockchain technology:architecture,consensus,and future trends Cl/2017 IEEE International Congress on Big Data(BigDataCongress).IEEE,2017:557-564.2 KusHWAHA S S,JosHI S,SINGH D,et al.Ethereum smart contract analysis tools:a systematicreview J.IEEE Access,2022,10:57037-57062.3 WAN Z Y,XIA X,Lo D,et al.Smart contract security:a practitioners perspective C/2021IEEE/ACM 43rd International Conference on Software Engineering(ICSE).IEEE,2021:1410-1422.4 MARIANO B,CHEN Y J,FENG Y,et al.Demystifying loops in smart contracts Cl/202035th IEEE/ACM International Conference on Automated Software Engineering.IEEE,2020:262-274.雪(编辑：王第42 卷374应用报学科学5 BALDONI R,CoPPA E,DELIA D C,et al.A survey of symbolic execution techniques J.ACMComputing Surveys,51(3):1-39.6魏昂，黄忠义，周鸣爱.智能合约安全与实施规范研究 .网络空间安全，2 0 2 0,11(3)：44-49.WEI A,HuANG Z Y,ZHoU M A.Research on the security and implementation of smartcontract J.Information Security and Technology,2020,11(3):44-49.(in Chinese)7倪远东，张超，殷婷婷.智能合约安全漏洞研究综述 .信息安全学报，2 0 2 0,5(3)：7 8-9 9.NI Y D,ZHANG C,YIN T T.A survey of smart contract vulnerability research J.Journal ofCyber Security,2020,5(3):78-99.(in Chinese)8 Luu L,CHU D H,OLICKEL H,et al.Making smart contracts smarter C/2016 ACM SIGSACconference on Computer and Communications Security,2016:254-269.9 CHEN T,FENG YZ,LIZ H,et al.GasChecker:scalable analysis for discovering gas-inefficientsmart contracts JJ.IEEE Transactions on Emerging Topics in Computing,2021,9(3):1433-1448.10陈霄汉，赵相福，张登记，等SlightDetection：一种以太坊智能合约安全漏洞的静态分析工具 J.应用科学学报，2 0 2 2，40(4)：6 9 5-7 12.CHEN X H,ZHAo X F,ZHANG D J,et al.SlightDetection:a static analysis tool for smartcontracts security vulnerabilities on ethereum J.Journal of Applied Sciences,2022,40(4):695-712.(in Chinese)11引张登记，赵相福，陈中育，等。基于Ethereum智能合约的安全策略分析 J应用科学学报，2 0 2 1,39(1):151-163.ZHANG D J,ZHAo X F,CHEN Z Y,et al.Analysis of security strategies for smart contractsbased on ethereum J.Journal of Applied Sciences,2021,39(1):151-163.(in Chinese)12林林锦滨，张晓菲，刘晖.符号执行技术研究 C/全国计算机安全学术交流会，2 0 0 9：412-416.13】付梦琳，吴礼发，洪征，等。智能合约安全漏洞挖掘技术研究 J。计算机应用，2 0 19，3 9(7)：19 5 9-1966.Fu M L,Wu L F,HonG Z,et al.Research on vulnerability mining technique for smartcontracts J.Journal of Computer Applications,2019,39(7):1959-1966.(in Chinese)14】袁勇，王飞跃.区块链技术发展现状与展望 J自动化学报，2 0 16，42(4)：48 1-49 4.YuAN Y,WANG F Y.Blockchain:the state of the art and future trends J.Acta AutomaticaSinica,2016,42(4):481-494.(in Chinese)15 LIu Y,ZHou X,GoNG W W.A survey of search strategies in the dynamic symbolic executionJ.ITM Web of Conferences,2017,12:03025.16 NAssIRZADEH B,SuN H,BANEscu S,et al.Gas gauge:a security analysis tool for smart con-tract out-of-gas vulnerabilities DB/OL.2021 2022-08-14.http:/arxiv.org/abs/2112.14771.17 FEIST J,GRIEco G,GRocE A.Slither:a static analysis framework for smart contractsCl/2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineeringfor Blockchain(WETSEB).IEEE,2019:8-15.18 MosSBERG M,MANZANo F,HENNENFENT E,et al.Manticore:a user-friendly symbolic ex-ecution framework for binaries and smart contracts Cl/2019 34th IEEE/ACM InternationalConference on Automated Software Engineering(ASE)IEEE,2019:1186-1189.19 ZHANG W,BANEsCU S,PAsos L,et al.Mpro:combining static and symbolic analysis forscalable testing of smart contract C/2019 IEEE 30th International Symposium on SoftwareReliability Engineering(ISSRE).IEEE,2019:456-462.20 ZHANG W,BANESCU S,PASos L,et al.MPro:combining static and symbolic analysis forscalable testing of smart contract C/2019 IEEE 30th International Symposium on SoftwareReliability Engineering(ISSRE).IEEE,2019:456-462.21 TsANKOv P,DAN A,DRACHSLER-CoHEN D,et al.Securify:practical security analysis ofsmart contracts C/Proceedings of the 2018 ACM SIGSAC Conference on Computer andCommunications Security,2018:67-82.22 TIKHOMIROv S,VoSKRESENSKAYA E,IVANITSKIY I,et al.SmartCheck:static analysis ofethereum smart contracts Cl/2018 IEEE/ACM 1st International Workshop on EmergingTrends in Software Engineering for Blockchain(WETSEB).IEEE,2018:9-16.