论文研究 基于动态符号执行技术的协议逆向分析方法 .pdf

基于动态符号执行技术的协议逆向分析方法，杨昌鑫，武斌，未知协议的协议逆向分析对其安全性研究具有十分重要的意义。目前基于网络轨迹和基于指令执行的两种主要分析方法在协议信息分析和山国利技论文在线http://www.paper.edu.cn基于指令执行的协议逆向技术基」指令执行的协议逆向技术其分析对象为产生或接收并分析协议数据的通信实体,通常为软件程序。其通过跟踪分析通信实体对协议报文数据的处理过程,米提取目标协议的相75关信息Caballero等人提出的基于动态污点分析技术的 Polyglot采用离线分析的方式对报文格式中的关键字进行识别。其通过判断解析指令中的参数类型来确定定长域和变长域,并通过跟踪污点数据与非污点的常量字符串之间发生的比较操作来识别协议关键字i基于污点数据分析提出了域结构识别方案 auto Format,其通过记录操作指令和函数调用栈来判断域之间的序列关系。该方案弥补」 Polyglot只能将报文格式识别为域的线性序列的缺点,但无法处理复杂结构和未知语义。Comparetti等人提出的 Prospex方案在 AutoFormat的基础上采用聚类的方式对相同状态的报文进行处理并通过报文序列的状态标注实现了协议状态机的分析。该方案可以根据逆向分析的结果,自动化生成模糊测试工只 Peach所需的测试脚本。但其并没有考虑域的语义85和取值约束,因此无法保证生成的模糊测试用例数据的有效性综合分析上述国内外相关硏究情况,目前相关的研究方法在针对协议的报文格式、域语义、域取值约束以及状态机等信息的分析和提取中,均存在不同程度的缺陷。基于网络轨迹的协议逆向技术其分析结果极大程度上依赖于协议数据样木集的完备性,虽然其操作简使易行,但该类方法在协议的珸义信息及协议状态机信息的提取上局限性较大;基于指令执行的协议逆向技术则充分利用了协议通信实体中包含的协议格式、语义及状态转换等信息。但目前基于动态污点分析的指令轨迹分析方法,受限于通信实体所接收的协议输入数据流,在协议格式和状态路径挖掘的充分性上存在局限,难以覆盖协议通信实体中关于协议数据处理的全部路径分支,且对于协议域的取值约束分析亦存在缺陷基于此,本文在指令执行分析思想的基础上,提出采用符号执行技术对目标协议的通信实体进行分析,挖掘通信实体的完备路径分支及各分支路径条件下的取值约束关系以解决协议语法、语义及取值约束等信恳的解析,通过构建通信实体的嵱径执行树解决协议状态机信息的提取,对现有方法在以上内容解析过程中存在的缺陷和不足进行改进。方法与关键技术分析动态符号执行100动态符号执行的本质是将实际执行的路径信息与符号执行技术相结合,用具体的输入数据执行程序,并在程序运行的过程中,通过程序插桩的手段收集路径分支处的约束条件,然后对收集到的约束条件集合中的某一个进行取反操作,再调用约束求解器对取反后的新约束条件集合进行求解,从而生成另一条执行路径下的测试用例并重复上述过程直至遍历测试对象的全部执行路径105在动态符号执行的过程中,符号执行会生成执行路径中条件语句对于输入的符号化约束国科技论文在线http://www.paper.edu.cn关系,而后由约束求解器对约束关系进行求解从而获得该路径对应的取值约束。约束求解是符号执行的基础,其主要依赖于可满足性模理论SMT。SMT是判定一阶逻辑公式在组合背景下珥论下的可满足性问题,其具体实现被称为SMT求解器。经过发展,目前活跃并成熟的SMT求解器包括CVC4、STP、Z3、 Yices等,这些约束求解器被程序分析工只广泛使用。基于动态符号执行技术的协议逆向分析方法结合动态符号执行的特征,我们可以利用其对办议通信实体进行分析。通信实体的每条执行路径即对应」协议的一种输入报文格式,分支路径卜的取值约束关系,即是该报文格式的取值约東。对于整个协议通信实体所构建的路径执行树,我们也可以将每个报文格式对应115的执行路径抽象成一个状态节点,从而根据路径执行树分析出协议的状态机信息。由于符号执行对于路径遍历及路径约束求解的特性,我们可以有效解决目前协议逆向分析中存在的语法、语义信息不完整,状态机信息缺乏等问题基于符号约東关系的输入报文格式解析对于未知协议的输入报文格式集合Σ,我们可以将其定义为Σ={σ0O1…,O},其中120σ表示该协议的输入报文格式。根据协议报文特征,输入报文σ由右干协议域组成,因此可将输入报文σ定义为σ={a0,1…,},其中a表示报文的一个组成域。在符号执行的过程中,动态符号执行引礤会在全局维扩一个状态信息,可表示为z,6),其中表小程序计数器,指向下一条要执行的指令:π表小路径条件的符号化约束关系,初始定义为兀:δ表示当前路径下各符号变量的符号状态。125假设为协议通信实体某输入报文σ的实际数据内容,采用动态符号执行分析协议通信实体对报文的处理,则引擎的初始状态可表示为:其中为输入的初始符号变量。协议通信实体在解析报文的过稈中,会从报文数据中通过逻辑或算数运算提取报文各组成域,即报文组成域α可表示为报文数据的函数映130射。符号执行引擎在分析过程中,会对新产生的变量进行符号化处理,并在约束集加入该变量的维护。因此,经协议通信实体对报文数据的运算处理后,引擎维护的路径分支的状态信息和符号化约束条件可表示为:6:{→,a→9(),a→90()…,a→9(兀:{%()∈o∩q()∈n…g()∈}4国科技论文在线http://www.paper.edu.cn其中()表示报文组成域a关于报文数据的符号约束关系,()∈表示程序执行当前路径的必要条件是()满足约束条件,程序执行当前路径的充分条件则为所有()均满足对应约束条件。通过求解π中维护的符号约束关系即可获得当前路径下的输入报文格式,通过报文组成域α与报文数据的约束关系φ即可求得该报文的各组成域的信息。对π中维护的符号约束关系中的某个条件进行取反操作,求解后即可得到另·条分支路径的输入报文数据,依140次遍历协议通信实体的协议报文处理相关的全部路径分支即可获得完备的协议输入报文格式集合∑及报文σ的语法、语义及取值约束等信息基于路径执行树的协议状态机分析协议的状态代表协议实体在当前会话时刻的上下文关系,其定义了协议实体间通信报文的序列及交互行为。协议实体的状态通常是有限的,其有限的全部状态构成协议的有限145状态集合Q={,,…,}。协议实体间的会话过程即是各协议有限状态集合中各状态之间的迁移过程,该过程可表示为6×a→b其中O定义为状态迁移函数,其表示协议实体间的会话从状态θ迁移到状态所需经历的过程。实质上,从θ到θ的迁移是多个中间状态的转换过程,相关中间状态的序列关150系即形成∫协议的状态迁移函数ω。协议通信实体在处理会话报文时,会根据当前时刻会话所处的状态对输入的报文数据进行处理,而当前吋刻的状态则依赖于前时刻所接收的会话数据。因此,在一次会话过程中,协议通信实体对输入报文的解析顺序和指令执行路径的跳转条件对应于协议状态机的一条子路径,通过分析一次公话中多个输入报文之间的排列顺序和关联关系即可推断出协议的状态转移信息。155协议实体在不同会话状态下可接收的输入报文格式是有限且固定的,若输入报文不符合当前会话状态则协议通信实体程序会进入会话异常处理分支,可导致报文被丢弃、目的端无响应、会话结束、断开连接等;若输入符合当前会话状态,则程序执行流程进入响应分支且卜一次接收的会话报文应符合更新后会话状态,会话报文的不同处理流程的木质即是协议通信实体中的不同的逻辑分支。160在会话状态θ下,通过动态符号执行分析获取各分支路径的符号约束关系集合,通过监测接收报文后协义实体的会话状态,剔除约束关系集合中无效的路径约束条件后得到日状态下会话有效的分支路径的符号约束关系集合:山国利技论文在线http://www.paper.edu.cn={(0,70,0),(1,x1,1)…,(,x,O)}其中(;,,δ)表示当前会话状态下协议通信实体中的一条执行路径的符号约束条165件,对约束进行求解即可获得协议实体在状态θ下可接收的输入报文格式集合。假设协议实体在执行符号约束集合中的某条路径后,会话状态从O迁移到θ,则同埋可求得θ状态下可接收的输入报文格式集合。根据以上分析,如图1所示,协议状态机集合△可衣示为个树结构。树结构的节点衣示当前会话状态;树结构中父子节点的顺序关系则对应于协议状态机中的一种状态转换路径;同一父节点的各个子节点的并列关系则表示父节点对应状态下的多种不同的协议状态转换路径。树结构中的一条状态路径如}0→2→)→>}(则表示该协议在会话中的一种状态迁移方式。0dd2d3图状态机树结构175Tree structure representation of state machine系统实现与实验评估系统设计与实现本文采用开源框架Angr2作为动态符号执行的基础平台。Angr是个基于 python实现的高度模块化的进分析平台,由加州大学圣芭芭拉分校计算机安全实验室的 Shellphish180闭队研发。框架功能包括:符号执行、中间语言表示、反汇编、稈序监控、控制流分析、数据依赖性分析、值焦分析等。系统功能主要分为协议输入报文格式集合的解析和协议状态机的构建,系统总体框架流程如图2所山国利技论文在线http://www.paper.edu.cn建立会话初始化发送报文符号执行分析符号执行分析报文无效约束关系求解路径约束求解输入报文格式集合路径执行树<会话状态>协议状态集合185图系统流程图System flow chart协议输入报文柊式集合解析部分实现输入报文格式的解析,包括报文的组成域、域结构、偏移、类型、取值约束等內容。初始化模坎载入协议的二进制实体程序后,通过污点追踪定位到程序对协议数据处理的函数入凵地址,并从该入口地址开始对程序进行符号执行分析,190之前的部分采用实际执行。符号执行分析各路径的约束条件后由约束求解器进行求解并生成新的测试输入数据,不断循环此过程从而得到协议的输入报文柊式结合协议状态机分析部分实现协议状态机信息的构建,其输入依赖于输入报文格式集合。该部分通过与协议通信实体之间建立会话,发送会话报文并通过分析程序对会话报文的解析过程,收集解析路径的符号化约束条件,求解当前会话状态下可接收的输入报文格式并更新协195议状态集合。通过判断会话状态是否维持,来确定输入的会话报文是否有效,若有效则继续从输入报文格式中选取新的会话报文作为会话输入;若会话结束,则标志该报文不符合当前会话状态,则引擎重新与协议通信实体建立会话,并根据协议状态集合中维护的状态树继续上一步的测试。实验评估与结果分析200本文提出的基于动态符号执行技术的协议逆向分析方法,主要应用于未知协议的语法、语义及状态机信息的提取。为验证其有效性,本文选取FTP协议作为测试对象。FTP(FilcTransfer protocol,FTP)即文本传输协议,是用于在网终上进行文件传输的一套标准协议。实验在假设无任何先验协议信息的情況下,用木文的方法分析FTP协议的相关信息,实验选取 Vsftpd作为FTP协议的通信实体。Ⅴsfpd是一个UNIx类操作系统上运行的开源FIP205服务器软件实验首先验证系统对协议输入报文格式解析的有效性。表1所小为系统解析岀的FTP协议输入报文格式支持的命令字与实验测试程序Vspd支持的FTP命令类型的对比,系统7国科技论文在线http://www.paper.edu.cn共分析出3个FTP协议标准命令,全部命中测试程序Ⅴsfφpd中支持的命令类型。表实验结果FTP命令类型210Experimental result- FTP command type基于动态符号执行VsftpdABORACCTAPPE. BYE. CDUP CWD DELE. ABORACCTAPPE. BYE. CDUP, CWD, DELEIIELP, LIST. MKD, MODE, NIST NOOP, PASS, TIELP, LIST. MKD MODE. NLST, NOOP, PASFTP命令字集合 PASV PORTPWD,QUIT, REINRESTRETR,,PASV,PORT, PWD.QUIT, REINREST,RETR,RMD,RNFRRNTO SITE SIZE SMNT STAT. RMDRNFR, RNTOSITE SIZESMNTSTATSTOR STRUSYSTTYPEUSERSTORSTRUSYSTTYPE USER总数33实验分别采用了典型协议逆向分析方法如人工逆向分析、PI、 Autoformat等对FTP协议报文进行逆向分析,并与本文提出的方法进行了比较。表2所示,本文提出的基于动态符号执行技术的协议逆向分析方法相较于其他典型算法虽然运行耗时相对较长,但在协议格式分析的完备性上有明显提高215表实验结果比对算法性能Experimental result comparison -FTP command types基于动态符号执行人工分析Autoformat技术FTP命令类型3328运行耗时3天6小时2小时11分5小时21分7小时33分覆盖率100%42.4848100%实验验证了系统对协议状态机信息的解析的有效性,系统对协议状态机的分析结果以树结构的形式输出。图3反映了系统推断的FIP协议的状态机部分模型。图中路径{0→1→2→3→4}表小了协以从登陆到行为交互到退出登陆的过程;图中父节点与子220节点取值重复的路径代衣状态保持,如路径{→衣示输入报文不符合PASS协议格式或PASS参数错误时,会话状态保持在当前状态;图中烙径参数P;表示当前状态转换路径支持的命令集。经过验证系统推断的协议状态机符合上P协议状态机规范。0USER0PAss2QUIT43图状态机分析结果225State machine analysis result国科技论文在线http://www.paper.edu.cn结论本文对目前协议逆向分析中国内外主要的研究方法进行了分析,提出了基于动态符号执行技术的协议逆冋分析方法,方法主要应用于未知协议的语法、语义、状态机信息的解析和提取。经过实验测试,测试结果衣明方法有效地改进了目前协议逆向分析技术中存在的协议230语法、语义、状态机信息不亢整,取值约東关系缺乏等问题,为协议逆向分析结果在协议安全性研究中的应用提供了帮助。参考文献[1]滔璠,吴礼发,杜有翔等.协议逆向工程矶究进展[.计算机应用矿究,2011,28(8):2801-2806.[2]BeddOeM.Protocolinformationprojectol].[2004-10-05].http://www.4tphi.net/awalters/pi/pi.html5k235储焰南.基于Ueos2的嵌入式GUI研究与应用「OL.「2008-7-31http:/www.kuryibu.com/tech/112361[3]LEITA C, MERMOUD K, DACIER M. Script Gen: an automated script generation tool for honeyd[c]/proc ofthe 21st Annual Computer Security Applications Conference. 2005: 203-214[4]李伟明’张爱芳,刘建财等.网络协议的自动化模糊测试漏洞挖掘方法门]计算机学报,2011,34(2):240242-255[5] CUI Wei-dong, KANNAN J, WANG H J Discoverer: automatic protocol reverse engineering from networktraces[C)/Proc of the 1 6th USENIX Security Symposium 2007: 199-212[6JCABALLERO, YIN Heng, LIANG Zhen-kai, et al. Polyglot: automatic extraction of protocol format usingdynamic binary analysis[C]/Proc of the 14th ACM Conference on Computer and Communications Security. 2007245317-329.[7LI Zhi-qiang, JIANG Xu-xing, XU Dong-yan, et al. Autonatic protocol format reverse engineering throughcontcxt-awarc monitored exccution[C]/Proc of thc 1Sth Symposium on Nctwork and Distributcd Systcm Sccurity2008.8 COMPARETTI P M, WONDRACEK G, KRUEGEL C, et al. Prospex: protocol specification250extraction[C]/Proc of the 3 0th IEEE Symposium on Security and Privacy. 2009: 110-125[9] GOLDFROID P, KLARUND N, SEN K. DART: directedautomated random testing[C]//Proc of PrograrmningLanguage Dcsign and Implementation. Ncw York: ACM Press, 2005: 213-223[10]王翀,吕荫润,陈力,王秀利,王水吉.SMT求解抆术的发展及最新应用研宄综述.计算机研究与发展,2017,54(7):1405-1425.255[1]吴礼发,王辰,法征,庄洪林等.协议状态机推断技术硏宄进展[J.计算机应用研宄,2015,32(71931-1936[12]Yan S, Wang R, Salls C, et al. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis[Ch/Security and Privacy. IEEE, 2016: 138-157.