一句话：提出基于程序验证的方法检测中断驱动程序中的数据竞争漏洞，旨在消除静态分析中的误报。
中断驱动程序中数据竞争问题普遍存在，且由于中断交错复杂而难以发现。静态分析是检测此类问题的主流技术，但现有方法难以处理中断的同步机制，导致大量误报，因此消除误报成为精确检测数据竞争的主要挑战。本文提出一种基于程序验证的方法来发现中断驱动程序中的数据竞争漏洞，试图借助程序验证技术提升检测精度，从而应对中断同步机制带来的误报问题。摘要未给出具体方法细节与实验评估结果。
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.
DOI 原文 ·
@inproceedings{paperbot6023,
title = {A program verification based approach to find data race vulnerabilities in interrupt-driven program},
author = {Haining Feng},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3418925}
}