Zheng, Y. (CSE) – Extending eBPF Beyond Kernel Extensions: Verified Interfaces for Runtime System Extensibility

Modern system software increasingly needs runtime extensibility: userspace applications need safe ways to expose domain-specific extension points, GPU resource management needs workload-specific memory and scheduling policies, and kernel eBPF JIT compilers need different runtime optimizations as workloads and hardware vary. However, built-in policies are safe but difficult to specialize across rapidly changing workloads and hardware environments, limiting efficiency, while code modifications are flexible but difficult to deploy safely. This dissertation argues that verified eBPF interfaces can turn eBPF from a kernel-extension mechanism into a general substrate for safe runtime extensibility. In this model, trusted mechanisms expose narrow, constrained programmable hooks; extensions declare their requirements; verifier-enforced checks preserve safety; and execution remains low-overhead.

I develop this thesis through three systems spanning userspace applications, heterogeneous GPU subsystems, and the kernel eBPF compiler itself. EIM, implemented in bpftime, applies verified eBPF interfaces to userspace applications, allowing application behavior to be extended through explicit constraints and efficient userspace eBPF execution. gpu_ext extends the same idea to heterogeneous systems by exposing programmable resource management hooks for GPU memory and scheduling policy across driver and device. BpfReJIT with kinsn makes the eBPF JIT compiler itself extensible: it enables runtime-guided optimization through dynamic recompilation and extends eBPF bytecode to express diverse hardware capabilities. Together, these systems show how verified eBPF interfaces can support safe programmability, separation of policy and mechanisms, and runtime specialization across applications, GPU subsystems, and the kernel JIT infrastructure.

Event Host: Yusheng Zheng, Ph.D. Student, Computer Science & Engineering

Advisor: Andi Quinn

Zoom: 504 350 0245

Passcode: 521336