Our paper "Verifying the verifier: eBPF Range Analysis Verification" accepted at CAV 2023. Work with students Hari and Matan, and colleague Srinivas Narayana. We propose an automated method to check the correctness of range analysis in the Linux Kernel’s eBPF verifier.

We automatically generate verification conditions that encode the operation of eBPF verifier directly from Linux Kernel’s C source code and check it against our specification.

When we discover instances where the eBPF verifier is unsound, we propose a method to generate an eBPF program that demonstrates the mismatch between the abstract and the concrete semantics.

We automatically checks the soundness of the eBPF verifier for 16 versions of the eBPF verifier in the Linux Kernel ranging from 4.14 to 5.19. In this process, we have discovered new bugs in older versions and proved the soundness of range analysis in the latest kernel. Preprint will be available soon.

#Rutgers #RutgersCS #RutgersSAS #CAV2023