[bpf-next] bpf, verifier: Automated formal verification tool for finding bugs in eBPF verifier range analysis routines

[bpf-next] bpf, verifier: Automated formal verification tool for finding bugs in eBPF verifier range analysis routines

[Sanjit Bhat]

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.

Re: [bpf-next] bpf, verifier: Automated formal verification tool for finding bugs in eBPF verifier range analysis routines

[Alexei Starovoitov]

On Mon, Oct 11, 2021 at 9:19 AM Sanjit Bhat <sanjit.bhat@gmail.com> 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!