Hi, We wanted to let you know about our upcoming research paper [1] on checking the soundness of range analysis in the eBPF verifier. Specifically, we were able to use abstract interpretation theory to check whether the verifier can be tricked into constructing a range or tnum for a register while its concrete value deviates from it. We have checked soundness of the kernel's cross-domain analysis (4 different intervals, tristate) starting directly from the kernel source code. Here are our salient results: (1) We have showed that the range analyses corresponding to all arithmetic (except multiplication), logic, and branching instructions in kernels starting from 5.13 through 5.19 (the latest we checked) are sound. (2) For kernels where our analysis did reveal a bug, most of the time, we were able to automatically synthesize proof of concept programs (PoCs) that manifest the soundness bugs. Frequently these PoC programs contain more than a single instruction to force the verifier into a bad state, and can be nontrivial to write down manually. Our tool is open source. As a starting point, the PoCs generated by our tool for kernel versions 5.8 and 5.7-rc1 are available at [2], to help illustrate the deviations in the eBPF programs from the kernel verifier's analysis. Adding PoCs for other kernel versions is also doable given more time. The readme shows how to run the PoCs and trigger verifier bugs. The first example is the case of a PoC for a well-known CVE generated by our tool automatically and with fewer instructions compared to a well-known exploit. It is also possible to follow a longer sequence of steps to replicate our entire analysis starting from the kernel sources [3]. We look forward to hearing any feedback and comments for improvement. We intend to continue working on hardening different parts of the eBPF verifier. We also welcome suggestions on other parts of the verifier that the community thinks are particularly important to harden. Thanks, Harishankar Vishwanathan [1] Verifying the Verifier: eBPF Range Analysis Verification, by Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. Appearing at Computer Aided Verification (CAV) 2023. https://harishankarv.github.io/assets/files/agni-cav23.pdf [2] https://github.com/bpfverif/ebpf-verifier-bugs/blob/main/README.md [3] https://github.com/bpfverif/ebpf-range-analysis-verification-cav23/blob/main/README.md
