一句话：提出基于抽象解释数值不变式的数据共享分析器，可靠且精确地识别中断驱动程序中的共享数据访问。
中断驱动程序广泛用于安全关键领域，任务与中断之间不正确的数据共享是并发缺陷的主要来源，因此数据共享分析对推理其并发行为至关重要。由于数据访问形式多样，现有工具在应用于中断驱动程序时误报和漏报都很严重。本文提出工具 SpecChecker-ISA：它使用以数值不变式参数化的内存访问模型来刻画各种形式的数据访问，这些不变式由基于抽象解释的数值分析计算得到，随后通过数值 meet 运算合并得到最终的数据共享结果，从而兼顾分析的可靠性与精度。在 4 个真实航天嵌入式软件上的实验表明，SpecChecker-ISA 能找出全部共享数据访问且误报很少，显著优于现有工具。
Concurrency bugs are common in interrupt-driven programs, which are widely used in safety-critical areas. These bugs are often caused by incorrect data sharing among tasks and interrupts. Therefore, data sharing analysis is crucial to reason about the concurrency behaviours of interrupt-driven programs. Due to the variety of data access forms, existing tools suffer from both extensive false positives and false negatives while applying to interrupt-driven programs. This paper presents SpecChecker-ISA, a tool that provides sound and precise data sharing analysis for interrupt-driven embedded software. The tool uses a memory access model parameterized by numerical invariants, which are computed by abstract interpretation based value analysis, to describe data accesses of various kinds, and then uses numerical meet operations to obtain the final result of data sharing. Our experiments on 4 real-world aerospace embedded software show that SpecChecker-ISA can find all shared data accesses with few false positives, significantly outperforming other existing tools. The demo can be accessed at https://github.com/wangilson/specchecker-isa.
DOI 原文 ·
@inproceedings{paperbot7374,
title = {SpecChecker-ISA: a data sharing analyzer for interrupt-driven embedded software},
author = {Boxiang Wang and Rui Chen and Chao Li and Tingting Yu and Dongdong Gao and Mengfei Yang},
booktitle = {ISSTA},
year = {2022},
doi = {10.1145/3533767.3543295}
}