[PATCH v2 bpf 0/4] Fix invariant violation for single-value tnums

[Paul Chaignon <paul.chaignon@gmail.com>]

We're hitting an invariant violation in Cilium that sometimes leads to
BPF programs being rejected and Cilium failing to start [1]. As far as
I know this is the first case of invariant violation found in a real
program (i.e., not by a fuzzer). The following extract from verifier
logs shows what's happening:

  from 201 to 236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
  236: R1=0 R6=ctx() R7=1 R9=scalar(smin=umin=smin32=umin32=3584,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100)) R10=fp0
  ; if (magic == MARK_MAGIC_HOST || magic == MARK_MAGIC_OVERLAY || magic == MARK_MAGIC_ENCRYPT) @ bpf_host.c:1337
  236: (16) if w9 == 0xe00 goto pc+45   ; R9=scalar(smin=umin=smin32=umin32=3585,smax=umax=smax32=umax32=3840,var_off=(0xe00; 0x100))
  237: (16) if w9 == 0xf00 goto pc+1
  verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0xe01, 0xe00] s64=[0xe01, 0xe00] u32=[0xe01, 0xe00] s32=[0xe01, 0xe00] var_off=(0xe00, 0x0)

More details are given in the second patch, but in short, the verifier
should be able to detect that the false branch of instruction 237 is
never true. After instruction 236, the u64 range and the tnum overlap
in a single value, 0xf00.

The long-term solution to invariant violation is likely to rely on the
refinement + invariant violation check to detect dead branches, as
started by Eduard. To fix the current issue, we need something with
less refactoring that we can backport to affected kernels.

The solution implemented in the second patch is to improve the bounds
refinement to avoid this case. It relies on a new tnum helper,
tnum_step, first sent as an RFC in [2]. The last two patches extend and
update the selftests.

Link: https://github.com/cilium/cilium/issues/44216 [1]
Link: https://lore.kernel.org/bpf/20251107192328.2190680-2-harishankar.vishwanathan@gmail.com/ [2]

Changes in v2:
  - Add guard suggested by Hari in tnum_step, to avoid undefined
    behavior spotted by AI code review.
  - Add explanation diagrams in code as suggested by Eduard.
  - Rework conditions for readability as suggested by Eduard.
  - Updated reference to SMT formula.
  - Rebased.

Harishankar Vishwanathan (1):
  bpf: Introduce tnum_step to step through tnum's members

Paul Chaignon (3):
  bpf: Improve bounds when tnum has a single possible value
  selftests/bpf: Test refinement of single-value tnum
  selftests/bpf: Avoid simplification of crafted bounds test

 include/linux/tnum.h                          |  3 +
 kernel/bpf/tnum.c                             | 56 ++++++++++++
 kernel/bpf/verifier.c                         | 30 ++++++
 .../selftests/bpf/prog_tests/reg_bounds.c     |  2 +-
 .../selftests/bpf/progs/verifier_bounds.c     | 91 +++++++++++++++++++
 5 files changed, 181 insertions(+), 1 deletion(-)

-- 
2.43.0