Re: [PATCH bpf-next v1 1/2] bpf: states with loop entry have incomplete read/precision marks

[Eduard Zingerman <eddyz87@gmail.com>]

On Tue, 2025-03-11 at 20:13 -0700, Eduard Zingerman wrote:
> Suppose the verifier state exploration graph looks as follows:
> 
>     .-> A --.    Suppose:
>     |   |   |    - state A is at iterator 'next';
>     |   v   v    - path A -> B -> A is verified first;
>     '-- B   C    - path A -> C is verified next;
>                  - B does not impose a read mark for register R1;
>                  - C imposes a read mark for register R1;
> 
> Under such conditions:
> - when B is explored and A is identified as its loop entry, the read
>   marks are copied from A to B by propagate_liveness(), but these
>   marks do not include R1;
> - when C is explored, the read mark for R1 is propagated to A,
>   but not to B.
> - at this point, state A has its branch count at zero, but state
>   B has incomplete read marks.
> 
> The same logic applies to precision marks.
> This means that states with a loop entry can have incomplete read and
> precision marks, regardless of whether the loop entry itself has
> branches.

Which makes me wonder.
If read/precision marks for B are not final and some state D outside
of the loop becomes equal to B, the read/precision marks for that
state would be incomplete as well:

        D------.  // as some read/precision marks are missing from C
               |  // propagate_liveness() won't copy all necessary
    .-> A --.  |  // marks to D.
    |   |   |  |
    |   v   v  |
    '-- B   C  |
        ^      |
        '------'

This makes comparison with 'loop_entry' states contagious,
propagating incomplete read/precision mark flag up to the root state.
This will have verification performance implications.

Alternatively read/precision marks need to be propagated in the state
graph until fixed point is reached. Like with DFA analysis.

Решето.

> The current verification logic does not account for this. An example
> of an unsafe program accepted by the verifier is the selftest included
> in the next patch.

[...]