Due to the non-deterministic occurring of interrupt service routines, vulnerabilities of interrupt-driven programs, such as data race and atomicity violation, are usually hard to discover. Static analysis is an effective method for vulnerability analysis of interrupt-driven programs. However, existing techniques usually produce a large number of false alarms, which limits the application of static analysis in practice. To achieve high precision in vulnerability analysis of interrupt-driven programs, this paper proposes a program verification enhanced precise analysis method. For each potential vulnerability detected by static analysis, we propose a vulnerability validation approach which employs program verification to further automatically verify its feasibility. We have implemented a prototype of our method on top of CBMC. Experimental results on both an academic benchmark and 24 real-world programs show that our method can successfully identify true vulnerabilities and achieve a high precise analysis.

The data race problem is common in the interrupt-driven program, and it is difficult to find as a result of complicated interrupt interleaving. Static analysis is a mainstream technology to detect those problems, however, the synchronization mechanism of interrupt is hard to be processed by the existing method, which brings many false alarms. Eliminating false alarms in static analysis is the main challenge for precisely data race detection.