Details

Autor(en) / Beteiligte

• Feng, Haining

Titel

A program verification based approach to find data race vulnerabilities in interrupt-driven program

Ist Teil von

• 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2020, p.1361-1363

Ort / Verlag

New York, NY, USA: ACM

Erscheinungsjahr

2020

Link zum Volltext

• IEEE_Xplore

Quelle

IEEE Xplore Digital Library

Beschreibungen/Notizen

• 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. In this paper, we present a framework of static analysis combined with program verification, which performs static analysis to find all potential races, and then verifies every race to eliminate false alarms. The experiment results on related race benchmarks show that our implementation finds all race bugs in the phase of static analysis, and eliminates all false alarms through program verification.