Filtering false alarms of buffer overflow analysis using SMT solvers

详细信息    查看全文

• 作者：Youil Kim ; Jooyong Lee ; Hwansoo Han ; Kwang-Moo Choe
• 关键词：Buffer overflow ; Program analysis ; False alarm ; SMT solver
• 刊名：Information and Software Technology
• 出版年：2010
• 出版时间：February 2010
• 年：2010
• 卷：52
• 期：2
• 页码：210-219
• 全文大小：443 K

文摘

Buffer overflow detection using static analysis can provide a powerful tool for software programmers to find difficult bugs in C programs. Sound static analysis based on abstract interpretation, however, often suffers from false alarm problem. Although more precise abstraction can reduce the number of the false alarms in general, the cost to perform such analysis is often too high to be practical for large software. On the other hand, less precise abstraction is likely to be scalable in exchange for the increased false alarms. In order to attain both precision and scalability, we present a method that first applies less precise abstraction to find buffer overflow alarms fast, and selectively applies a more precise analysis only to the limited areas of code around the potential false alarms. In an attempt to develop the precise analysis of alarm filtering for large C programs, we perform a symbolic execution over the potential alarms found in the previous analysis, which is based on the abstract interpretation. Taking advantage of a state-of-art SMT solver, our precise analysis efficiently filters out a substantial number of false alarms. Our experiment with the test cases from three open source programs shows that our filtering method can reduce about 68 % of false alarms on average.