一句话：提出静态分析工具 Spinner，检测 eBPF 运行时中因上下文混淆与嵌套程序递归调用导致的锁违规。
eBPF 允许在不修改源码或加载内核模块的情况下扩展内核能力，但其内核级运行环境使锁使用错误可能导致死锁、系统挂起等严重后果。本文提出 Spinner，一个针对 eBPF 运行时的锁违规静态检测工具。Spinner 检测两类问题：(1) 上下文混淆，即 eBPF helper 函数在特定执行上下文下使用了不正确的加锁原语；(2) helper 函数中的锁可能被嵌套 eBPF 程序递归调用。两者均可能引发死锁。在 Linux eBPF 子系统的评估中，Spinner 共发现 34 个锁违规 bug，其中仅 5 个曾被 Syzbot 发现，表明其能有效补充现有动态测试手段。
The eBPF technology is widely used for many applications, including tracing, packet filtering, network usage monitoring, and so on. The versatility of eBPF allows the kernel’s capabilities to be extended without needing to modify source code or load kernel modules. However, the eBPF subsystem may introduce new bugs that could lead to crashes, data loss, and other issues that can negatively impact system stability, reliability, availability, security, and overall performance. Specifically, locking violations, which occur when locks are not used correctly, can lead to problems like deadlocks and system hangs. Since eBPF operates at the kernel level, errors here have far-reaching consequences.To tackle this issue, we present Spinner, a tool for detecting locking violations in the eBPF runtime. Spinner uses static analysis to (1) detect cases of context confusion where incorrect locking primitives are used in eBPF helper functions given their execution context, and (2) identify locks in helper functions that can be called recursively using nested eBPF programs. Both of these situations could result in deadlocks. So far, Spinner has identified 34 locking violation bugs in the eBPF subsystem in Linux, only 5 of which were previously found by Syzbot.
DOI 原文 ·
@inproceedings{paperbot9358,
title = {Spinner: Detecting Locking Violations in the eBPF Runtime},
author = {Priya Govindasamy and Joseph Bursey and Hsin-Wei Hung and Ardalan Amiri Sani},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00180}
}