| Message ID | 20240127175237.526726-1-maxtram95@gmail.com (mailing list archive) |
|---|---|
| Headers | show |
| Series | Improvements for tracking scalars in the BPF verifier | expand |
Hello: This series was applied to bpf/bpf-next.git (master) by Andrii Nakryiko <andrii@kernel.org>: On Sat, 27 Jan 2024 19:52:31 +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,v3,1/6] bpf: Track spilled unbounded scalars https://git.kernel.org/bpf/bpf-next/c/e67ddd9b1cff - [bpf-next,v3,2/6] selftests/bpf: Test tracking spilled unbounded scalars https://git.kernel.org/bpf/bpf-next/c/6be503cec6c9 - [bpf-next,v3,3/6] bpf: Preserve boundaries and track scalars on narrowing fill https://git.kernel.org/bpf/bpf-next/c/c1e6148cb4f8 - [bpf-next,v3,4/6] selftests/bpf: Add test cases for narrowing fill https://git.kernel.org/bpf/bpf-next/c/067313a85c6f - [bpf-next,v3,5/6] bpf: handle scalar spill vs all MISC in stacksafe() https://git.kernel.org/bpf/bpf-next/c/6efbde200bf3 - [bpf-next,v3,6/6] selftests/bpf: states pruning checks for scalar vs STACK_MISC https://git.kernel.org/bpf/bpf-next/c/73a28d9d000e You are awesome, thank you!
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. Patches 1-9 of the original series were previously applied in v2. Patches 1-2 (Maxim): Support the case when boundary checks are first performed after the register was spilled to the stack. Patches 3-4 (Maxim): Support narrowing fills. Patches 5-6 (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 5: File Program States (A) States (B) States (DIFF) -------------------- -------- ---------- ---------- ---------------- pyperf100.bpf.o on_event 4878 6528 +1650 (+33.83%) pyperf180.bpf.o on_event 6936 11032 +4096 (+59.05%) pyperf600.bpf.o on_event 22271 39455 +17184 (+77.16%) pyperf600_iter.bpf.o on_event 400 490 +90 (+22.50%) strobemeta.bpf.o on_event 4895 14028 +9133 (+186.58%) * With patch 5: File Program States (A) States (B) States (DIFF) ----------------------- ------------- ---------- ---------- --------------- bpf_xdp.o tail_lb_ipv4 2770 2224 -546 (-19.71%) pyperf100.bpf.o on_event 4878 5848 +970 (+19.89%) pyperf180.bpf.o on_event 6936 8868 +1932 (+27.85%) pyperf600.bpf.o on_event 22271 29656 +7385 (+33.16%) pyperf600_iter.bpf.o on_event 400 450 +50 (+12.50%) xdp_synproxy_kern.bpf.o syncookie_tc 280 226 -54 (-19.29%) xdp_synproxy_kern.bpf.o syncookie_xdp 302 228 -74 (-24.50%) v2 changes: Fixed comments in patch 1, moved endianness checks to header files in patch 12 where possible, added Eduard's ACKs. v3 changes: Maxim: Removed __is_scalar_unbounded altogether, addressed Andrii's comments. Eduard: Patch #5 (#14 in v2) changed significantly: - Logical changes: - Handling of STACK_{MISC,ZERO} mix turned out to be incorrect: a mix of MISC and ZERO in old state is not equivalent to e.g. just MISC is current state, because verifier could have deduced zero scalars from ZERO slots in old state for some loads. - There is no reason to limit the change only to cases when old or current stack is a spill of unbounded scalar, it is valid to compare any 64-bit scalar spill with fake register impersonating MISC. - STACK_ZERO vs spilled zero case was dropped, after recent changes for zero handling by Andrii and Yonghong it is hard (impossible?) to conjure all ZERO slots for an spi. => the case does not make any difference in veristat results. - Use global static variable for unbound_reg (Andrii) - Code shuffling to remove duplication in stacksafe() (Andrii) Eduard Zingerman (2): bpf: handle scalar spill vs all MISC in stacksafe() selftests/bpf: states pruning checks for scalar vs STACK_MISC Maxim Mikityanskiy (4): 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 | 9 + kernel/bpf/verifier.c | 103 ++++-- .../selftests/bpf/progs/verifier_spill_fill.c | 324 +++++++++++++++++- 3 files changed, 404 insertions(+), 32 deletions(-)