ELAID:detecting integer-Overflow-to-Buffer-Overflow vulnerabilities by light-weight and accurate static analysis

作     者：Lili Xu Mingjie Xu Feng Li Wei Huo Lili Xu;Mingjie Xu;Feng Li;Wei Huo

作者机构：Institute of Information EngineeringChinese Academy of SciencesBeijingChina School of Cyber SecurityUniversity of Chinese Academy of SciencesBeijingChina 

出 版 物：《Cybersecurity》 (网络空间安全科学与技术（英文）)

年 卷 期：2018年第1卷第1期

页      面：860-878页

核心收录：

学科分类：07[理学] 0701[理学-数学] 070101[理学-基础数学] 

基　　金：supported in part by the National Natural Science Foundation of China(Grant No.61802394,U1836209) Foundation of Science and Technology on Information Assurance Laboratory(No.KJ-17-110) National Key Research and Development Program of China(2016QY071405) Strategic Priority Research Program of the CAS(XDC02040100,XDC02030200,XDC02020200) 

主　　题：Integer-Overflow-to-Buffer-Overflow(IO2BO)vulnerability Inter-procedural dataflow analysis Taint analysis Path satisfiability 

摘      要：The Integer-Overflow-to-Buffer-Overflow(IO2BO)vulnerability has been widely exploited by attackers to cause severe damages to computer *** identifying this kind of vulnerability is critical for software *** many works have been done to mitigate integer overflow,existing tools either report large number of false positives or introduce unacceptable time *** address this problem,in this article we present a static analysis *** first constructs an inter-procedural call graph and utilizes taint analysis to accurately identify potential IO2BO *** it uses a light-weight method to further filter out false ***,it generates constraints representing the conditions under which a potential IO2BO vulnerability can be triggered,and feeds the constraints to SMT solver to decide their *** have implemented a prototype system ELAID based on LLVM,and evaluated it on 228 programs of the NIST’s SAMATE Juliet test suite and 14 known IO2BO vulnerabilities in real *** experiment results show that our system can effectively and efficiently detect all known IO2BO vulnerabilities.