paperbot · PL 论文追踪

全部论文 待读 收藏

P1 UBITect: a precise and scalable method to detect use-before-initialization bugs in Linux kernel

UBITect:一种精确且可扩展的 Linux 内核未初始化使用缺陷检测方法
FSE Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2020匹配度 6/10 · 该论文属于程序分析与静态分析工具,结合流敏感类型限定符分析和符号执行,并在 Linux 内核中落地,和用户偏好的“理论+工程落地、问题驱动”方向相关;但它不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,因此并非当前研究画像的核心交叉方向。引用 33 inbox
Yizhuo Zhai, Yu Hao, Hang Zhang, Daimeng Wang, Chengyu Song, Zhiyun Qian, Mohsen Lesani, Srikanth V. Krishnamurthy, Paul Yu
crossref: 2026-09-12

AI 速览

一句话:结合流敏感类型限定符分析与符号执行,实现 Linux 内核中精确且可扩展的未初始化使用缺陷检测。

Linux 内核中的 use-before-initialization(UBI)缺陷可导致信息泄露和权限提升。强制初始化可能引入 NULL 指针解引用等未定义行为,因此检测并人工修补是更好的缓解方式。精确检测 UBI 需要路径敏感分析,跟踪变量在各执行路径上的初始化状态,但这难以扩展到整个内核。UBITect 将流敏感类型限定符分析与符号执行结合:限定符分析筛选可能引发 UBI 的变量,并引导符号执行精确检查;它无需人工注解,也不修改源码或中间表示。在 Linux 4.14 上,它报告 190 个缺陷,其中 78 个被判为真阳性,52 个被维护者确认。

问题
Linux 内核中的 UBI 缺陷可造成信息泄露和权限提升,而强制初始化可能带来未定义行为;精确检测需要路径敏感跟踪,却难以扩展到整个内核。
方法
UBITect 结合流敏感的类型限定符分析与符号执行,由可扩展的限定符分析引导符号执行检查可能发生 UBI 的变量,且无需人工注解或修改源码/IR。
评估
在 Linux 内核 4.14 上评估,UBITect 报告 190 个缺陷,其中 78 个被作者视为真阳性,52 个获 Linux 维护者确认。
原文摘要(Abstract)

Use-before-Initialization (UBI) bugs in the Linux kernel have serious security impacts, such as information leakage and privilege escalation. Developers are adopting forced initialization to cope with UBI bugs, but this approach can still lead to undefined behaviors (e.g., NULL pointer dereference). As it is hard to infer correct initialization values, we believe that the best way to mitigate UBI bugs is detection and manual patching. Precise detection of UBI bugs requires path-sensitive analysis. The detector needs to track an associated variable’s initialization status along all the possible program execution paths to its uses. However, such exhaustive analysis prevents the detection from scaling to the whole Linux kernel. This paper presents UBITect, a UBI bug finding tool which combines flow-sensitive type qualifier analysis and symbolic execution to perform precise and scalable UBI bug detection. The scalable qualifier analysis guides symbolic execution to analyze variables that are likely to cause UBI bugs. UBITect also does not require manual effort for annotations and hence, it can be directly applied to the kernel without any source code or intermediate representation (IR) change. On the Linux kernel version 4.14, UBITect reported 190 bugs, among which 78 bugs were deemed by us as true positives and 52 were confirmed by Linux maintainers.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot5826,
  title = {UBITect: a precise and scalable method to detect use-before-initialization bugs in Linux kernel},
  author = {Yizhuo Zhai and Yu Hao and Hang Zhang and Daimeng Wang and Chengyu Song and Zhiyun Qian and Mohsen Lesani and Srikanth V. Krishnamurthy and Paul Yu},
  booktitle = {FSE},
  year = {2020},
  doi = {10.1145/3368089.3409686}
}