CN115408689B 一种重入漏洞的检测与修复方法、系统 （北京大学）

本发明公开了一种重入漏洞的检测与修复能合约源代码进行编译并生成以太坊虚拟机字过程中根据重入模式映射表识别路径的重入模本发明能够在保证合约语义不变的前提下进行2代码的执行路径并生成控制流图，遍历过程中根据重入模式映射表识别路径的重入模式，2)检测修复系统对待检测的智能合约源代码3)根据检测结果，如果该智能合约源代码4)检测修复系统利用语义等价测试用例、重入漏4.如权利要求3所述的方法，其特征在于，检测修复系统对该智能合约源代码进行修3单路径重入模式检测模块，用于对待处理的智能合约源代码进组合重入路径检测模块，用于对主重入路径模式中具有相同路径条件的路径进行去测试用例代码生成模块，用于对包含状态修改节点的路径生成一个语义等价测试用重入漏洞修复模块，用于对包含重入漏洞的智能合约源代码修复结果验证模块，用于利用语义等价测试用例、重入漏4的指令编号和源码映射找到对应语句的源码范围，再结合抽象语法树AST找到对应语句的9.如权利要求7或8所述的系统，其特征在于，所述522日，总市值为2010亿美元(参考R.Bagshaw.Top10cryptocurrenciesbymarket分析的方法(参考L.Luu,D._H.Chu,H.Olickeletal.“Makingsmartcontractssmarter”.In:Proceedingsofthe2016ACMSIGSACconferenceoncomputerandAnalyzingSafetyofSmartContracts.”In:NDSS,2018；P.Tsankov,A.Dan,D.Drachsler_Cohenetal.“Securify:Practicalsecurityanalysisofsmartcontracts”.In:Proceedingsofthe2018ACMSIGSACConferenceonComputerandSystemSecuritySymposium,NDSS2019,SanDiego,California,USA,February24_27,“生成与验证”框架实现了SCRepair系统来自动化修复重入漏洞(参考X.L.Yu,O.Al_Bataineh,D.Loetal.“Smartcontractrepair”.ACMTransactionsonSoftwareEngineeringandMethodology(TOSEM),2020,29(4):1–32)。但目前系统只能检测修复链交易，难以检测修复未上链产生交易的漏洞合约。并且系统中使用相对随机的方法生成补漏洞的修复与语义等价的形式化验证。6VirtualMachine)字节码、ABI(应用二进制接口，ApplicationBinaryInterface)、[0013](/Z3Prover/z3)约束求解器对EVM字节码进行遍历，得到合约的执行路径并生成控制流图，遍历过程中根据路径上的关键指令识别单路径的重入模式，重入模式定义与关键指令见重入模式映射表，并以路径为单位记录主重入路径模式求解器和污渍跟踪技术判断组合后路径连通性与重入函数>以及主重入路径的ID与重入漏洞有关的指令编号等信息(比如外部调用指令[0016]31)语义等价测试用例：接收单重入路径检测时产生的语义等价测试用例计算请7测试用例模板生成可以在Truffle中运行的测试用例Solidity代码。模板中针对每一个测要。修改前和修改后的合约均需微调内容包括：对于缺少fallback函数的合约添加[0020]4)检测修复系统对包含重入漏洞的源代码进行修复[0021]41)基于锁的修复模板：依据22)中生成的重入函数对，对重入函数对<主重入函用(CALL指令)对应语句的AST节点c与RCW模式中写操作(SSTORE指令)对应语句的AST节点8本文提出的重入漏洞检测与修复工具进行测试。结果显示，系统对重入漏洞的检测率为100其中4个真实合约文件中均包含RRW指令SSTORE、外部调用指令(CALL,DELEGATECALL,STATICCALL),日志记录指令(LOG0~令形成RC、RW、RL和RJ集合，判断这些指令是否构成主重入路径RCR模式的一部分。针对9[0041]组合重入路径检测流程如图2所示。这一步本文将主重入路径中的重入模式与被解器进行求解，为了提高求解成功率，本文使用自定义配置策略求解，包括simplify，solve_eqs,bit_blast,aig,s[0043]基于锁策略的重入漏洞修复流程如图3所示。添加锁不会影响函数内已有数据值[0045]基于重排序策略的重入漏洞修复流程图如图4所示。分为RCW修复信息生成和RCR入漏洞的SSTORE指令和外部调用指令编号，通过sourcemapping中指令与源码的映射关[0046]语句移动时的语义等价检测需要检查移动后合约CFG中受影响子图中是否包含读这些读节点对应的storage变量替换为局部变量，局部变量的初始化添加在紧邻移动后的初始化AST添加至函数AST中。在全部函数AST修改添加完成后，利用prettier_plugin_[0050]测试用例代码生成流程如图5所示。模块首先接收检测过程中的测试用例生成请求，并利用Z3约束求解器计算出测试用例参数，形成JSON格式文件。然后读取测试用例[0052]修复结果验证流程如图6所示。本文使用Truffle框架和Ganache测试网络完成测[0058]1)在RCW重入模式中：主重入模式为RCW，被重入模式为RC/RW/RL/RJ中的任意一种，主重入模式中的读操作R和写操作W与被重入模式中的读操作R对应相同的storage变[0059]2)在RCR重入模式中：主重入模式为RCR，被重入模式为RC/RW/RL/RJ中的任意一意一子问题无解则返回空集。首先对所有写操作根据storage变量名进行划分，每一个storage变量下可能包含1个或多个写操作。然后根据每一个storage变量依次对条件约束赖于两个写操作。首先根据变量a将条件约束划分为依赖a的条件约束和不依赖a的条件约