On Mon, Oct 11, 2021 at 9:19 AM Sanjit Bhat <sanjit.bhat@xxxxxxxxx> wrote: > > 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. It certainly sounds interesting! Keep us posted on the progress. Do you plan to do forward analysis and find bugs proactively? It sounds like the tool can only analyze the past commits? Could you contribute the auto-generated progs as selftests? Thanks!
