On Thu, 2023-06-01 at 10:13 -0700, Alexei Starovoitov wrote:
> On Thu, Jun 1, 2023 at 9:57 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
> >
> > On Wed, 2023-05-31 at 19:05 -0700, Alexei Starovoitov wrote:
> > > [...]
> > > > Suppose that current verification path is 1-7:
> > > > - On a way down 1-6 r7 will not be marked as precise, because
> > > > condition (r7 > X) is not predictable (see check_cond_jmp_op());
> > > > - When (7) is reached mark_chain_precision() will start moving up
> > > > marking the following registers as precise:
> > > >
> > > > 4: if (r6 > r7) goto +1 ; r6, r7
> > > > 5: r7 = r6 ; r6
> > > > 6: if (r7 > X) goto ... ; r6
> > > > 7: r9 += r6 ; r6
> > > >
> > > > - Thus, if checkpoint is created for (6) r7 would be marked as read,
> > > > but will not be marked as precise.
> > > >
> > > > Next, suppose that jump from 4 to 6 is verified and checkpoint for (6)
> > > > is considered:
> > > > - r6 is not precise, so check_ids() is not called for it and it is not
> > > > added to idmap;
> > > > - r7 is precise, so check_ids() is called for it, but it is a sole
> > > > register in the idmap;
> > >
> > > typos in above?
> > > r6 is precise and r7 is not precise.
> >
> > Yes, it should be the other way around in the description:
> > r6 precise, r7 not precise. Sorry for confusion.
> >
> > > > - States are considered equal.
> > > >
> > > > Here is the log (I added a few prints for states cache comparison):
> > > >
> > > > from 10 to 13: safe
> > > > steq hit 10, cur:
> > > > R0=scalar(id=2) R6=scalar(id=2) R7=scalar(id=1) R9=fp-8 R10=fp0 fp-8=00000000
> > > > steq hit 10, old:
> > > > R6_rD=Pscalar(id=2) R7_rwD=scalar(id=2) R9_rD=fp-8 R10=fp0 fp-8_rD=00000000
> > >
> > > the log is correct, thouhg.
> > > r6_old = Pscalar which will go through check_ids() successfully and both are unbounded.
> > > r7_old is not precise. different id-s don't matter and different ranges don't matter.
> > >
> > > As another potential fix...
> > > can we mark_chain_precision() right at the time of R1 = R2 when we do
> > > src_reg->id = ++env->id_gen
> > > and copy_register_state();
> > > for both regs?
> >
> > This won't help, e.g. for the original example precise markings would be:
> >
> > 4: if (r6 > r7) goto +1 ; r6, r7
> > 5: r7 = r6 ; r6, r7
> > 6: if (r7 > X) goto ... ; r6 <-- mark for r7 is still missing
> > 7: r9 += r6 ; r6
>
> Because 6 is a new state and we do mark_all_scalars_imprecise() after 5 ?
Yes, precision marks are not inherited by child states.
>
> > What might help is to call mark_chain_precision() from
> > find_equal_scalars(), but I expect this to be very expensive.
>
> maybe worth giving it a shot?
Sure, will report a bit later today.
> > > I think
> > > if (rold->precise && !check_ids(rold->id, rcur->id, idmap))
> > > would be good property to have.
> > > I don't like u32_hashset either.
> > > It's more or less saying that scalar id-s are incompatible with precision.
> > >
> > > I hope we don't need to do:
> > > + u32 reg_ids[MAX_CALL_FRAMES];
> > > for backtracking either.
> > > Hacking id-s into jmp history is equally bad.
> > >
> > > Let's figure out a minimal fix.
> >
> > Solution discussed with Andrii yesterday seems to work.
>
> The thread is long. Could you please describe it again in pseudo code?
- Add a function mark_precise_scalar_ids(struct bpf_verifier_env *env,
struct bpf_verifier_state *st)
such that it:
- collect PRECISE_IDS: a set of IDs of all registers marked in env->bt
- visit all registers with ids from PRECISE_IDS and make sure
that these registers are marked in env->bt
- Call mark_precise_scalar_ids() from __mark_chain_precision()
for each state 'st' visited by states chain processing loop,
so that:
- mark_precise_scalar_ids() is called for current state when
__mark_chain_precision() is entered, reusing id assignments in
current state;
- mark_precise_scalar_ids() is called for each parent state, reusing
id assignments valid at 'last_idx' instruction of that state.
The idea is that in situations like below:
4: if (r6 > r7) goto +1
5: r7 = r6
--- checkpoint #1 ---
6: <something>
7: if (r7 > X) goto ...
8: r7 = 0
9: r9 += r6
The mark_precise_scalar_ids() would be called at:
- (9) and current id assignments would be used.
- (6) and id assignments saved in checkpoint #1 would be used.
If <something> is the code that modifies r6/r7 the link would be
broken and we would overestimate the set of precise registers.
