一句话：提出 intAtom，通过分阶段路径剪枝与约束求解，精确高效检测中断驱动程序中的原子性违反。
中断驱动程序广泛用于航天等安全关键领域，但中断的不确定交错会引发并发缺陷，其中原子性违反危害较大。已有基于模式的检测难以兼顾精度与可扩展性。本文提出 intAtom：先用数据流分析与访问交错模式匹配识别候选违反；再分析被抢占任务/中断中连续访问间的路径可行性以识别原子性意图并过滤候选；最后通过符号摘要与代表性抢占点选择的模块化路径剪枝，结合约束求解消除不可行路径。路径可行性检查基于稀疏值流分析，提升可扩展性。在基准和6个真实航天嵌入式程序上，误报降低72%，检测速度提升3倍，平均误报率19.6%，发现19个开发者确认的缺陷。
Interrupt-driven programs are widely used in aerospace and other safety-critical areas. However, uncertain interleaving execution of interrupts may cause concurrency bugs, which could result in serious safety problems. Most of the previous researches tackling the detection of interrupt concurrency bugs focus on data races, that are usually benign as shown in empirical studies. Some studies focus on pattern-based atomicity violations that are most likely harmful. However, they cannot achieve simultaneous high precision and scalability. This paper presents intAtom, a precise and efficient static detection technique for interrupt atomicity violations, described by access interleaving pattern. The key point is that it eliminates false violations by staged path pruning with constraint solving. It first identifies all the violation candidates using data flow analysis and access interleaving pattern matching. intAtom then analyzes the path feasibility between two consecutive accesses in preempted task/interrupt, in order to recognize the atomicity intention of developers, with the help of which it filters out some candidates. Finally, it performs a modular path pruning by constructing symbolic summary and representative preemption points selection to eliminate the infeasible path in concurrent context efficiently. All the path feasibility checking processes are based on sparse value-flow analysis, which makes intAtom scalable. intAtom is evaluated on a benchmark and 6 real-world aerospace embedded programs. The experimental results show that intAtom reduces the false positive by 72% and improves the detection speed by 3 times, compared to the state-of-the-art methods. Furthermore, it can finish analyzing the real-world aerospace embedded software very fast with an average FP rate of 19.6%, while finding 19 bugs that were confirmed by developers.
DOI 原文 ·
@inproceedings{paperbot7383,
title = {Precise and efficient atomicity violation detection for interrupt-driven programs via staged path pruning},
author = {Chao Li and Rui Chen and Boxiang Wang and Tingting Yu and Dongdong Gao and Mengfei Yang},
booktitle = {ISSTA},
year = {2022},
doi = {10.1145/3533767.3534412}
}