On Fri, Sep 22, 2023 at 11:36 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> 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 think it is, yes. With the use of
if (!bpf_iter_num_next(&it))
break;
you can postpone any important markings as deep into iteration
verification as necessary. So yeah, the idea to explore code path
level by level won't cover all the cases, unfortunately.
> > 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.
Ok, sounds good.
