基于约束系统模型的缓冲区溢出漏洞检测系统
|
摘要
软件安全检测是保证计算机系统安全、避免遭受恶意攻击的重要技术手段。鉴于静态检测技术自动化程度高、分析速度快等优点,研究静态漏洞检测技术具有重要意义。
针对缓冲区溢出漏洞,本文在深入分析其形成机理的基础之上,综合约束分析、模型检测两种技术对程序缓冲区进行跟踪分析,通过在缓冲区操作程序点插入缓冲区属性初始化、属性传递和属性断言等信息,构建了缓冲区属性约束系统,从而采用模型检测技术通过求解约束系统完成程序缓冲区漏洞的检测。
针对约束分析的精确性问题,本文提出了基于GCC抽象语法树的过程内别名分析算法,该算法通过指针变量分析生成指针变量的别名信息集合,并完成集合元素属性与互为别名的缓冲区属性信息的变换映射,从而有效地提高了分析精确性。
在关键技术研究的基础上,本文设计并实现了基于约束系统模型求解的缓冲区溢出漏洞自动检测原型系统:CodeAnalysis。测试结果表明:该系统能够检测出典型的已知缓冲区溢出漏洞,并且针对未知的缓冲区漏洞,该系统亦能有效地检测并定位。
Software safety detecting is playing an important way to protect Computer System and avoid being attacted, depending on Static Analysis’s excellences such as higher automatization, researching the technologies of Static Analysis is very important.
Aiming at Buffer Overflow Vulnerability, this paper has researched its base principle, and combined constraint analysis and model checking technology which have been applied in detecting BOVs sepatately, through following analysis to insert information as buffer attributes initialization、attributes transfer and attributes assert,then has constructed buffer Attributes constraint system, and adopted model checking technology to solve constraint system in order to detect BOVs among c programs.
For the problem of constraint analysis’accuracy, this paper has brought forward alias analysis algorithm during process based on GCC Abstract Syntax Tree, by pointer variable analysis this algorithm has generated alias information assemble, and has finished the exchange mapping between assemble element attributes and attributes of alias buffer information, so the accuracy is increased effectively.
Based on the analysis of pivotal technology above, this paper has designed a prototype system to detect BOVs based on constraint system model checking, the testing result shows that this prototype system can discover typical known vulnerabilities,and for unknown vulnerabilities this system aslo can locate effectively.
针对缓冲区溢出漏洞,本文在深入分析其形成机理的基础之上,综合约束分析、模型检测两种技术对程序缓冲区进行跟踪分析,通过在缓冲区操作程序点插入缓冲区属性初始化、属性传递和属性断言等信息,构建了缓冲区属性约束系统,从而采用模型检测技术通过求解约束系统完成程序缓冲区漏洞的检测。
针对约束分析的精确性问题,本文提出了基于GCC抽象语法树的过程内别名分析算法,该算法通过指针变量分析生成指针变量的别名信息集合,并完成集合元素属性与互为别名的缓冲区属性信息的变换映射,从而有效地提高了分析精确性。
在关键技术研究的基础上,本文设计并实现了基于约束系统模型求解的缓冲区溢出漏洞自动检测原型系统:CodeAnalysis。测试结果表明:该系统能够检测出典型的已知缓冲区溢出漏洞,并且针对未知的缓冲区漏洞,该系统亦能有效地检测并定位。
Software safety detecting is playing an important way to protect Computer System and avoid being attacted, depending on Static Analysis’s excellences such as higher automatization, researching the technologies of Static Analysis is very important.
Aiming at Buffer Overflow Vulnerability, this paper has researched its base principle, and combined constraint analysis and model checking technology which have been applied in detecting BOVs sepatately, through following analysis to insert information as buffer attributes initialization、attributes transfer and attributes assert,then has constructed buffer Attributes constraint system, and adopted model checking technology to solve constraint system in order to detect BOVs among c programs.
For the problem of constraint analysis’accuracy, this paper has brought forward alias analysis algorithm during process based on GCC Abstract Syntax Tree, by pointer variable analysis this algorithm has generated alias information assemble, and has finished the exchange mapping between assemble element attributes and attributes of alias buffer information, so the accuracy is increased effectively.
Based on the analysis of pivotal technology above, this paper has designed a prototype system to detect BOVs based on constraint system model checking, the testing result shows that this prototype system can discover typical known vulnerabilities,and for unknown vulnerabilities this system aslo can locate effectively.
引文
[1] Paul Q.Judge, The Next Generation of Messaging Threats[A], In: the RSA2005 conference[C]. San Francisco,2005-12.
[2] CERT. CERT/CC Statistics 1995-2008[EB/OL].: http://www.cert.org/stats/, 2009-02-12.
[3] nfocus.安全漏洞[EB/OL].: http://www.nsfocus.net/index.php?act=sec_bug, 2010-03.
[4] Buffer Overflows– What Are They and What Can I Do About Them. [EB/OL].: http://www.cert.org/ homeusers/buffer_overflow.html .2001-12..
[5] Internet Worm Resource:HomePage. [EB/OL].:http://worm.ccert.edu.cn/wiki/index.cgi?Home Page.2007.
[6] David Wheeler,Flawfinder Homepage[EB/OL].: http://www.dwheeler.com/flawfinder/, 2001
[7] J. Viega, J.T. Bloch, Y,Kohno, G. McGraw. ITS4: A static vulnerability scanner for Cand C++ code[A], In: 16th Annual Computer Security Applications Conference (ACSAC'00)[C], New Orleans, Louisiana,2000-11.
[8] Secure Software Solutions,Secure Software Announces Initial Release of RATS, [EB/OL].: http://www.securesw.com/rats/.
[9]夏一民,罗军,张民选.基于静态分析的安全漏洞检测技术研究[J].计算机科学,2006,33(20):279-282..
[10] J S FOSTER, M. FAHNDRICH, A. AIKEN. A theory of Type Qualifiers[A].In ACM SIGPLAN conference on programming language design and implementation(PLDI’99)[C]. Altanta, Georgia, 1999-5: 192-203.
[11] M. Das, S. Lerner, seigle M. Path sensitive program verification in polynomial time[A]. In: proc, of the ACM SIGPLAN 2002 conf—on programming Languages Design and Implementation Berlin[C].Germany.June 2002:57-68.
[12] BANE[EB/OL].http://www.cs .berkeley .edu /Research/Aiken/bane.html,2005-2:79~l11.
[13] Aiken A.Introduction to set constraint-based program analysis[J]. Science of Computer Programming,1999,35(2):79-111.
[14] G. J. Holznmnn. The model checker SPIN [J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295.
[15] SMV [EB/OL]. :http://www.cs.cmu.edu/~modelcheck/,2009-5.
[16] H. Chen, D. Wagner. MOPS:an infrastructure for examing security properties of software[A]. In: Conf. on Comp and Commun.Sec[C]. Berkeley:University of California at Berkeley, 2002-11: 235-244.
[17] Ball T, Rajamani SK. The SLAM project: Debugging system software via static analysis. In: Launchbury J, Mitchell JC, eds. Proc of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 1-3.
[18] BLAST, BLAST: Berkeley Lazy Abstraction Software Verification Tool [EB/OL].http://mtc.epfl.ch/software-tools/blast/index-epfl.php, 2008-7.
[19] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement for symbolic model checking[J]. Journal of the ACM, 2003,50(5):752-794.
[20] C. Flanagan, K. R. M. Leino, Houdini. An annotation assistant for ESC/Sava[R]. Notes in Computer Science 2021 ,FME 2001.Lecture,2001:500~517.
[21] W. Bush, J. Pincus, D. Sielaff.A static analyzer for finding dynamic programming errors[A]. In:Software-practice and Expenience[C]. New York, NY, USA: John Wiley & Sons, Inc ,2000-7-30: 755~802.
[22]张林,曾庆凯.软件安全漏洞的静态检测技术[J].计算机工程,2008,34(12):157-159.
[23] Cousot P, Cousot R. Systematic design of program analysis frameworks[A]. In: Proc. of the 6th POPL[C]. San Antonio: ACM Press, 1979: 69?282.
[24] Cousot P, Cousot R. Abstract interpretation based program testing[A]. In: Proc. of the SSGRR 2000 Computer & eBusiness Int’l Conf[C]. Compactdisk ,2000:248.
[25] Mangleme[EB/OL]: http://lcamtuf.coredump.cx/mangleme/mangle.cgi, 2006-04- 02.
[26] Hamachi[EB/OL]: http://metasploit.com/users/hdm/tools/hamachi/hamachi.html, 2006-07- 03.
[27] Axman[EB/OL]: http://metasploit.com/users/hdm/tools/axman, 2007-09-01.
[28] Spike [EB/OL]: http://lists.immunitysec.com/mailman/listinfo/spike, 2006-07-03.
[29] Daniel P.Bovet, Marco Cesati. Understanding the Linux Kernel [M]. O’Reilly Media, Inc. Seprember 2008:807.
[30] Wagner D, Foster J, Brewer E, Aiken A. A first step towards automated detection of buffer overrun vulnerabilities[A].In: In The 2000 Network and Distributed SystemsSecurity Conference[C]. San Diego, CA, February 2000:3-17.
[31] Cousot P. Formal language, grammar and set-constraint-based program analysis by abstract interpretation[A]. In: Functional Programming and Computer Architecture[C],ACM 1995:170-181.
[32] Henzinger T A, Jhala R, Majumdar R, et al. Lazy Abstraction [A]. In: 29th Annual Symposium on Principles of Programming Languages[C]. Springer. 2002: 58-70.
[33] Clarke EM, Grumberg O, Peled D.Model Checking[M]. MIT, 1999.
[34] Henzinger TA, Jhala R, Majumdar R, Necula GC, Sutre G, Weimer W. Temporal-safety poofs for systems code[A]. In: Proc.CAV, LNCS 2404[C]. Springer, 2002:526-538.
[35] Clarke EM, Grumberg O, Jha S, Yuan Lu, Veith H. Counterexample-guided abstraction refinement for symbolic model checking[A]. In J.ACM, Sep. 2003:752-794.
[36] Chaki S, Groce A, Strichman O, Explaining Abstract Counterexamples [A], In: 12th International Symposium on Foundations of Software Engineering (FSE) 2005[C]. Newport Beach, California. 2005:73-82.
[37] G. C. Necula, S. McPeak, S. P. Rahul, and W. eimer. CIL: Intermediate language and tools for analysis and transformation of C programs[A]. In: Compiler Construction, Lecture Notesin Computer Science 2304[C], Springer, 2002: 213-228.
[38] Libxml2[EB/OL]: http://xmlsoft.org/index.html,2008.
[39] Alfred V.Aho, Monica S.Lam, Ravi Sethi et al.编译原理[M].北京:机械工业出版社, 2009.
[40] Emami M, Ghiya R, HendrenL. Context-sensitive interprocedual points-to analysis in the presence of function pointers[A]. In: Proceedings of ACM S IGPLAN’94 Conference on Programming Language Design and Implementation[C].ACM, 1994: 242~256.
[41]黄波,臧斌宇,俞一峻等。指针数组的过程内别名分析[J]。软件学报,1999, 10(06):41-48.
[42] B.Steensgaard. Points-to analysis in almost linear time[A]. In: Symposium on Principles of Programming Languages[C], ACM,1996: 32-41.
[43] Home page of gzip software[EB/OL].: http://www.gzip.org/,2003-6.
[44] Home page of glftpd software[EB/OL].: http://www.glftpd.com/,2005-12.
[45] Shankar U, Talwar K, Foster JS, Wagner D. Detecting Format String Vulnerabilities with Type Qualifiers [A]. In: Proceeding of the 10th USENIX Security Symp [C]. Washington: SENIX, 2001:201-218.
[46] Jiri Barnat, Lubos Brim, Petr Rockai: DiVinE Multi-Core– A Parallel LTL Model-Checker[A]. Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis[C]. Springer, Seoul, Korea,2008: 234–239.
[47] J. Barnat and P. Rockai. Shared Hash Tables in Parallel Model Checking[A]. In : Participant proceedings of the Sixth International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2007), CTIT, University of Twente,2007:79-91.
[48] J. Barnat, L. Brim, I. Cerna, M. Ceska, and J. Tumova. Jana Tumova: ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems[C]. In:. 5rd International Conference on Quantitative Evaluation of Systems (QEST’08), IEEE CS Press,,2008: 77–78.
[2] CERT. CERT/CC Statistics 1995-2008[EB/OL].: http://www.cert.org/stats/, 2009-02-12.
[3] nfocus.安全漏洞[EB/OL].: http://www.nsfocus.net/index.php?act=sec_bug, 2010-03.
[4] Buffer Overflows– What Are They and What Can I Do About Them. [EB/OL].: http://www.cert.org/ homeusers/buffer_overflow.html .2001-12..
[5] Internet Worm Resource:HomePage. [EB/OL].:http://worm.ccert.edu.cn/wiki/index.cgi?Home Page.2007.
[6] David Wheeler,Flawfinder Homepage[EB/OL].: http://www.dwheeler.com/flawfinder/, 2001
[7] J. Viega, J.T. Bloch, Y,Kohno, G. McGraw. ITS4: A static vulnerability scanner for Cand C++ code[A], In: 16th Annual Computer Security Applications Conference (ACSAC'00)[C], New Orleans, Louisiana,2000-11.
[8] Secure Software Solutions,Secure Software Announces Initial Release of RATS, [EB/OL].: http://www.securesw.com/rats/.
[9]夏一民,罗军,张民选.基于静态分析的安全漏洞检测技术研究[J].计算机科学,2006,33(20):279-282..
[10] J S FOSTER, M. FAHNDRICH, A. AIKEN. A theory of Type Qualifiers[A].In ACM SIGPLAN conference on programming language design and implementation(PLDI’99)[C]. Altanta, Georgia, 1999-5: 192-203.
[11] M. Das, S. Lerner, seigle M. Path sensitive program verification in polynomial time[A]. In: proc, of the ACM SIGPLAN 2002 conf—on programming Languages Design and Implementation Berlin[C].Germany.June 2002:57-68.
[12] BANE[EB/OL].http://www.cs .berkeley .edu /Research/Aiken/bane.html,2005-2:79~l11.
[13] Aiken A.Introduction to set constraint-based program analysis[J]. Science of Computer Programming,1999,35(2):79-111.
[14] G. J. Holznmnn. The model checker SPIN [J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295.
[15] SMV [EB/OL]. :http://www.cs.cmu.edu/~modelcheck/,2009-5.
[16] H. Chen, D. Wagner. MOPS:an infrastructure for examing security properties of software[A]. In: Conf. on Comp and Commun.Sec[C]. Berkeley:University of California at Berkeley, 2002-11: 235-244.
[17] Ball T, Rajamani SK. The SLAM project: Debugging system software via static analysis. In: Launchbury J, Mitchell JC, eds. Proc of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 1-3.
[18] BLAST, BLAST: Berkeley Lazy Abstraction Software Verification Tool [EB/OL].http://mtc.epfl.ch/software-tools/blast/index-epfl.php, 2008-7.
[19] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement for symbolic model checking[J]. Journal of the ACM, 2003,50(5):752-794.
[20] C. Flanagan, K. R. M. Leino, Houdini. An annotation assistant for ESC/Sava[R]. Notes in Computer Science 2021 ,FME 2001.Lecture,2001:500~517.
[21] W. Bush, J. Pincus, D. Sielaff.A static analyzer for finding dynamic programming errors[A]. In:Software-practice and Expenience[C]. New York, NY, USA: John Wiley & Sons, Inc ,2000-7-30: 755~802.
[22]张林,曾庆凯.软件安全漏洞的静态检测技术[J].计算机工程,2008,34(12):157-159.
[23] Cousot P, Cousot R. Systematic design of program analysis frameworks[A]. In: Proc. of the 6th POPL[C]. San Antonio: ACM Press, 1979: 69?282.
[24] Cousot P, Cousot R. Abstract interpretation based program testing[A]. In: Proc. of the SSGRR 2000 Computer & eBusiness Int’l Conf[C]. Compactdisk ,2000:248.
[25] Mangleme[EB/OL]: http://lcamtuf.coredump.cx/mangleme/mangle.cgi, 2006-04- 02.
[26] Hamachi[EB/OL]: http://metasploit.com/users/hdm/tools/hamachi/hamachi.html, 2006-07- 03.
[27] Axman[EB/OL]: http://metasploit.com/users/hdm/tools/axman, 2007-09-01.
[28] Spike [EB/OL]: http://lists.immunitysec.com/mailman/listinfo/spike, 2006-07-03.
[29] Daniel P.Bovet, Marco Cesati. Understanding the Linux Kernel [M]. O’Reilly Media, Inc. Seprember 2008:807.
[30] Wagner D, Foster J, Brewer E, Aiken A. A first step towards automated detection of buffer overrun vulnerabilities[A].In: In The 2000 Network and Distributed SystemsSecurity Conference[C]. San Diego, CA, February 2000:3-17.
[31] Cousot P. Formal language, grammar and set-constraint-based program analysis by abstract interpretation[A]. In: Functional Programming and Computer Architecture[C],ACM 1995:170-181.
[32] Henzinger T A, Jhala R, Majumdar R, et al. Lazy Abstraction [A]. In: 29th Annual Symposium on Principles of Programming Languages[C]. Springer. 2002: 58-70.
[33] Clarke EM, Grumberg O, Peled D.Model Checking[M]. MIT, 1999.
[34] Henzinger TA, Jhala R, Majumdar R, Necula GC, Sutre G, Weimer W. Temporal-safety poofs for systems code[A]. In: Proc.CAV, LNCS 2404[C]. Springer, 2002:526-538.
[35] Clarke EM, Grumberg O, Jha S, Yuan Lu, Veith H. Counterexample-guided abstraction refinement for symbolic model checking[A]. In J.ACM, Sep. 2003:752-794.
[36] Chaki S, Groce A, Strichman O, Explaining Abstract Counterexamples [A], In: 12th International Symposium on Foundations of Software Engineering (FSE) 2005[C]. Newport Beach, California. 2005:73-82.
[37] G. C. Necula, S. McPeak, S. P. Rahul, and W. eimer. CIL: Intermediate language and tools for analysis and transformation of C programs[A]. In: Compiler Construction, Lecture Notesin Computer Science 2304[C], Springer, 2002: 213-228.
[38] Libxml2[EB/OL]: http://xmlsoft.org/index.html,2008.
[39] Alfred V.Aho, Monica S.Lam, Ravi Sethi et al.编译原理[M].北京:机械工业出版社, 2009.
[40] Emami M, Ghiya R, HendrenL. Context-sensitive interprocedual points-to analysis in the presence of function pointers[A]. In: Proceedings of ACM S IGPLAN’94 Conference on Programming Language Design and Implementation[C].ACM, 1994: 242~256.
[41]黄波,臧斌宇,俞一峻等。指针数组的过程内别名分析[J]。软件学报,1999, 10(06):41-48.
[42] B.Steensgaard. Points-to analysis in almost linear time[A]. In: Symposium on Principles of Programming Languages[C], ACM,1996: 32-41.
[43] Home page of gzip software[EB/OL].: http://www.gzip.org/,2003-6.
[44] Home page of glftpd software[EB/OL].: http://www.glftpd.com/,2005-12.
[45] Shankar U, Talwar K, Foster JS, Wagner D. Detecting Format String Vulnerabilities with Type Qualifiers [A]. In: Proceeding of the 10th USENIX Security Symp [C]. Washington: SENIX, 2001:201-218.
[46] Jiri Barnat, Lubos Brim, Petr Rockai: DiVinE Multi-Core– A Parallel LTL Model-Checker[A]. Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis[C]. Springer, Seoul, Korea,2008: 234–239.
[47] J. Barnat and P. Rockai. Shared Hash Tables in Parallel Model Checking[A]. In : Participant proceedings of the Sixth International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2007), CTIT, University of Twente,2007:79-91.
[48] J. Barnat, L. Brim, I. Cerna, M. Ceska, and J. Tumova. Jana Tumova: ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems[C]. In:. 5rd International Conference on Quantitative Evaluation of Systems (QEST’08), IEEE CS Press,,2008: 77–78.