vbpf / prevail / 30762301447

86%

push

github

Check the divisor a 32-bit division actually uses (fixes #1205) (#1217)

* Check the divisor a 32-bit division actually uses (fixes #1205)

A 32-bit DIV/MOD divides by the low half of the divisor register, but the
divide-by-zero check tested the full 64-bit value:

    const auto v = s.is_signed ? reg.svalue : reg.uvalue;
    require_value(dom.state, v != 0, "Possible division by zero");

So a divisor that is a nonzero multiple of 2^32 passed the check while the
runtime divides by zero:

    r1 = 1
    r1 <<= 32          ; uvalue = 0x1_0000_0000, entails uvalue != 0
    w0 /= w1           ; the CPU's divisor is (u32)r1 == 0

With allow_division_by_zero=false the verifier accepted a program it exists to
reject. This is not a memory-safety hole -- eBPF defines /0 as 0 and %0 as the
dividend, and the transformer models that -- but the checker and the transformer
disagreed about what the divisor is: the transformer already reads it as
eval_interval(z, 32) while the checker read all 64 bits.

ValidDivisor carried no width, so the checker could not tell the two cases
apart. Give it the is64 of the division that produced it, and on the 32-bit path
test the same 32-bit view of the divisor the transformer divides by. The 64-bit
path keeps the existing entailment check, which is more precise than an interval
test on a relational domain.

The assertion now prints as "w2 != 0" for a 32-bit division, matching the
llvm-objdump register-naming convention already used for instruction operands,
so the message says which half was checked. Its reg_name helper moves to file
scope in printing.cpp to be shared with the assertion printer.

Regression tests in udivmod.yaml and sdivmod.yaml divide and take the modulo,
signed and unsigned, by a register holding 2^32; all four are accepted without
the fix. Two further tests pin precision: a 32-bit division by 2^32 + 5 is still
accepted (it divides by 5), and a 64-bit division by 2^32 is still accepted,
since there the divisor i... (continued)

11 of 11 new or added lines in 3 files covered. (100.0%)

9357 of 10771 relevant lines covered (86.87%)

6270727.46 hits per line