x86可执行程序时序安全漏洞检验方法

《x86可执行程序时序安全漏洞检验方法》由会员分享，可在线阅读，更多相关《x86可执行程序时序安全漏洞检验方法（5页珍藏版）》请在装配图网上搜索。

1、第11A期李佳静等：x86可执行程序时序安全漏洞检验方法101x86可执行程序时序安全漏洞检验方法李佳静, 韦韬, 毛剑(北京大学 计算机科学技术研究所，北京 100871)摘 要：给出了对静态检查可执行程序时序安全漏洞中的2个主要问题的研究结果：1) 2种新的时序安全漏洞模型；2) 建立二进制程序的下推自动机方法。实验证明该方法可以有效地辅助在可执行程序中验证和发现时序安全漏洞。关键词：信息安全；安全漏洞分析；模型检验；时序属性中图分类号：TP314 文献标识码：A 文章编号：1000-436X(2007)11A-0098-05Method of model checking x86 exe

2、cutables for temporal security vulnerabilitiesLI Jia-jing, WEI Tao, MAO Jian(Institute of Computer Science & Technology of Peking University, Beijing 100871, China)Abstract: Two research results of temporal vulnerabilities in x86 executables were giveded. First two new models of temporal vulnerabili

3、ties were presented; secondly a method of building pushdown automata for executables was given. Experiments showed the method was effective to verify and find temporal vulnerabilities in x86 executables.Key words: information security; vulnerability analysis; model checking; temporal properties1 引言软

4、件中存在安全漏洞是引起计算机系统中安全事件的重要因素，保证软件的安全已经成为巨大的挑战。目前很多减少软件中存在的安全漏洞的方法被提出来，例如通过使用安全的语言来避免缓冲区溢出漏洞。然而，安全的程序语言不能防止所有的安全漏洞，例如在软件中广泛存在的时序安全漏洞。这些漏洞通常是路径相关的，很难通过测试或者人工审计发现，因此需要能够自动检查这种安全漏洞的工具进行辅助分析。收稿日期：2007-09-21基金项目：国家高技术研究发展计划（“863”计划）基金资助项目（2006AA01Z402）Foundation Item: The National High Technology Research a

5、nd Development Program of China(863 Program) (2006AA01Z402)现有的时序安全分析方法主要分为动态分析方法和静态分析方法。静态分析方法主要针对源代码1,2。但是多数应用程序难以获取其源码；且即使源码可得，也不能完备表现程序行为。因此，针对可执行代码的安全漏洞分析会更为有效与完备。同时目前逆向工程工具在提取程序的高级语义方面存在不足，难以对安全漏洞进行自动化辅助分析。动态分析方法集中于对文件竞争条件的检查3,4，这些方法通常有大量漏报。本文提出了一种针对x86可执行程序的静态时序安全漏洞分析方法。该方法可以自动建立可执行程序的抽象表示和进行漏

6、洞检验，有效减少人工分析的工作量。本文的工作主要包括：1)根据公共漏洞库（CVE, common vulnerabilities and exposures）和安全编程规范提出了两种时序漏洞模型；2)提出了一种建立可执行程序的下推自动机的方法；3)基于改进的控制流分析和数据流分析，使得模型检验的结果更有效。以上方法已在自研制的时序安全漏洞分析系统BinMc中使用，对多个应用程序的可执行代码进行了校验检测。实验表明该方法可有效实现针对可执行程序的时序漏洞辅助分析。2 相关研究工作目前程序时序安全漏洞分析方法可以分为静态分析方法和动态分析方法。Bishop使用词法分析检查程序中的文件访问文件竞争条

7、件漏洞，没有考虑程序的控制流和信息流信息，因此产生大量误报。MOPS使用模型检验检查程序中的时序安全漏洞2。SLAM使用迭代过程验证驱动程序1。阳小奇等人通过为变量和函数附加契约及其他资源泄漏等安全漏洞5。这些方法目前只应用于源代码。Ganapathy等使用模型检测分析API层次的脆弱性6。这些方法需要手工建立对被分析系统的简化模型。图1 可执行程序时序安全漏洞检验方法模型动态分析集中于对文件竞争条件漏洞的利用和防护。Borisov指出方法无法消除文件竞争条件漏洞3；Wei等人使用动态方法检查程序中可能引起文件竞争条件的函数调用4。动态分析一般不能遍历程序的所有控制流路径，从而产生漏报。3 时

8、序漏洞分析方法基于Chen等人的时序安全漏洞的抽象分析模型2，本文提出了一种检查可执行程序的时序安全漏洞方法。如图1所示，该方法分为以下3个环节：1)描述时序安全漏洞。对程序中时序安全漏洞关键行为进行分析，并使用自动机描述；2)产生可执行程序的面向安全检查的抽象表示。首先将可执行程序反汇编和反编译得到程序的控制流和数据流语义，再建立程序的抽象语法树和语法树的流图；3)检验时序安全漏洞。使用模型检验检查程序中的时序安全漏洞，如果程序中存在安全漏洞则输出疑似路径。在本节中首先介绍时序漏洞分析抽象模型，然后就本文方法的3个环节进行详细说明。3.1 时序漏洞分析抽象模型Chen等人给出的时序安全漏洞的

