[bpf-next,00/15] Improvements for tracking scalars in the BPF verifier

Message

Maxim Mikityanskiy Dec. 20, 2023, 9:39 p.m. UTC

From: Maxim Mikityanskiy <[e-mail]>

The goal of this series is to extend the verifier's capabilities of
tracking scalars when they are spilled to stack, especially when the
spill or fill is narrowing. It also contains a fix by Eduard for
infinite loop detection and a state pruning optimization by Eduard that
compensates for a verification complexity regression introduced by
tracking unbounded scalars. These improvements reduce the surface of
false rejections that I saw while working on Cilium codebase.

Patch 1 (Maxim): Fix for an existing test, it will matter later in the
series.

Patches 2-3 (Eduard): Fixes for false rejections in infinite loop
detection that happen in the selftests when my patches are applied.

Patches 4-5 (Maxim): Fix the inconsistency of find_equal_scalars that
was possible if 32-bit spills were made.

Patches 6-11 (Maxim): Support the case when boundary checks are first
performed after the register was spilled to the stack.

Patches 12-13 (Maxim): Support narrowing fills.

Patches 14-15 (Eduard): Optimization for state pruning in stacksafe() to
mitigate the verification complexity regression.

veristat -e file,prog,states -f '!states_diff<50' -f '!states_pct<10' -f '!states_a<10' -f '!states_b<10' -C ...

 * Without patch 14:

File                  Program       States (A)  States (B)  States    (DIFF)
--------------------  ------------  ----------  ----------  ----------------
bpf_xdp.o             tail_lb_ipv6        3877        2936    -941 (-24.27%)
pyperf180.bpf.o       on_event            8422       10456   +2034 (+24.15%)
pyperf600.bpf.o       on_event           22259       37319  +15060 (+67.66%)
pyperf600_iter.bpf.o  on_event             400         540    +140 (+35.00%)
strobemeta.bpf.o      on_event            4702       13435  +8733 (+185.73%)

 * With patch 14:

File                  Program       States (A)  States (B)  States  (DIFF)
--------------------  ------------  ----------  ----------  --------------
bpf_xdp.o             tail_lb_ipv6        3877        2937  -940 (-24.25%)
pyperf600_iter.bpf.o  on_event             400         500  +100 (+25.00%)

Eduard Zingerman (4):
  bpf: make infinite loop detection in is_state_visited() exact
  selftests/bpf: check if imprecise stack spills confuse infinite loop
    detection
  bpf: Optimize state pruning for spilled scalars
  selftests/bpf: states pruning checks for scalar vs STACK_{MISC,ZERO}

Maxim Mikityanskiy (11):
  selftests/bpf: Fix the u64_offset_to_skb_data test
  bpf: Make bpf_for_each_spilled_reg consider narrow spills
  selftests/bpf: Add a test case for 32-bit spill tracking
  bpf: Add the assign_scalar_id_before_mov function
  bpf: Add the get_reg_width function
  bpf: Assign ID to scalars on spill
  selftests/bpf: Test assigning ID to scalars on spill
  bpf: Track spilled unbounded scalars
  selftests/bpf: Test tracking spilled unbounded scalars
  bpf: Preserve boundaries and track scalars on narrowing fill
  selftests/bpf: Add test cases for narrowing fill

 include/linux/bpf_verifier.h                  |   2 +-
 kernel/bpf/verifier.c                         | 160 +++++-
 .../bpf/progs/verifier_direct_packet_access.c |   2 +-
 .../selftests/bpf/progs/verifier_loops1.c     |  24 +
 .../selftests/bpf/progs/verifier_spill_fill.c | 529 +++++++++++++++++-
 .../testing/selftests/bpf/verifier/precise.c  |   6 +-
 6 files changed, 677 insertions(+), 46 deletions(-)