On Thu, 2023-09-21 at 02:14 -0700, Alexei Starovoitov wrote:
> On Tue, Sep 19, 2023 at 5:19 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
> >
> > > >
> > > > Note that R7=fp-16 in old state vs R7_w=57005 in cur state.
> > > > The registers are considered equal because R7 does not have a read mark.
> > > > However read marks are not yet finalized for old state because
> > > > sl->state.branches != 0.
>
> By "liveness marks are not finalized" you mean that
> regs don't have LIVE_DONE?
> That shouldn't matter to state comparison.
> It only needs to see LIVE_READ.
> LIVE_DONE is a sanity check for liveness algorithm only.
> It doesn't affect correctness.
No, actually I mean that the state where R7 is read had not been seen
yet and thus read mark had not been propagated to the parent state.
See below.
> > > > (Note: precision marks are not finalized as
> > > > well, which should be a problem, but this requires another example).
> > >
> > > I originally convinced myself that non-finalized precision marking is
> > > fine, see the comment next to process_iter_next_call() for reasoning.
> > > If you can have a dedicated example for precision that would be great.
> > >
> > > As for read marks... Yep, that's a bummer. That r7 is not used after
> > > the loop, so is not marked as read, and it's basically ignored for
> > > loop invariant checking, which is definitely not what was intended.
> >
> > Liveness is a precondition for all subsequent checks, so example
> > involving precision would also involve liveness. Here is a combined
> > example:
> >
> > r8 = 0
> > fp[-16] = 0
> > r7 = -16
> > r6 = bpf_get_current_pid_tgid()
> > bpf_iter_num_new(&fp[-8], 0, 10)
> > while (bpf_iter_num_next(&fp[-8])) {
> > r6++
> > if (r6 != 42) {
> > r7 = -32
> > continue;
> > }
> > r0 = r10
> > r0 += r7
> > r8 = *(u64 *)(r0 + 0)
> > }
> > bpf_iter_num_destroy(&fp[-8])
> > return r8
> >
> > (Complete source code is at the end of the email).
> >
> > The call to bpf_iter_num_next() is reachable with r7 values -16 and -32.
> > State with r7=-16 is visited first, at which point r7 has no read mark
> > and is not marked precise.
> > State with r7=-32 is visited second:
> > - states_equal() for is_iter_next_insn() should ignore absence of
> > REG_LIVE_READ mark on r7, otherwise both states would be considered
> > identical;
>
> I think assuming live_read on all regs in regsafe() when
> cb or iter body is being processed will have big impact
> on processed insns.
> I suspect the underlying issue is different.
>
> In the first pass of the body with r7=-16 the 'r0 += r7'
> insn should have added the read mark to r7,
> so is_iter_next_insn after 2nd pass with r7=-32 should reach
> case SCALAR_VALUE in regsafe().
> There we need to do something with lack of precision in r7=-16,
> but assume that is fixed, the 3rd iter of the loop should continue
> and 'r0 += r7' in the _3rd_ iter of the loop should propagate
> read mark all the way to r7=-32 reg.
I repeat the complete example with added instruction numbers in the
end of the email. As of now verifier takes the following paths:
First:
// First path is for "drained" iterator and is not very interesting.
0: (b7) r8 = 0 ; R8_w=0
...
2: (b7) r7 = -16 ; R7_w=-16
...
4: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1)
...
12: (85) call bpf_iter_num_next#63182
; R0_w=0 fp-8=iter_num(ref_id=2,state=drained,depth=0) refs=2
13: (15) if r0 == 0x0 goto pc+8
22: (bf) r1 = r10
...
26: (95) exit
Second:
// Note: at 13 a first checkpoint with "active" iterator state is reached
// this checkpoint is created for R7=-16 w/o read mark.
from 12 to 13: R0_w=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) R6=scalar(id=1)
R7=-16 R8=0 R10=fp0 fp-8=iter_num(ref_id=2,state=active,depth=1)
fp-16=00000000 refs=2
13: (15) if r0 == 0x0 goto pc+8 ; R0_w=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) refs=2
14: (07) r6 += 1 ; R6=scalar() refs=2
15: (55) if r6 != 0x2a goto pc+2 ; R6=42 refs=2
16: (b7) r7 = -32 ; R7_w=-32 refs=2
17: (05) goto pc-8
10: (bf) r1 = r10 ; R1_w=fp0 R10=fp0 refs=2
11: (07) r1 += -8
is_iter_next (12):
old:
R0=scalar() R1_rw=fp-8 R6_r=scalar(id=1) R7=-16 R8_r=0 R10=fp0
fp-8_r=iter_num(ref_id=2,state=active,depth=0) fp-16=00000000 refs=2
cur:
R0=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) R1_w=fp-8 R6=42 R7_w=-32
R8=0 R10=fp0 fp-8=iter_num(ref_id=2,state=active,depth=1) fp-16=00000000 refs=2
> hit
12: safe
// At this point R7=-32 but it still lacks read or precision marks,
// thus states_equal() called from is_state_visited() for is_iter_next_insn()
// branch returns true. (I added some logging to make it clear above)
Third:
// This is r6 != 42 branch, it hits same checkpoint as "second" path.
// Note that this branch has "r0 += r7" and will propagate read mark
// for R7 to the "old" checkpoint but that's too late, R7=-32 state
// has already been pruned.
from 15 to 18: R0=rdonly_mem(id=3,ref_obj_id=2,off=0,imm=0) R6=scalar()
R7=-16 R8=0 R10=fp0 fp-8=iter_num(ref_id=2,state=active,depth=1)
fp-16=00000000 refs=2
18: (bf) r0 = r10 ; R0_w=fp0 R10=fp0 refs=2
19: (0f) r0 += r7
20: (79) r8 = *(u64 *)(r0 +0) ; R0_w=fp-16 R8_w=P0 fp-16=00000000 refs=2
21: (05) goto pc-12
10: (bf) r1 = r10 ; R1_w=fp0 R10=fp0 refs=2
11: (07) r1 += -8
is_iter_next (12):
old:
R0=scalar() R1_rw=fp-8 R6_r=scalar(id=1) R7_r=P-16 R8_r=0 R10=fp0
fp-8_r=iter_num(ref_id=2,state=active,depth=0) fp-16_r=00000000 refs=2
cur:
R0_w=fp-16 R1_w=fp-8 R6=scalar() R7=-16 R8_w=P0 R10=fp0
fp-8=iter_num(ref_id=2,state=active,depth=1) fp-16=00000000 refs=2
> hit
12: safe
Here on the second path the state with R7=-32 is pruned and this is
not safe. Registers that differ in this state are R6 and R7. I can
update the example so that there would be no difference in R6, so
let's ignore that for now. As for R7, in the "old" state it is not
marked read because children states of "old" that read R7 had not been
visited yet.
> I mean the parentage chain between regs should link
> regs of iterations.
> I believe the process_iter_next_call() logic maintains
> correct parentage chain, since it's just a push_stack()
> and is_state_visited() should be connecting parents.
> So in case of iter body the issue with above loop is only
> in missing precision,
> but for your cb verification code I suspect the issue is due
> to lack of parentage chain and liveness is not propagated ?
Right, parentage chain is preserved by both process_iter_next_call()
and cb processing code as both use push_stack().
> I could be completely off the mark.
> The discussion is hard to follow.
> It's probably time to post raw patch and continue with code.
The "fix" that I have locally is not really a fix. It forces "exact"
states comparisons for is_iter_next_insn() case:
1. liveness marks are ignored;
2. precision marks are ignored;
3. scalars are compared using regs_exact().
It breaks a number a number of tests, because iterator "entry" states
are no longer equal and upper iteration bound is not tracked:
- iters/simplest_loop
- iters/iter_obfuscate_counter
- iters/testmod_seq_truncated
- iters/num
- iters/testmod_seq
- linked_list/pop_front_off
- linked_list/pop_back_off
The log above shows that (1) and (2) are inevitable.
(But might be relaxed if some data flow analysis which marks
registers that *might* be precise or read is done before
main verification path).
For (3), I'm not sure and need to think a bit more but "range_within"
logic seems fishy for states with .branches > 0.
--- complete example with insn numbers ---
SEC("fentry/" SYS_PREFIX "sys_nanosleep")
__failure
__msg("20: (79) r8 = *(u64 *)(r0 +0)")
__msg("invalid read from stack R0 off=-32 size=8")
__naked int iter_next_exact(void)
{
/* r8 = 0
* fp[-16] = 0
* r7 = -16
* r6 = bpf_get_current_pid_tgid()
* bpf_iter_num_new(&fp[-8], 0, 10)
* while (bpf_iter_num_next(&fp[-8])) {
* r6++
* if (r6 == 42) {
* r7 = -32
* continue;
* }
* r0 = r10
* r0 += r7
* r8 = *(u64 *)(r0 + 0)
* }
* bpf_iter_num_destroy(&fp[-8])
* return r8
*/
asm volatile (
"r8 = 0;" // 0
"*(u64 *)(r10 - 16) = r8;" // 1
"r7 = -16;" // 2
"call %[bpf_get_current_pid_tgid];" // 3
"r6 = r0;" // 4
"r1 = r10;" // 5
"r1 += -8;" // 6
"r2 = 0;" // 7
"r3 = 10;" // 8
"call %[bpf_iter_num_new];" // 9
"1:"
"r1 = r10;" // 10
"r1 += -8;\n" // 11
"call %[bpf_iter_num_next];" // 12
"if r0 == 0 goto 2f;" // 13
"r6 += 1;" // 14
"if r6 != 42 goto 3f;" // 15
"r7 = -32;" // 16
"goto 1b;\n" // 17
"3:"
"r0 = r10;" // 18
"r0 += r7;" // 19
"r8 = *(u64 *)(r0 + 0);" // 20
"goto 1b;\n" // 21
"2:"
"r1 = r10;" // 22
"r1 += -8;" // 23
"call %[bpf_iter_num_destroy];" // 24
"r0 = r8;" // 25
"exit;" // 26
:
: __imm(bpf_get_current_pid_tgid),
__imm(bpf_iter_num_new),
__imm(bpf_iter_num_next),
__imm(bpf_iter_num_destroy),
__imm(bpf_probe_read_user)
: __clobber_all
);
}
