On Wed, Apr 13, 2022 at 12:04 PM Nikolay Borisov <nborisov@xxxxxxxx> wrote:
>
>
>
> On 13.04.22 г. 20:29 ч., Zvi Effron wrote:
> > On Wed, Apr 13, 2022 at 12:08 AM Nikolay Borisov <nborisov@xxxxxxxx> wrote:
> >>
> >> <snip>
> >>>>>> // Add this dentry name to path
> >>>>>> struct qstr d_name = BPF_CORE_READ(dentry, d_name);
> >>>>>> // Ensure path is no longer than PATH_MAX-1 and copy the terminating NULL
> >>>>>> unsigned int len = (d_name.len+1) & (PATH_MAX-1);
> >>>>>> // Start writing from the end of the buffer
> >>>>>> unsigned int off = buf_off - len;
> >>>>>> // Is string buffer big enough for dentry name?
> >>>>>> int sz = 0;
> >>>>>> // verify no wrap occurred
> >>>>>> if (off <= buf_off)
> >>>>>> sz = bpf_probe_read_kernel_str(&string_p->buf[IDX(off)], len, (void *)d_name.name);
> >>>>>> else
> >>>>>> break;
> >>>>>>
> >>>>>> if (sz > 1) {
> >>>>>> buf_off -= 1; // replace null byte termination with slash sign
> >>>>>> bpf_probe_read(&(string_p->buf[IDX(buf_off)]), 1, &slash);
> >>>>>> buf_off -= sz - 1;
> >>>
> >>> Isn't it (theoretically) possible for this to underflow? What happens if
> >>> sz > 1 and sz >= buf_off?
> >>
> >> No, because sz is bounded by len since bpf_probe_read_kernel_str would
> >> copy at most len -1 bytes as per description of the function. Since
> >> we've ensured len is smaller than buff_off (due to off <= buf_off check)
> >> then sz is also guaranteed to be less than buf_off.
> >>
> >> <snip>
> >>
> >
> > That's in a single iteration, though. Each iteration, sz can be 4095 (when
> > len = PATH_MAX - 1). buff_off can be reduced by up to 4095 (1 + sz - 1). Your
> > loop allows 20 iterations, which would be a total adjustment to buff_off of
> > 77,786 before the last iteration. This would cause buff_off to underflow (it
> > starts at 32767).
>
> But in the last iteration it would result in an underflow which means
> we'd go into the else arm and break.
>
You might be in a case where the verifier does not track what's required to
prove correctness here. In order to prove correctness, relations between
len, sz, off, and buff_off must be tracked. The verifier does not track
relations between variables, just current state of registers.
You can see this when looking at how the verifier is validating via its output.
When it validates IDX(off), all it knows is the register being used has a
minimum value of 28672 and a maximum value of 32767. Similarly, it knows that
len has a maximum value of 4095. It does not know about the relation between
len and off. So when it compares off to buf, it sees that the maximum value of
IDX(off) (32767) plus the maximum value of len (4095) can exceed the size of
buf (32768).
To prove this isn't possible, it would need to know that as IDX(off) varies
upwards, len varies downwards by the same amount. But the verifier does not
track relations between variables (in fact, it doesn't even know about
variables) so it does not know this.
> >
> >>>>> IDX(off) is bounded, but verifier needs to be sure that `off + len`
> >>>>> never goes beyond map value. so you should make sure and prove off <=
> >>>>> MAX_PERCPU_BUFSIZE - PATH_MAX. Verifier actually caught a real bug for
> >>>>
> >>>> But that is guaranteed since off = buff_off - len, and buf_off is
> >>>> guaranteed to be at most MAX_PERCPU_BUFSIZE -1, meaning off is in the
> >>>> worst case MAX_PERCPU_BUFSIZE - len so the map value access can't go
> >>>> beyond the end ?
> >>>>
> >>>
> >>> If there's underflow in the calculation of buff_off (see above) then
> >>> buff_off > MAX_PERCPU_BUFSIZE - 1. Which makes off no longer bounded by
> >>> MAX_PERCPU_BUFSIZE - len, and it could exceed MAX_PERCPU_BUFSIZE.
> >>
> >> As per my rationale above I don't think buf_off can underflow.
> >>
> >>>
> >>
> >> <snip>
> >
