On Wed, Sep 21, 2022 at 02:41:28PM +0000, Dave Thaler wrote: > Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> 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 >
