一句话:提出路径敏感且别名感知的类型状态分析框架 PATA,通过基于路径的别名分析提升 OS 缺陷检测精度与效率。
操作系统缺陷检测对系统可靠性与安全性至关重要,但静态类型状态分析常因别名关系识别不精确、类型状态跟踪和路径可行性验证开销高,而难以兼顾精度与可扩展性。本文提出 PATA 框架,基于控制流路径和访问路径进行路径敏感的别名分析,并利用所得别名关系降低类型状态跟踪与路径可行性验证成本,从而提升面向大规模 OS 代码的缺陷检测效率。作者在 Linux 内核及 Zephyr、RIOT、TencentOS-tiny 三个 IoT OS 上评估 PATA,检测空指针解引用、未初始化变量访问和内存泄漏三类缺陷。PATA 共发现 574 个真实缺陷,误报率为 28%,其中 206 个已被四个 OS 的开发者确认;与七个先进静态方法相比,PATA 能发现它们遗漏的真实缺陷,且误报率更低。
Operating system (OS) is the cornerstone for modern computer systems. It manages devices and provides fundamental service for user-level applications. Thus, detecting bugs in OSes is important to improve reliability and security of computer systems. Static typestate analysis is a common technique for detecting different types of bugs, but it is often inaccurate or unscalable for large-size OS code, due to imprecision of identifying alias relationships as well as high costs of typestate tracking and path-feasibility validation. In this paper, we present PATA, a novel path-sensitive and aliasaware typestate analysis framework to detect OS bugs. To improve the precision of identifying alias relationships in OS code, PATA performs a path-based alias analysis based on control-flow paths and access paths. With these alias relationships, PATA reduces the costs of typestate tracking and path-feasibility validation, to boost the efficiency of path-sensitive typestate analysis for bug detection. We have evaluated PATA on the Linux kernel and three popular IoT OSes (Zephyr, RIOT and TencentOS-tiny) to detect three common types of bugs (null-pointer dereferences, uninitialized variable accesses and memory leaks). PATA finds 574 real bugs with a false positive rate of 28%. 206 of these bugs have been confirmed by the developers of the four OSes.We also compare PATA to seven state-of-the-art static approaches (Cppcheck, Coccinelle, Smatch,CSA, Infer, Saber and SVF). PATA finds many real bugs missed by them, with a lower false positive rate.