Re: Rethink how to deal with division/modulo-on-zero (was Re: FW: ebpf-docs: draft of ISA doc updates in progress)

[Shung-Hsi Yu <shung-hsi.yu@suse.com>]

On Wed, Sep 21, 2022 at 02:41:28PM +0000, Dave Thaler wrote:
> Shung-Hsi Yu <shung-hsi.yu@suse.com> writes: 
> > Just like how BPF verifier prevents a _possible_ out-of-bound memory access,
> > e.g. arr[i] when `i` is not bound-checked. Ideally I'd expect a coherent
> > approach toward division/modulo-on-zero as well; the verifier should prevent
> > program that _might_ do division-on-zero from loading in the first place.
> [...]
> > Admittedly even if achievable, this is a radical approach that is not backward
> > compatible. If such check is implemented, programs that used to load may
> > now be rejected.
> 
> FWIW, the PREVAIL verifier attempted to do that, although it was incomplete until a patch I just submitted to it yesterday.

Cool, and skimming through the PR I'm surprised by how minimal the changes
are. Interesting to know that it's possible.

> However, when running the patched version, it would reject some cilium, falco, suricata, etc. programs that it uses as test cases,
> so my patch proposed making it optional in that verifier although maybe there's
> some better alternative.
> 
> Certainly I think a runtime should implement the 0 check itself regardless of whether it's rejected or allowed by verification, but I wanted to share evidence that your "may now be rejected" is demonstrably true.

Thanks!

> Dave
>