9、抽象分析模型。该模型使用有穷状态机（FSA, finite states automata）描述时序安全漏洞，下推自动机（PDA, pushdown automata）描述程序行为，使用模型检验方法检查程序中是否存在时序安全漏洞。令表示程序中安全相关的操作集合，表示违反安全属性的安全操作序列集合，表示程序的执行路径集合。程序是否满足安全属性等价于是否为空。实验表明大多数时序相关的安全属性可以使用正则语言表示，假设是一个正则语言，则存在一个有穷自动机接受B，即。为了表示包含函数调用的执行路径，需要一个栈来记录函数调用的返回地址，由栈产生的语言是上下文无关语言，则存在一个下推自动机P接受。即。初始

10、问题转化为是否为空。使用标准的方法求M和P的交集。产生一个新的PDA，称作复合PDA ，它接受。使用Esparza的算法可以计算在中状态是否可达，如果可达则输出执行路径。3.2 时序安全漏洞模型根据对CVE和Linux安全编程规范的分析，提出了两种时序漏洞模型。3.2.1 错误放弃权限漏洞程序如何放弃特权已经有了深入的研究2，但在实现中setuid()/setguid()是可能失败的，如果没有检查它们的返回状态，程序可能没有放弃特权就调用危险系统函数。本节提出一个程序错误放弃特权时序漏洞模型。如图2所示，该模型使用2个自动机表示。图2(a)描述对setuid()/setguid()的返回结果的

11、检查：程序的初始状态为，经过x=setuid(*)或x=setguid(*)程序从状态到达（其中x=setuid(*)表示setuid()的参数可以为任意值，x为setuid(*)的返回值），经过判断if(x=0)或者if(x!=0)程序从状态到达（x为上步中setuid()/setguid()返回值）；图2(b)描述不安全系统调用引起的系统状态变化：程序的初始状态为，当调用access()或exec()等函数时程序状态从变为。若程序使得1(a)的状态机处于状态或者，1(b)的状态机处于状态时，则程序中存在错误放弃特权漏洞。图2 错误放弃特权漏洞FSA3.2.2 文件竞争条件漏洞Schwarz

12、等人将文件相关的函数调用分为两类，一类是对文件的检查；另一类是对文件的操作2。但是该模型不能描述（open(f)chmod(f)）函数对引起的竞争条件漏洞。对文件的chmod()操作依赖于对open()的结果的假设，因此open()函数可以看作是一种隐式的检查。根据Wei等将产生文件竞争条件的函数进行分组的方法4，本文对每组可能产生条件竞争的函数对建立一个状态机。例如图3所示。程序的初始状态为，经过open(f)或create(f)程序从状态到达，经过chmod(f)或chown(f)程序从状态到达结束状态（其中f为第一步中使用的f）。若程序使得状态机到达结束状态，则程序中存在文件竞争条件漏洞

13、。图3 文件竞争条件漏洞的FSA3.3 面向安全分析的抽象表示面向安全分析的抽象表示主要分为2个环节：反汇编和反编译；抽象语法树解析。3.3.1 反汇编和反编译由于反汇编技术已经非常成熟，实现中使用IDA pro 4.9完成反汇编工作。反编译的工作主要包括控制流分析和数据流分析。本文在实验环节采用的控制流分析方法对复合条件分支识别、嵌套循环识别和多路分支识别算法做出了改进7,8。数据流分析使用静态单赋值（Static Single Assignment, SSA）分析和符号执行取代传统的定义-使用链（def-use chain）分析。3.3.2 抽象语法树解析先将经过反编译的程序生成为语义等价

14、的C语言。然后在抽象语法树层次对程序进行转换，产生适合静态分析工具的形式。代码生成算法与Cifuentes的算法相似9。深度优先遍历控制流图中的每个节点，对于节点中每个控制流无关语句，生成它们对应的算术表达式；对于控制流相关的语句根据以该节点为根节点组成的子树的结构，逐层生成目标代码。将每个C语言函数转换为抽象语法树。以抽象语法元素为节点，语法元素之间的可达关系为边，使用类似建立控制流图的算法，建立抽象语法树的流图。3.4 模型检验使用3.3节生成的程序抽象表示可以使用现有的算法建立可执行程序的PDA2。在模型检验环节，使用MOPS的model checker（以下简称MC）。MC可以遍历程序

15、的每条路径，还可以匹配函数的返回地址和它的调用地址，支持流敏感、上下文敏感、路经敏感的安全漏洞分析。4 实验和分析本文提出的安全漏洞模型刻画以及漏洞检测方法已在自研制安全漏洞检测工具BinMc中实现应用。本节给出根据两种时序安全漏洞模型，使用BinMc进行的2组实验与分析结果。测试环境为2.6GHz AMD Opteron Server，8G RAM。4.1 实验1ftpd 0.17中存在错误放弃特权漏洞（CVE-2006-6008）。BinMc报告了4条从main函数到ftpd-popen的路径，经过分析其中2条为真实路径。在2条真实的路径中，程序调用execv()函数之前没有对setuid

