I’m Sanjit Bhat, a researcher at UT Austin. My advisor, Hovav Shacham, and I have been working on a tool to enable developers to automatically check the eBPF verifier’s range analysis routines for bugs, to generate sample bad inputs if bugs exist, and to formally prove that there are no range analysis bugs. We’re reaching out to get your feedback on whether there would be interest in using our tool. Some more details about what the tool does: We verify the range analysis routines in the eBPF verifier. These routines predict the output range of ALU operations on scalar registers. They include all code touched from the `adjust_scalar_min_max_vals` function in `verifier.c`, as well as the functions in `tnum.c`. In the past, these routines have led to a few CVE’s, e.g., CVE-2020-8835, CVE-2020-27194, and CVE-2021-3490. Our tool, written purely in Python, translates the C range analysis code to Z3 SMT solver inputs and verifies that the code implements a correct range analysis pass for all 32- and 64-bit ALU operations on scalar registers. Our tool already produces some interesting results, described below, but we’re still actively working on it. We would love your thoughts on ways we could make it more useful. Some preliminary results: We analyzed commit bc895e8b, which made a small change to the `signed_sub_overflows` function from 32-bit inputs to 64-bit inputs. Our tool found that before the commit, range analysis of 64-bit scalar-scalar subtraction was incorrect. The tool generated a BPF program that exploits the bug and leaves a register that has a concrete value outside the register’s tracked range. After applying the patch, the tool determined that 64-bit subtraction was now correct. In addition to this bug, we were able to re-find bugs exploited in prior zero-days, and we’ve done preliminary analysis on all verifier range analysis ops on a commit from back in May. Please let us know if this tool sounds interesting! We would be happy to explain it in more detail and collaborate on using it to aid eBPF verifier development.
