Re: [PATCH v3 bpf-next 0/2] bpf: properly verify tail call behavior

[Eduard Zingerman <eddyz87@gmail.com>]

On Wed, 2025-11-05 at 18:40 +0100, Martin Teichmann wrote:
> I added the changes you proposed.
> 
> regarding bpf_insn_successors(), nothing needs to be done, call
> already have the next instruction as successor by default, and this
> is all we need. The fact that a tail call can also be an exit in
> disguise is handled by calling bpf_update_live_stack().

Consider the following scenario:

main:
  int a;
  int b[10] = { 1, 2, ... };
  if <random>:
    a = 100500;
  foo(&a);
  return b[a];

foo(int *a):
  tail call;
  *a = 0;
  return;

W/o bpf_insn_successors() knowing that tail call can jump directly to
return, verifier will assume that write to *a always happens, and
accept the above program.

While trying to create a reproducer for the above scenario I found an
issue with current patch-set and precision tracking.
Consider a modifier version of you test case:

  SEC("socket")
  __log_level(2)
  __flag(BPF_F_TEST_STATE_FREQ)
  __naked unsigned long caller_stack_write_tail_call(void)
  {
        asm volatile (
        "r6 = r1;"
        "*(u64 *)(r10 - 8) = -8;"
        "call %[bpf_get_prandom_u32];"
        "if r0 != 42 goto 1f;"
        "goto 2f;"
  "1:"
        "*(u64 *)(r10 - 8) = -1024;"
  "2:"
        "r1 = r6;"
        "r2 = r10;"
        "r2 += -8;"
        "call write_tail_call;"
        "r1 = *(u64 *)(r10 - 8);"
        "r2 = r10;"
        "r2 += r1;"
        "r0 = *(u64 *)(r2 + 0);"
        "exit;"
        :: __imm(bpf_get_prandom_u32)
        : __clobber_all);
  }

  static __used __naked unsigned long write_tail_call(void)
  {
        asm volatile (
        "r6 = r2;"
        "r2 = %[map_array] ll;"
        "r3 = 0;"
        "call %[bpf_tail_call];"
        "*(u64 *)(r6 + 0) = -16;"
        "r0 = 0;"
        "exit;"
        :
        : __imm(bpf_tail_call),
          __imm_addr(map_array)
        : __clobber_all);
  }

Currently, it hits the following error:

  10: (79) r1 = *(u64 *)(r10 -8)        ; R1=-8 R10=fp0 fp-8=-8
  11: (bf) r2 = r10                     ; R2=fp0 R10=fp0
  12: (0f) r2 += r1
  mark_precise: frame0: last_idx 12 first_idx 10 subseq_idx -1 
  mark_precise: frame0: regs=r1 stack= before 11: (bf) r2 = r10
  mark_precise: frame0: regs=r1 stack= before 10: (79) r1 = *(u64 *)(r10 -8)
  mark_precise: frame0: parent state regs= stack=-8:  R0=scalar() R6=ctx() R10=fp0 fp-8=P-8
  mark_precise: frame0: last_idx 19 first_idx 15 subseq_idx 10 
  mark_precise: frame0: regs= stack=-8 before 19: (85) call bpf_tail_call#12
  mark_precise: frame0: regs= stack=-8 before 18: (b7) r3 = 0
  mark_precise: frame0: regs= stack=-8 before 16: (18) r2 = 0xff11000109035000
  mark_precise: frame0: regs= stack=-8 before 15: (bf) r6 = r2
  mark_precise: frame0: parent state regs= stack=-8:  R6=ctx() R10=fp0 fp-8=P-8
  mark_precise: frame0: last_idx 9 first_idx 9 subseq_idx 15 
  mark_precise: frame0: regs= stack=-8 before 9: (85) call pc+5
  verifier bug: static subprog leftover stack slots 1
  processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 5 peak_states 5 mark_read 0
  =============

This happens, because __mark_chain_precision() moves from a history
entry with frame index 0, to a history entry with frame index 1.
backtrack_insn() assumes that such changes are impossible, because
there always would be an EXIT instruction for a subprogram, where it
would adjust bt->frame by +1. Which is not the case with patch-set.

So, one needs to track frame index in struct bpf_jmp_history_entry,
or fake a jump from tail call to EXIT, instead of directly leaving
subprogram.

After that is resolved, I think that bpf_insn_successors() issue
described above will manifest itself.

> In total, this patch now fixed three bugs: a regression wheras
> programs that modify packet data after a tail call are unnecessarily
> rejected, proper treatment of precision propagation and live stack
> tracking.
> 
> Martin Teichmann (2):
>   bpf: properly verify tail call behavior
>   bpf: test the proper verification of tail calls
> 
>  kernel/bpf/verifier.c                         | 26 ++++++++--
>  .../selftests/bpf/progs/verifier_live_stack.c | 46 ++++++++++++++++++
>  .../selftests/bpf/progs/verifier_sock.c       | 39 ++++++++++++++-
>  .../bpf/progs/verifier_subprog_precision.c    | 47 +++++++++++++++++++
>  4 files changed, 153 insertions(+), 5 deletions(-)