BPF List
 help / color / mirror / Atom feed
From: Eduard Zingerman <eddyz87@gmail.com>
To: Andrii Nakryiko <andrii.nakryiko@gmail.com>
Cc: bpf@vger.kernel.org, ast@kernel.org, andrii@kernel.org,
	daniel@iogearbox.net,  martin.lau@linux.dev, kernel-team@fb.com,
	yhs@fb.com
Subject: Re: [PATCH bpf-next v2 1/4] bpf: verify scalar ids mapping in regsafe() using check_ids()
Date: Wed, 31 May 2023 23:31:04 +0300	[thread overview]
Message-ID: <aa64ee05281ec952df41b7a7842ed2836ae79762.camel@gmail.com> (raw)
In-Reply-To: <CAEf4BzYE_7m3FNc6dtZeKb6tNbW4xkhz6SVdV6KetD5reSer6A@mail.gmail.com>

On Wed, 2023-05-31 at 13:12 -0700, Andrii Nakryiko wrote:
> On Wed, May 31, 2023 at 12:30 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Wed, 2023-05-31 at 11:29 -0700, Andrii Nakryiko wrote:
> > > On Wed, May 31, 2023 at 10:21 AM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > > > 
> > > > On Tue, 2023-05-30 at 14:37 -0700, Andrii Nakryiko wrote:
> > > > [...]
> > > > > Also, it might make sense to drop SCALAR register IDs as soon as we
> > > > > have only one instance of it left (e.g., if "paired" register was
> > > > > overwritten already). I.e., aggressively drop IDs when they become
> > > > > useless. WDYT?
> > > > 
> > > > I added modification which resets sole scalar IDs to zero before
> > > > states comparison, it shows some speedup but is still slow:
> > > > 
> > > >   Filter        | Number of programs | Number of programs
> > > >                 | patch #1           | patch #1 + sole scalar ID pruning
> > > >   ----------------------------------------------------------------------
> > > >   states_pct>10 | 40                 | 40
> > > >   states_pct>20 | 20                 | 19
> > > >   states_pct>30 | 15                 | 13
> > > >   states_pct>40 | 11                 | 8
> > > > 
> > > > (Out of 177 programs).
> > > > 
> > > > I'll modify mark_chain_precision() to propagate precision marks for
> > > > find_equal_scalars(), so that it could be compared to current patch #3
> > > > in terms of code complexity and verification performance.
> > > > 
> > > > If you have any thoughts regarding my previous email, please share.
> > > > 
> > > 
> > > Yep, I do. Given SCALAR registers with the same ID are meant to "share
> > > the destiny", shouldn't it be required that when we mark r6 as precise
> > > we should automatically mark linked r7 as precise at the same point.
> > > So in your example:
> > > 
> > > 7: r9 += r6
> > > 
> > > should be where we request both r6 and r7 (and whatever other register
> > > has the same ID) to be marked as precise. It should be very easy to
> > > implement, especially given my recent refactoring with
> > > mark_chain_precision_batch.
> > 
> > Ok, I'll modify the `struct backtrack_state` as follows:
> > 
> >   struct backtrack_state {
> >         struct bpf_verifier_env *env;
> >         u32 frame;
> >         u32 reg_masks[MAX_CALL_FRAMES];
> > +       u32 reg_ids[MAX_CALL_FRAMES];
> >         u64 stack_masks[MAX_CALL_FRAMES];
> > +       u64 stack_ids[MAX_CALL_FRAMES];
> >   };
> > 
> > And add corresponding logic to backtrack_insn().
> 
> I don't see why you need to change anything about backtrack_state at
> all, so we are not on the same page.
> 
> What I propose is that in mark_chain_precision(), when given regno, go
> over all *current* registers with the same ID, and set all of them as
> "to be marked precise". And then call mark_chain_precision_batch().
> See propagate_precision() for how we do similar stuff for bulk
> precision propagation.
> 
> backtrack_state shouldn't need to know about IDs, unless I'm missing something

Consider a modified version of the original example:

  1: r9 = ... some pointer with range X ...
  2: r6 = ... unbound scalar ID=a ...
  3: r7 = ... unbound scalar ID=b ...
  4: if (r6 > r7) goto +1
  5: r7 = r6
  6: if (r7 > X) goto ...
  7: r7 = 0
  8: r9 += r6

Suppose verification path is 1-8, the ID assignments are:

                            r6.id r7.id
  4: if (r6 > r7) goto +1   a     b
  5: r7 = r6                a     a
  6: if (r7 > X) goto ...   a     a
  7: r7 = 0                 a     -
  8: r9 += r6               a     -

