On Fri, Oct 27, 2023 at 01:46:35PM -0700, Andrii Nakryiko wrote:
> On Thu, Oct 26, 2023 at 10:44 PM Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> wrote:
> > On Mon, Oct 23, 2023 at 09:14:08PM +0800, Shung-Hsi Yu wrote:
> > > Hi,
> > >
> > > CC those who had worked on bound tracking before for feedbacks, as well as
> > > Dave who works on PREVAIL (verifier used on Windows) and Paul who've written
> > > about PREVAIL[1], for whether there's existing knowledge on this topic.
> > >
> > > Here goes a long one...
> > >
> > > ---
> > >
> > > While looking at Andrii's patches that improves bounds logic (specifically
> > > patches [2][3]). I realize we may be able to unify umin/umax/smin/smax into
> > > just two u64. Not sure if this has already been discussed off-list or is
> > > being worked upon, but I can't find anything regarding this by searching
> > > within the BPF mailing list.
> > >
> > > For simplicity sake I'll focus on unsigned bounds for now. What we have
> > > right in the Linux Kernel now is essentially
> > >
> > > struct bounds {
> > > u64 umin;
> > > u64 umax;
> > > }
> > >
> > > We can visualize the above as a number line, using asterisk to denote the
> > > values between umin and umax.
> > >
> > > u64
> > > |----------********************--|
> > >
> > > Say if we have umin = A, and umax = B (where B > 2^63). Representing the
> > > magnitude of umin and umax visually would look like this
> > >
> > > <----------> A
> > > |----------********************--|
> > > <-----------------------------> B (larger than 2^63)
> > >
> > > Now if we go through a BPF_ADD operation and adds 2^(64 - 1) = 2^63,
> > > currently the verifier will detect that this addition overflows, and thus
> > > reset umin and umax to 0 and U64_MAX, respectively; blowing away existing
> > > knowledge.
> > >
> > > |********************************|
> > >
> > > Had we used u65 (1-bit more than u64) and tracks the bound with u65_min and
> > > u65_max, the verifier would have captured the bound just fine. (This idea
> > > comes from the special case mentioned in Andrii's patch[3])
> > >
> > > u65
> > > <---------------> 2^63
> > > <----------> A
> > > <--------------------------> u65_min = A + 2^63
> > > |--------------------------********************------------------|
> > > <---------------------------------------------> u65_max = B + 2^63
> > >
> > > Continue on this thought further, let's attempting to map this back to u64
> > > number lines (using two of them to fit everything in u65 range), it would
> > > look like
> > >
> > > u65
> > > |--------------------------********************------------------|
> > > vvvvvvvvvvvvvvvvvvvv
> > > |--------------------------******|*************------------------|
> > > u64 u64
> > >
> > > And would seems that we'd need two sets of u64 bounds to preserve our
> > > knowledge.
> > >
> > > |--------------------------******| u64 bound #1
> > > |**************------------------| u64 bound #2
> > >
> > > Or just _one_ set of u64 bound if we somehow are able to track the union of
> > > bound #1 and bound #2 at the same time
> > >
> > > |--------------------------******| u64 bound #1
> > > U |**************------------------| u64 bound #2
> > > vvvvvvvvvvvvvv vvvvvv union on the above bounds
> > > |**************------------******|
> > >
> > > However, this bound crosses the point between U64_MAX and 0, which is not
> > > semantically possible to represent with the umin/umax approach. It just
> > > makes no sense.
> > >
> > > |**************------------******| union of bound #1 and bound #2
> > >
> > > The way around this is that we can slightly change how we track the bounds,
> > > and instead use
> > >
> > > struct bounds {
> > > u64 base; /* base = umin */
> > > /* Maybe there's a better name other than "size" */
> > > u64 size; /* size = umax - umin */
> > > }
> > >
> > > Using this base + size approach, previous old bound would have looked like
> > >
> > > <----------> base = A
> > > |----------********************--|
> > > <------------------> size = B - A
> > >
> > > Looking at the bounds this way means we can now capture the union of bound
> > > #1 and bound #2 above. Here it is again for reference
> > >
> > > |**************------------******| union of bound #1 and bound #2
> > >
> > > Because registers are u64-sized, they wraps, and if we extend the u64 number
> > > line, it would look like this due to wrapping
> > >
> > > u64 same u64 wrapped
> > > |**************------------******|*************------------******|
> > >
> > > Which can be capture with the base + size semantic
> > >
> > > <--------------------------> base = (u64) A + 2^63
> > > |**************------------******|*************------------******|
> > > <------------------> size = B - A,
> > > doesn't change after add
> > >
> > > Or looking it with just a single u64 number line again
> > >
> > > <--------------------------> base = (u64) A + 2^63
> > > |**************------------******|
> > > <-------------> base + size = (u64) (B + 2^32)
> > >
> > > This would mean that umin and umax is no longer readily available, we now
> > > have to detect whether base + size wraps to determin whether umin = 0 or
> > > base (and similar for umax). But the verifier already have the code to do
> > > that in the existing scalar_min_max_add(), so it can be done by reusing
> > > existing code.
> > >
> > > ---
> > >
> > > Side tracking slightly, a benefit of this base + size approach is that
> > > scalar_min_max_add() can be made even simpler:
> > >
> > > scalar_min_max_add(struct bpf_reg_state *dst_reg,
> > > struct bpf_reg_state *src_reg)
> > > {
> > > /* This looks too simplistic to have worked */
> > > dst_reg.base = dst_reg.base + src_reg.base;
> > > dst_reg.size = dst_reg.size + src_reg.size;
> > > }
> > >
> > > Say we now have another unsigned bound where umin = C and umax = D
> > >
> > > <--------------------> C
> > > |--------------------*********---|
> > > <----------------------------> D
> > >
> > > If we want to track the bounds after adding two registers on with umin = A &
> > > umax = B, the other with umin = C and umin = D
> > >
> > > <----------> A
> > > |----------********************--|
> > > <-----------------------------> B
> > > +
> > > <--------------------> C
> > > |--------------------*********---|
> > > <----------------------------> D
> > >
> > > The results falls into the following u65 range
> > >
> > > |--------------------*********---|-------------------------------|
> > > + |----------********************--|-------------------------------|
> > >
> > > |------------------------------**|**************************-----|
> > >
> > > This result can be tracked with base + size approach just fine. Where the
> > > base and size are as follow
> > >
> > > <------------------------------> base = A + C
> > > |------------------------------**|**************************-----|
> > > <--------------------------->
> > > size = (B - A) + (D - C)
> > >
> > > ---
> > >
> > > Now back to the topic of unification of signed and unsigned range. Using the
> > > union of bound #1 and bound #2 again as an example (size = B - A, and
> > > base = (u64) A + 2^63)
> > >
> > > |**************------------******| union of bound #1 and bound #2
> > >
> > > And look at it's wrapped number line form again
> > >
> > > u64 same u64 wrapped
> > > <--------------------------> base
> > > |**************------------******|*************------------******|
> > > <------------------> size
> > >
> > > Now add in the s64 range and align both u64 range and s64 at 0, we can see
> > > what previously was a bound that umin/umax cannot track is simply a valid
> > > smin/smax bound (idea drawn from patch [2]).
> > >
> > > 0
> > > |**************------------******|*************------------******|
> > > |----------********************--|
> > > s64
> > >
> > > The question now is be what is the "signed" base so we proceed to calculate
> > > the smin/smax. Note that base starts at 0, so for s64 the line that
> > > represents base doesn't start from the left-most location.
> > > (OTOH size stays the same, so we know it already)
> > >
> > > s64
> > > 0
> > > <-----> signed base = ?
> > > |----------********************--|
> > > <------------------> size is the same
> > >
> > > If we put u64 range back into the picture again, we can see that the "signed
> > > base" was, in fact, just base casted into s64, so there's really no need for
> > > a "signed" base at all
> > >
> > > <--------------------------> base
> > > |**************------------******|
> > > 0
> > > <-----> signed base = (s64) base
> > > |----------********************--|
> > >
> > > Which shows base + size approach capture signed and unsigned bounds at the
> > > same time. Or at least its the best attempt I can make to show it.
> > >
> > > One way to look at this is that base + size is just a generalization of
> > > umin/umax, taking advantage of the fact that the similar underlying hardware
> > > is used both for the execution of BPF program and bound tracking.
> > >
> > > I wonder whether this is already being done elsewhere, e.g. by PREVAIL or
> > > some of static code analyzer, and I can just borrow the code from there
> > > (where license permits).
> >
> > As per [1], PREVAIL uses the zone domain[2][3] to track values along with
> > relationships between values, where as the Linux Kernel tracks values with
> > min/max (i.e. interval domain) and tnum. In short, PREVAIL does not use this
> > trick, but I guess it probably don't need to since it's already using
> > something that considered to be more advanced.
>
> tnum is actually critical for checking memory alignment (i.e.,
> checking that low 2-3 bits are always zero), which range tracking
> can't do. So I suspect PREVAIL doesn't validate those conditions,
> while kernel's verifier does.
I didn't know this :)
Looking into Wikipedia's article on Zone domain it seems that indeed it
cannot tell memory alignment.
> > Also, found some research papers on this topic referring to it as Wrapped
> > Intervals[4] or Modular Interval Domain[5]. The former has an MIT-licensed
> > C++ implementation[6] available as reference.
> >
> > 1: https://pchaigno.github.io/ebpf/2023/09/06/prevail-understanding-the-windows-ebpf-verifier.html
> > 2: https://en.wikipedia.org/wiki/Difference_bound_matrix#Zone
> > 3: https://github.com/vbpf/ebpf-verifier/blob/6d5ad53/src/crab/split_dbm.hpp
> > 4: https://dl.acm.org/doi/abs/10.1145/2651360
>
> this one (judging by the name of the paper) looks exactly like what we
> are trying to do here. I'll give it a read some time later.
I'm putting off reading it fully (for some fun), and only went through
the introduction and a few figures so far. It does seem like it had
all the bits that I need to know to make this work.
Also, the use of circles to visualize the numerical domain in the paper
makes great intuitive sense, too bad my ASCII art skill is not good
enough to draw circles.
> ... Meanwhile
> I posted full patch set with range logic ([0]), feel free to take a
> look as well.
>
> [0] https://patchwork.kernel.org/project/netdevbpf/list/?series=797178&state=*
A bit late to the party, but I'm coming back to (the latest version of)
this series.
[...]
