[PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[dthaler1968]

From: Dave Thaler <dthaler@microsoft.com>

Fix modulo zero, division by zero, overflow, and underflow.
Also clarify how a negative immediate value is used in unsigned division

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
---
 Documentation/bpf/instruction-set.rst | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
index e672d5ec6cc..2ba7c618f33 100644
--- a/Documentation/bpf/instruction-set.rst
+++ b/Documentation/bpf/instruction-set.rst
@@ -99,19 +99,26 @@ code      value  description
 BPF_ADD   0x00   dst += src
 BPF_SUB   0x10   dst -= src
 BPF_MUL   0x20   dst \*= src
-BPF_DIV   0x30   dst /= src
+BPF_DIV   0x30   dst = (src != 0) ? (dst / src) : 0
 BPF_OR    0x40   dst \|= src
 BPF_AND   0x50   dst &= src
 BPF_LSH   0x60   dst <<= src
 BPF_RSH   0x70   dst >>= src
 BPF_NEG   0x80   dst = ~src
-BPF_MOD   0x90   dst %= src
+BPF_MOD   0x90   dst = (src != 0) ? (dst % src) : dst
 BPF_XOR   0xa0   dst ^= src
 BPF_MOV   0xb0   dst = src
 BPF_ARSH  0xc0   sign extending shift right
 BPF_END   0xd0   byte swap operations (see `Byte swap instructions`_ below)
 ========  =====  ==========================================================
 
+Underflow and overflow are allowed during arithmetic operations,
+meaning the 64-bit or 32-bit value will wrap.  If
+eBPF program execution would result in division by zero,
+the destination register is instead set to zero.
+If execution would result in modulo by zero,
+the destination register is instead left unchanged.
+
 ``BPF_ADD | BPF_X | BPF_ALU`` means::
 
   dst_reg = (u32) dst_reg + (u32) src_reg;
@@ -128,6 +135,10 @@ BPF_END   0xd0   byte swap operations (see `Byte swap instructions`_ below)
 
   dst_reg = dst_reg ^ imm32
 
+Also note that the division and modulo operations are unsigned,
+where 'imm' is first sign extended to 64 bits and then converted
+to an unsigned 64-bit value.  There are no instructions for
+signed division or modulo.
 
 Byte swap instructions
 ~~~~~~~~~~~~~~~~~~~~~~
-- 
2.33.4

Re: [PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[sdf]

On 01/05, dthaler1968@googlemail.com wrote:
> From: Dave Thaler <dthaler@microsoft.com>

> Fix modulo zero, division by zero, overflow, and underflow.
> Also clarify how a negative immediate value is used in unsigned division

> Signed-off-by: Dave Thaler <dthaler@microsoft.com>

Acked-by: Stanislav Fomichev <sdf@google.com>

With a small note below.

> ---
>   Documentation/bpf/instruction-set.rst | 15 +++++++++++++--
>   1 file changed, 13 insertions(+), 2 deletions(-)

> diff --git a/Documentation/bpf/instruction-set.rst  
> b/Documentation/bpf/instruction-set.rst
> index e672d5ec6cc..2ba7c618f33 100644
> --- a/Documentation/bpf/instruction-set.rst
> +++ b/Documentation/bpf/instruction-set.rst
> @@ -99,19 +99,26 @@ code      value  description
>   BPF_ADD   0x00   dst += src
>   BPF_SUB   0x10   dst -= src
>   BPF_MUL   0x20   dst \*= src
> -BPF_DIV   0x30   dst /= src
> +BPF_DIV   0x30   dst = (src != 0) ? (dst / src) : 0
>   BPF_OR    0x40   dst \|= src
>   BPF_AND   0x50   dst &= src
>   BPF_LSH   0x60   dst <<= src
>   BPF_RSH   0x70   dst >>= src
>   BPF_NEG   0x80   dst = ~src
> -BPF_MOD   0x90   dst %= src
> +BPF_MOD   0x90   dst = (src != 0) ? (dst % src) : dst
>   BPF_XOR   0xa0   dst ^= src
>   BPF_MOV   0xb0   dst = src
>   BPF_ARSH  0xc0   sign extending shift right
>   BPF_END   0xd0   byte swap operations (see `Byte swap instructions`_  
> below)
>   ========  =====   
> ==========================================================

> +Underflow and overflow are allowed during arithmetic operations,
> +meaning the 64-bit or 32-bit value will wrap.  If
> +eBPF program execution would result in division by zero,
> +the destination register is instead set to zero.
> +If execution would result in modulo by zero,
> +the destination register is instead left unchanged.
> +
>   ``BPF_ADD | BPF_X | BPF_ALU`` means::

>     dst_reg = (u32) dst_reg + (u32) src_reg;
> @@ -128,6 +135,10 @@ BPF_END   0xd0   byte swap operations (see `Byte  
> swap instructions`_ below)

>     dst_reg = dst_reg ^ imm32


[..]

> +Also note that the division and modulo operations are unsigned,
> +where 'imm' is first sign extended to 64 bits and then converted
> +to an unsigned 64-bit value.  There are no instructions for
> +signed division or modulo.

Less sure about this part, but it looks to be true at least by looking at
the interpreter which does:

DST = DST / IMM

where:

DST === (u64) regs[insn->dst_reg]
IMM === (s32) insn->imm

(and s32 is sign-expanded to u64 according to C rules)

>   Byte swap instructions
>   ~~~~~~~~~~~~~~~~~~~~~~
> --
> 2.33.4

Re: [PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[Daniel Borkmann]

On 1/5/23 8:01 PM, sdf@google.com wrote:
> On 01/05, dthaler1968@googlemail.com wrote:
>> From: Dave Thaler <dthaler@microsoft.com>
> 
>> Fix modulo zero, division by zero, overflow, and underflow.
>> Also clarify how a negative immediate value is used in unsigned division
> 
>> Signed-off-by: Dave Thaler <dthaler@microsoft.com>
> 
> Acked-by: Stanislav Fomichev <sdf@google.com>
> 
> With a small note below.
> 
>> ---
>>   Documentation/bpf/instruction-set.rst | 15 +++++++++++++--
>>   1 file changed, 13 insertions(+), 2 deletions(-)
> 
>> diff --git a/Documentation/bpf/instruction-set.rst b/Documentation/bpf/instruction-set.rst
>> index e672d5ec6cc..2ba7c618f33 100644
>> --- a/Documentation/bpf/instruction-set.rst
>> +++ b/Documentation/bpf/instruction-set.rst
>> @@ -99,19 +99,26 @@ code      value  description
>>   BPF_ADD   0x00   dst += src
>>   BPF_SUB   0x10   dst -= src
>>   BPF_MUL   0x20   dst \*= src
>> -BPF_DIV   0x30   dst /= src
>> +BPF_DIV   0x30   dst = (src != 0) ? (dst / src) : 0
>>   BPF_OR    0x40   dst \|= src
>>   BPF_AND   0x50   dst &= src
>>   BPF_LSH   0x60   dst <<= src
>>   BPF_RSH   0x70   dst >>= src
>>   BPF_NEG   0x80   dst = ~src
>> -BPF_MOD   0x90   dst %= src
>> +BPF_MOD   0x90   dst = (src != 0) ? (dst % src) : dst
>>   BPF_XOR   0xa0   dst ^= src
>>   BPF_MOV   0xb0   dst = src
>>   BPF_ARSH  0xc0   sign extending shift right
>>   BPF_END   0xd0   byte swap operations (see `Byte swap instructions`_ below)
>>   ========  =====  ==========================================================
> 
>> +Underflow and overflow are allowed during arithmetic operations,
>> +meaning the 64-bit or 32-bit value will wrap.  If
>> +eBPF program execution would result in division by zero,
>> +the destination register is instead set to zero.
>> +If execution would result in modulo by zero,
>> +the destination register is instead left unchanged.
>> +
>>   ``BPF_ADD | BPF_X | BPF_ALU`` means::
> 
>>     dst_reg = (u32) dst_reg + (u32) src_reg;
>> @@ -128,6 +135,10 @@ BPF_END   0xd0   byte swap operations (see `Byte swap instructions`_ below)
> 
>>     dst_reg = dst_reg ^ imm32
> 
> 
> [..]
> 
>> +Also note that the division and modulo operations are unsigned,
>> +where 'imm' is first sign extended to 64 bits and then converted
>> +to an unsigned 64-bit value.  There are no instructions for
>> +signed division or modulo.
> 
> Less sure about this part, but it looks to be true at least by looking at
> the interpreter which does:
> 
> DST = DST / IMM
> 
> where:
> 
> DST === (u64) regs[insn->dst_reg]
> IMM === (s32) insn->imm
> 
> (and s32 is sign-expanded to u64 according to C rules)

Yeap, the actual operation is in the target width, so for 32 bit it's casted
to u32, e.g. for modulo (note that the verifier rewrites it into `(src != 0) ?
(dst % src) : dst` form, so here is just the extract of the plain mod insn and
it's similar for div):

         ALU64_MOD_X:
                 div64_u64_rem(DST, SRC, &AX);
                 DST = AX;
                 CONT;
         ALU_MOD_X:
                 AX = (u32) DST;
                 DST = do_div(AX, (u32) SRC);
                 CONT;
         ALU64_MOD_K:
                 div64_u64_rem(DST, IMM, &AX);
                 DST = AX;
                 CONT;
         ALU_MOD_K:
                 AX = (u32) DST;
                 DST = do_div(AX, (u32) IMM);
                 CONT;

So in above phrasing the middle part needs to be adapted or just removed.

Thanks,
Daniel

RE: [PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[Dave Thaler]

Daniel Borkmann wrote:
[...]
> >> +Also note that the division and modulo operations are unsigned,
> >> +where 'imm' is first sign extended to 64 bits and then converted to
> >> +an unsigned 64-bit value.  There are no instructions for signed
> >> +division or modulo.
> >
> > Less sure about this part, but it looks to be true at least by looking
> > at the interpreter which does:
> >
> > DST = DST / IMM
> >
> > where:
> >
> > DST === (u64) regs[insn->dst_reg]
> > IMM === (s32) insn->imm
> >
> > (and s32 is sign-expanded to u64 according to C rules)
> 
> Yeap, the actual operation is in the target width, so for 32 bit it's casted to
> u32, e.g. for modulo (note that the verifier rewrites it into `(src != 0) ?
> (dst % src) : dst` form, so here is just the extract of the plain mod insn and it's
> similar for div):
> 
>          ALU64_MOD_X:
>                  div64_u64_rem(DST, SRC, &AX);
>                  DST = AX;
>                  CONT;
>          ALU_MOD_X:
>                  AX = (u32) DST;
>                  DST = do_div(AX, (u32) SRC);
>                  CONT;
>          ALU64_MOD_K:
>                  div64_u64_rem(DST, IMM, &AX);
>                  DST = AX;
>                  CONT;
>          ALU_MOD_K:
>                  AX = (u32) DST;
>                  DST = do_div(AX, (u32) IMM);
>                  CONT;
> 
> So in above phrasing the middle part needs to be adapted or just removed.

The phrasing was based on the earlier discussion on this list (see
https://lore.kernel.org/bpf/CAADnVQJ387tWd7WgxqfoB44xMe17bY0RRp_Sng3xMnKsywFpxg@mail.gmail.com/) where
Alexei wrote "imm32 is _sign_ extended everywhere",
and I cited the div_k tests in lib/test_bpf.c that assume sign extension
not zero extension.

So I don't know how to reconcile your comments with that thread.
If you do, please educate me :)

Dave

Re: [Bpf] [PATCH] bpf, docs: Fix modulo zero, division by zero, overflow, and underflow

[Daniel Borkmann]

On 1/6/23 7:11 PM, Dave Thaler wrote:
> Daniel Borkmann wrote:
> [...]
>>>> +Also note that the division and modulo operations are unsigned,
>>>> +where 'imm' is first sign extended to 64 bits and then converted to
>>>> +an unsigned 64-bit value.  There are no instructions for signed
>>>> +division or modulo.
>>>
>>> Less sure about this part, but it looks to be true at least by looking
>>> at the interpreter which does:
>>>
>>> DST = DST / IMM
>>>
>>> where:
>>>
>>> DST === (u64) regs[insn->dst_reg]
>>> IMM === (s32) insn->imm
>>>
>>> (and s32 is sign-expanded to u64 according to C rules)
>>
>> Yeap, the actual operation is in the target width, so for 32 bit it's casted to
>> u32, e.g. for modulo (note that the verifier rewrites it into `(src != 0) ?
>> (dst % src) : dst` form, so here is just the extract of the plain mod insn and it's
>> similar for div):
>>
>>           ALU64_MOD_X:
>>                   div64_u64_rem(DST, SRC, &AX);
>>                   DST = AX;
>>                   CONT;
>>           ALU_MOD_X:
>>                   AX = (u32) DST;
>>                   DST = do_div(AX, (u32) SRC);
>>                   CONT;
>>           ALU64_MOD_K:
>>                   div64_u64_rem(DST, IMM, &AX);
>>                   DST = AX;
>>                   CONT;
>>           ALU_MOD_K:
>>                   AX = (u32) DST;
>>                   DST = do_div(AX, (u32) IMM);
>>                   CONT;
>>
>> So in above phrasing the middle part needs to be adapted or just removed.
> 
> The phrasing was based on the earlier discussion on this list (see
> https://lore.kernel.org/bpf/CAADnVQJ387tWd7WgxqfoB44xMe17bY0RRp_Sng3xMnKsywFpxg@mail.gmail.com/) where
> Alexei wrote "imm32 is _sign_ extended everywhere",
> and I cited the div_k tests in lib/test_bpf.c that assume sign extension
> not zero extension.

`Where 'imm' is first sign extended to 64 bits and then converted to an unsigned
64-bit value` is true for the 64 bit operation, for the 32-bit it's just converted
to an unsigned 32-bit value, see the (u32)IMM which is (u32)(s32) insn->imm. From
the phrasing, it was a bit less clear perhaps.

Thanks,
Daniel