[bpf-next,v2,0/5] bpf/verifier: range computation improvements

Message

Cupertino Miranda April 17, 2024, 12:23 p.m. UTC

Hi everyone,

This is the second series of this patches, now changed after Yonghong
review. Thank you for the review.

Changes from v1:
 - Reordered patches in the series.
 - Fix refactor to be acurate with original code.
 - Fixed other mentioned small problems.


This patch series is a follow up on the problem identified in
https://github.com/systemd/systemd/issues/31888.
This problem first shown as a result of a GCC compilation for BPF that
ends converting a condition based decision tree, into a logic based one
(making use of XOR), in order to compute expected return value for the
function.

This issue was also reported in
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both
the original reproducer pattern and some other that also fails within
clang.

This is the result of an earlier test that allows to describe the
problem better:

  VERIFIER LOG:
  =============
  Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported.
  0: R1=ctx() R10=fp0
  ; asm volatile ("                                       \ @ verifier_bounds.c:755
  0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
  1: (bf) r6 = r0                       ; R0_w=scalar(id=1) R6_w=scalar(id=1)
  2: (b7) r1 = 0                        ; R1_w=0
  3: (7b) *(u64 *)(r10 -8) = r1         ; R1_w=0 R10=fp0 fp-8_w=0
  4: (bf) r2 = r10                      ; R2_w=fp0 R10=fp0
  5: (07) r2 += -8                      ; R2_w=fp-8
  6: (18) r1 = 0xffff8e8ec3b99000       ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8)
  8: (85) call bpf_map_lookup_elem#1    ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8)
  9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm
  11: (b4) w1 = 0                       ; R1_w=0
  12: (77) r6 >>= 63                    ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
  13: (ac) w1 ^= w6                     ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
  14: (16) if w1 == 0x0 goto pc+2       ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1)
  15: (16) if w1 == 0x1 goto pc+1       ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2)
  16: (79) r0 = *(u64 *)(r0 +8)
  invalid access to map value, value_size=8 off=8 size=8
  R0 min value is outside of the allowed memory range
  processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1
  =============

The test collects a random number and shifts it right by 63 bits to reduce its
range to (0,1), which will then xor to compute the value of w1, checking
if the value is either 0 or 1 after.
By analysing the code and the ranges computations, one can easily deduce
that the result of the XOR is also within the range (0,1), however:

  11: (b4) w1 = 0                       ; R1_w=0
  12: (77) r6 >>= 63                    ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
  13: (ac) w1 ^= w6                     ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
                                            ^
                                            |___ No range is computed for R1

The verifier seems to act pessimistically and will only compute a range
for dst_reg, if the src_reg is a known value.
This happens in:

  -- verifier.c:13700 --
  if (!src_known &&
      opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) {
          __mark_reg_unknown(env, dst_reg);
          return 0;
  }

This patch series addresses the problem and improves the support for
range computation for XOR and OR.
Apart from XOR and OR the patch series also improves the range
computation for MUL for the case where either of its operands is a known
value.

Looking forward to your comments.

Regards,
Cupertino

Cupertino Miranda (5):
  bpf/verifier: refactor checks for range computation
  bpf/verifier: improve XOR and OR range computation
  selftests/bpf: XOR and OR range computation tests.
  bpf/verifier: relax MUL range computation check
  selftests/bpf: MUL range computation tests.

 kernel/bpf/verifier.c                         | 160 ++++++++++-------
 .../selftests/bpf/progs/verifier_bounds.c     | 163 ++++++++++++++++++
 2 files changed, 260 insertions(+), 63 deletions(-)