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

作　　者：Lili Xu Mingjie Xu Feng Li Wei Huo 

机构地区：[1]Institute of Information Engineering,Chinese Academy of Sciences,Beijing,China [2]School of Cyber Security,University of Chinese Academy of Sciences,Beijing,China

出　　处：《Cybersecurity》2018年第1期860-878,共19页网络空间安全科学与技术（英文）

基　　金：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).

摘　　要：The Integer-Overflow-to-Buffer-Overflow(IO2BO)vulnerability has been widely exploited by attackers to cause severe damages to computer systems.Automatically identifying this kind of vulnerability is critical for software security.Despite many works have been done to mitigate integer overflow,existing tools either report large number of false positives or introduce unacceptable time consumption.To address this problem,in this article we present a static analysis framework.It first constructs an inter-procedural call graph and utilizes taint analysis to accurately identify potential IO2BO vulnerabilities.Then it uses a light-weight method to further filter out false positives.Specifically,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 satisfiability.We 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 world.The experiment results show that our system can effectively and efficiently detect all known IO2BO vulnerabilities.

关 键 词：Integer-Overflow-to-Buffer-Overflow(IO2BO)vulnerability Inter-procedural dataflow analysis Taint analysis Path satisfiability 

分 类 号：O15[理学—数学]