Re: [BUG] verifier escape with iteration helpers (bpf_loop, ...)

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2023-09-21 at 19:48 -0700, Andrii Nakryiko wrote:
> Yes, my gut feeling was that if this idea works at all, then ordering
> for this won't matter. The question is if the idea itself is sound.
> Basically, I need to convince myself that subsequent iterations won't
> add any new read/precise marks. You are good at counter examples, so
> maybe you can come up with an example where input state into iteration
> #1 will get more precision marks only at iteration #2 or deeper. If
> that's the case, then this whole idea of postponing loop convergence
> checks probably doesn't work.

Consider the following code:

    1.  SEC("fentry/" SYS_PREFIX "sys_nanosleep")
    2.  int num_iter_bug(const void *ctx) {
    3.      struct bpf_iter_num it;
    4.      __u64 val = 0;
    5.      __u64 *ptr = &val;
    6.      __u64 rnd = bpf_get_current_pid_tgid();
    7.
    8.      bpf_iter_num_new(&it, 0, 10);
    9.      while (bpf_iter_num_next(&it)) {
    10.          rnd++;
    11.          if (rnd == 42) {
    12.              ptr = (void*)(0xdead);
    13.              continue;
    14.          }
    15.          if (!bpf_iter_num_next(&it))
    16.              break;
    17.          bpf_probe_read_user(ptr, 8, (void*)(0xdeadbeef));
    18.      }
    19.      bpf_iter_num_destroy(&it);
    20.      return 0;
    21. }

As far as I understand the following verification paths would be
explored (ignoring traces with drained iterators):
- entry:
  - 8,9,10,11,12,13:
    - at 9 checkpoint (C1) would be created with it{.depth=0,.state=active},ptr=&val;
    - at 11 branch (B1) would be created with it{.depth=0,.state=active},ptr=&val;
    - jump from 13 to 9 would be postponed with state
      it{.depth=0,.state=active},ptr=0xdead as proceeding would increase 'it' depth;
- jump from 11 to 15 (branch B1):
  - 15:
    - checkpoint would be created with it{.depth=0,.state=active};
    - jump from 15 to 17 would be postponed with state
      it{.depth=0,.state=active} as proceeding would increase 'it' depth.
- at this point verifier would run out of paths that don't increase
  iterators depth and there are two choices:
  - (a) jump from 13 to 9 with state it{.depth=0,.state=active},ptr=0xdead;
  - (b) jump from 15 to 17 with state it{.depth=0,.state=active},ptr=&val.
  If (a) would be processed first there would be no read mark for
  'ptr' in C1 yet and verifier runs into to the same issue as with
  original example.

Do I miss something or is it a legit counter-example?

> I can't say I understand what exactly you are proposing and how you
> are going to determine these conservative precision marks. But I'd
> like to learn some new ideas, so please elaborate :)

I'll send a follow-up email, trying to figure out what to do with pointers.