On Wed, 14 May 2025 at 13:30, Luis Gerhorst <luis.gerho...@fau.de> wrote:
>
> Kumar Kartikeya Dwivedi <mem...@gmail.com> writes:
>
> (including relevant part from other message)
>
> > On Thu, 1 May 2025 at 04:00, Luis Gerhorst <luis.gerho...@fau.de> wrote:
> >
> >> +static bool error_recoverable_with_nospec(int err)
> >> +{
> >> + /* Should only return true for non-fatal errors that are allowed to
> >> + * occur during speculative verification. For these we can insert a
> >> + * nospec and the program might still be accepted. Do not include
> >> + * something like ENOMEM because it is likely to re-occur for the
> >> next
> >> + * architectural path once it has been recovered-from in all
> >> speculative
> >> + * paths.
> >> + */
> >> + return err == -EPERM || err == -EACCES || err == -EINVAL;
> >> +}
> >
> > Why can't we unconditionally do this? So the path with speculation
> > that encounters an error (even if EFAULT) is not explored for the
> > remaining pushed speculative states. If the error remains regardless
> > of speculation normal symbolic execution will encounter it. The
> > instructions only explored as part of speculative execution are not
> > marked as seen (see: sanitize_mark_insn_seen), so they'll be dead code
> > eliminated and the code doesn't reach the JIT, so no "unsafe gadget"
> > remains in the program where execution can be steered.
> >
> > So the simplest thing (without having to reason about these three
> > error codes, I'm sure things will get out of sync or we'll miss
> > potential candidates) is probably to just unconditionally mark
> > cur_aux(env)->nospec.
>
> [...]
>
> > Hm, now looking at this and thinking more about this, I think
> > recoverable error logic is probably ok as is.
> > Scratch my earlier suggestion about unconditional handling. I guess
> > what would be better would be
> > handling everything except fatal ones. In case of fatal ones we should
> > really quit verification and return.
> > We may make partial changes to verifier state / env and try to bail
> > out using -ENOMEM and -EFAULT.
> > So unconditional continuation would be problematic as we'd act in a
> > partial state never meant to be seen.
> >
> > The logic otherwise looks ok, so:
> >
> > Acked-by: Kumar Kartikeya Dwivedi <mem...@gmail.com>
>
> Thank you very much for having a look, so then I will leave it as is if
> I understand you correctly.
>
> Please let me know if "what would be better would be handling everything
> except fatal ones" was meant literally. Such a deny-list approach would
> likely be:
>
> return err != -ENOMEM && err != -EFAULT;
>
> I initially decided to limit it to -EPERM, -EACCES, and -EINVAL as I was
> relatively confident all their cases were safe to "catch" and because it
> already had the desired effect for most real-world programs. However, if
> you find the deny-list approach easier to reason about, I can also do
> that. In that case, I will review the remaining errors (besides -EPERM,
> -EACCES, and -EINVAL) and make sure they can be caught.
>
> Also, thanks for the pointer regarding sanitize_check_bounds() (sorry
> for the delay; the message is still on my to-do list). I will address it
> in v4 if it is safe or send a separate fix if it is indeed a bug.
Yeahl, that's correct.
My only concern was if things shift around we return -EBUSY or whatever
(even though it's unlikely, but you get the idea) it will be missed
and we may break use cases we were permitting? Definitely need to be
careful either way, but I guess the surface of interaction for unpriv programs
is relatively set in stone so it won't matter too much.
It's probably better since you've audited paths returning that error
which do not leave things in a partial state. So I guess we should be
conservative and stick to the three you have right now.