16、()的返回制进行检查。rssh是一个与openssh结合使用的程序。BinMc在rssh-2.0.0的可执行程序rssh_chroot_helper中报告了2条路径。经过分析，其中1条为真实路径。该路径没有检查setuid()的返回值，在之后的系统调用chdir()中使用用户输入作为参数，可能将用户的根目录更改为任意目录。该安全漏洞还没有报告过。实验1结果如表1所示。表1实验1结果程序名可执行程序大小/KB生成路径真实路径处理时间（分:秒）Linux-ftpd 0.17Ftpd58421:20rssh 2.0.0rssh_chroot_helper9210:0.44.2 实验2unzip-5.

17、52存在文件竞争条件漏洞(CVE-2005-2475)。在实验中BinMc报告2条从入口函数start开始的路径，经过分析其中1条为真实路径。使用Schwarz的文件竞争模型检查，BinMc报告了17条路径。TTSP是一种将集中式应用程序部署在瘦客户端上的程序。BinMc在TTSP的可执行程序thintux-vncpasswd中报告1条可能产生条件竞争的路径，经过分析该路径是真实路径。在该路径中首先打开文件，然后修改该文件的属性。这使得供给者可能在两个操作的时间窗内替换该文件。使用Schwarz的文件竞争模型无法检查出该漏洞。实验2结果如表2所示。表2实验2结果程序名可执行程序大小/KB生成路

18、径真实路径处理时间（分:秒）unzip5.52unzip99213:14TTSPThinux_vnc paxxwd1110:114.3 性能分析从实验中可见BinMc的结果存在误报，这些误报是由于使用上下文无关语言为可执行路径建模引入的不精确性。这种误报可以通过数据流分析进行消减。BinMc也可能存在漏报，这是由于以下几点原因造成的：1)IDA Pro反汇编错误；2)没有考虑在控制流图中没有出现的控制流；3)有些漏洞只在某些特定的配置下存在。其中原因1)可以通过改进反汇编算法进行改进，原因2)和3)是静态分析方法共同存在的弱点。5 结束语本文提出了一种针对二进制可执行程序的时序安全检查方法，以

19、自动识别程序中存在的时序安全漏洞。同时本文提出了两种时序安全漏洞模型。通过两组实验，证明该方法可以有效地辅助在可执行程序中验证和发现时序安全漏洞。对可执行程序的静态时序安全漏洞检查仍有以下工作值得进一步研究：1)通过对分支语句的条件分析减少误报。2)使用污染数据分析辅助时序安全漏洞分析。参考文献：1BALL T , RAJAMANI S K. Automatically validating temporal safety properties of interfacesA. Proc 8th Intl SPIN Workshop on Model Checking of SoftwareC.

20、 2001. 103-122.2SCHWARZ B, CHEN H, WAGNER D. Model checking an entire linux distribution for security violationsA. Proc Annual. Computer Security Applications ConferenceC. 2005. 13-22.3BORISOV N, JOHNSON R, SASTRY N, et al. Fixing races for fun and profit: how to abuse atimeA. 13th USENIX Security S

21、ymposiumC. 2005. 303-314.4WEI J, PU C. TOCTTOU vulnerabilities in UNIX-style file systems: an anatomical studyA. 4th USENIX Conference on File and Storage TechnologiesC. 2005. 12.5阳小奇,刘坚.一种基于契约的跨过程安全分析方法J.西安电子科技大学学报, 2006, 33(3):390-394.YANG X Q, LIU J. Acontract-based interprocedural safety analysi

22、s methodJ. Journal of Xidian University, 2006, 33(3):390-394.6GANAPATHY V, SESHIA S A, JHA S, et al. Automatic discovery of API-level exploitsA. 27th International Conference on Software EngineeringC. 2005. 312-321.7WEI T, MAO J, ZOU W, et al. Structuring 2-way branches in binary executablesA. To Ap

23、pear in 31st Annual IEEE International Computer Software and Applications ConferenceC.2007.8WEI T, MAO J, ZOU W, et al. A new algorithm for identifying loops in decompilationA. To Appear in the 14th International Static Analysis SymposiumC. 2007.9CIFUENTES C. Structuring decompiled graphsA. International Conference on Compiler ConstructionC. 1996. 91-105.作者简介：李佳静（1979-），女，黑龙江大庆人，北京大学博士生，主要研究方向为软件脆弱性分析、恶意代码分析。毛剑（1978-），女，江苏溧水人，博士，主要研究方向为网络与信息安全。韦韬（1975-），男，江苏江都人，博士，主要研究方向为反编译，软件脆弱性分析、恶意代码分析。毛剑（1978-），女，江苏溧水人，博士，主要研究方向为网络与信息安全。