When mark_chain_precision() is called at (8) it no longer knows that
r6 and r7 shared the same ID at some point in the past. What you
suggest won't work in this case, what I suggest won't work as well.

Looks like the only way to do it correctly is to save ID assignments
after each find_equal_scalars() (for (6) in this example) in the
bpf_verifier_state, and use this information in backtrack_insn().
For example, extend jmp_history.

> 
> > 
> > > The question I have (and again, haven't spent any time thinking about
> > > any other corner cases, sorry) is whether that alone would be a proper
> > > fix?
> > 
> > As far as I understand, in terms of correctness it would be a proper fix.
> > In terms of performance, I hope that it would be enough but we will see.
> 
> ok, let's try that then, before we commit to u32_hashset stuff
> 
> > 
> > > As for this u32_hashset, it just feels like a big overkill, tbh. If we
> > > have to do something like that, wouldn't it be better to, say, set
> > > highest bit in reg->id (for all linked registers, of course) to mark
> > > it as "used for range checks" instead of maintaining a separate check?
> > 
> > Unfortunately no, because this ID change would have to be propagated
> > backwards. It was the first implementation I tried.
> > 
> > > But just the whole idea of keeping track of some special circumstances
> > > under which IDs are meaningful seems wrong... All this logic is
> > > complicated, now we are adding another layer of complexity on top. And
> > > the complexity is not in the code, it's in thinking about all possible
> > > scenarios and their interactions.
> > 
> > I agree that adding more layers is a complication in itself.
> > Thank you for your input.
> > 
> > > > [...]
> > 


  reply	other threads:[~2023-05-31 20:31 UTC|newest]

Thread overview: 33+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-05-30 17:27 [PATCH bpf-next v2 0/4] verify scalar ids mapping in regsafe() Eduard Zingerman
2023-05-30 17:27 ` [PATCH bpf-next v2 1/4] bpf: verify scalar ids mapping in regsafe() using check_ids() Eduard Zingerman
2023-05-30 21:37   ` Andrii Nakryiko
2023-05-30 23:02     ` Eduard Zingerman
2023-06-01  2:05       ` Alexei Starovoitov
2023-06-01 16:57         ` Eduard Zingerman
2023-06-01 17:13           ` Alexei Starovoitov
2023-06-01 18:52             ` Eduard Zingerman
2023-06-02 18:50               ` Andrii Nakryiko
2023-06-02 19:13                 ` Eduard Zingerman
2023-06-02 19:27                   ` Alexei Starovoitov
2023-06-02 19:37                     ` Eduard Zingerman
2023-06-02 19:43                       ` Alexei Starovoitov
2023-06-02 19:51                         ` Eduard Zingerman
2023-06-02 20:03                           ` Alexei Starovoitov
2023-06-02 20:22                             ` Eduard Zingerman
2023-06-02 20:17                   ` Andrii Nakryiko
2023-06-02 21:13                     ` Eduard Zingerman
2023-06-02 22:07                       ` Andrii Nakryiko
2023-06-02 23:20                         ` Eduard Zingerman
2023-06-05 20:43                           ` Eduard Zingerman
     [not found]     ` <f2abf39bcd4de841a89bb248de9e242a880aaa93.camel@gmail.com>
2023-05-31 18:29       ` Andrii Nakryiko
2023-05-31 19:30         ` Eduard Zingerman
2023-05-31 20:12           ` Andrii Nakryiko
2023-05-31 20:31             ` Eduard Zingerman [this message]
2023-05-31 21:14               ` Andrii Nakryiko
2023-05-31 22:15                 ` Eduard Zingerman
2023-05-31 22:54                   ` Andrii Nakryiko
2023-05-31 23:42                     ` Eduard Zingerman
2023-06-01  0:23                       ` Andrii Nakryiko
2023-05-30 17:27 ` [PATCH bpf-next v2 2/4] selftests/bpf: verify that check_ids() is used for scalars in regsafe() Eduard Zingerman
2023-05-30 17:27 ` [PATCH bpf-next v2 3/4] bpf: filter out scalar ids not used for range transfer " Eduard Zingerman
2023-05-30 17:27 ` [PATCH bpf-next v2 4/4] selftests/bpf: check env->that range_transfer_ids has effect Eduard Zingerman

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=aa64ee05281ec952df41b7a7842ed2836ae79762.camel@gmail.com \
    --to=eddyz87@gmail.com \
    --cc=andrii.nakryiko@gmail.com \
    --cc=andrii@kernel.org \
    --cc=ast@kernel.org \
    --cc=bpf@vger.kernel.org \
    --cc=daniel@iogearbox.net \
    --cc=kernel-team@fb.com \
    --cc=martin.lau@linux.dev \
    --cc=yhs@fb.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox