Filtering false alarms of buffer overflow analysis using SMT solvers

Buffer overflow detection using static analysis can provide a powerful tool for software ers to find difficult bugs in C programs. Sound static analysis based on abstract interpretation, however, often suffers from false alarm problem. Although more precise ion 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, cise 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 cise 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, based on the abstract interpretation. Taking advanta...

• Type: Journal
• Year: 2010
• Where: INFSOF
• Authors: Youil Kim, Jooyong Lee, Hwansoo Han, Kwang-Moo Choe
• Keywords: Analysis, False Alarm, INFSOF 2010, Knowledge Management, Precise Analysis