mbox series

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

Message ID 20240108205209.838365-1-maxtram95@gmail.com
Headers show
Series Improvements for tracking scalars in the BPF verifier | expand

Message

Maxim Mikityanskiy Jan. 8, 2024, 8:51 p.m. UTC
From: Maxim Mikityanskiy <maxim@isovalent.com>

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%)

v2 changes:

Fixed comments in patch 1, moved endianness checks to header files in
patch 12 where possible, added Eduard's ACKs.

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                  |   4 +-
 include/linux/filter.h                        |  12 +
 kernel/bpf/verifier.c                         | 155 ++++-
 .../bpf/progs/verifier_direct_packet_access.c |   2 +-
 .../selftests/bpf/progs/verifier_loops1.c     |  24 +
 .../selftests/bpf/progs/verifier_spill_fill.c | 533 +++++++++++++++++-
 .../testing/selftests/bpf/verifier/precise.c  |   6 +-
 7 files changed, 685 insertions(+), 51 deletions(-)

Comments

patchwork-bot+netdevbpf@kernel.org Jan. 12, 2024, 3 a.m. UTC | #1
Hello:

This series was applied to bpf/bpf-next.git (master)
by Alexei Starovoitov <ast@kernel.org>:

On Mon,  8 Jan 2024 22:51:54 +0200 you wrote:
> From: Maxim Mikityanskiy <maxim@isovalent.com>
> 
> 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.
> 
> [...]

Here is the summary with links:
  - [bpf-next,v2,01/15] selftests/bpf: Fix the u64_offset_to_skb_data test
    https://git.kernel.org/bpf/bpf-next/c/02fb00d34de1
  - [bpf-next,v2,02/15] bpf: make infinite loop detection in is_state_visited() exact
    https://git.kernel.org/bpf/bpf-next/c/3a96c705f48a
  - [bpf-next,v2,03/15] selftests/bpf: check if imprecise stack spills confuse infinite loop detection
    https://git.kernel.org/bpf/bpf-next/c/723909ae6496
  - [bpf-next,v2,04/15] bpf: Make bpf_for_each_spilled_reg consider narrow spills
    https://git.kernel.org/bpf/bpf-next/c/0e00a9551c61
  - [bpf-next,v2,05/15] selftests/bpf: Add a test case for 32-bit spill tracking
    https://git.kernel.org/bpf/bpf-next/c/221dffec93e8
  - [bpf-next,v2,06/15] bpf: Add the assign_scalar_id_before_mov function
    https://git.kernel.org/bpf/bpf-next/c/85b6e9d75c8e
  - [bpf-next,v2,07/15] bpf: Add the get_reg_width function
    https://git.kernel.org/bpf/bpf-next/c/b08973e4d9c4
  - [bpf-next,v2,08/15] bpf: Assign ID to scalars on spill
    https://git.kernel.org/bpf/bpf-next/c/26b560765e67
  - [bpf-next,v2,09/15] selftests/bpf: Test assigning ID to scalars on spill
    https://git.kernel.org/bpf/bpf-next/c/5a052eb509e9
  - [bpf-next,v2,10/15] bpf: Track spilled unbounded scalars
    https://git.kernel.org/bpf/bpf-next/c/53ac20c9e0dd
  - [bpf-next,v2,11/15] selftests/bpf: Test tracking spilled unbounded scalars
    https://git.kernel.org/bpf/bpf-next/c/9ba80a06cabb
  - [bpf-next,v2,12/15] bpf: Preserve boundaries and track scalars on narrowing fill
    (no matching commit)
  - [bpf-next,v2,13/15] selftests/bpf: Add test cases for narrowing fill
    (no matching commit)
  - [bpf-next,v2,14/15] bpf: Optimize state pruning for spilled scalars
    (no matching commit)
  - [bpf-next,v2,15/15] selftests/bpf: states pruning checks for scalar vs STACK_{MISC,ZERO}
    (no matching commit)

You are awesome, thank you!