KernelScript: Cross-Boundary Typed DSL for eBPF Applications
2026-07-27 • Programming Languages
Programming LanguagesOperating Systems
AI summaryⓘ
The authors explain that eBPF is a way to add custom programs inside the Linux kernel safely, but currently the code is split between different parts and can cause hidden errors. They created KernelScript, a special programming language that keeps all related code in one place and checks for mistakes before running. Their tests show that KernelScript catches bugs that usual methods miss and makes it easier to update code without breaking things, all while still working with existing tools.
eBPFLinux kerneltype systemKernelScriptprogram verifiermapsuser spaceXDPlibbpfDSL
Authors
Cong Wang, Siyuan Sun, Yusheng Zheng
Abstract
eBPF lets developers extend Linux with custom packet processing, tracing, and scheduling logic, and a verifier proves before execution that the code will not crash the kernel. The programming model, however, is fragmented: a single application spans kernel code, a userspace loader, and shared maps, yet the relationships among these pieces go unchecked. E.g. A map or event type defined differently on each side silently corrupts shared state. We observe that these cross-boundary relationships duplicate information that a type system can unify. We present KernelScript, a DSL that types maps, program handles, and execution domains in one source, then compiles to standard C through the original toolchain. We evaluate KernelScript on 43 eBPF workloads covering XDP, TC, kprobe, tracepoint, and struct_ops. KernelScript rejects cross-boundary bugs at compile time that standard C/libbpf still builds and loads, a unified source shrinks the diffs for cross-boundary changes by 5x, and generated code remains compatible with the existing toolchain.