Topics

math between pkt pointer and register with unbounded min value is not allowed #verifier

Simon
 

I'm playing with bcc to prototype an UDP load balancer.

I'm facing an issue that I didn't succeed to understand...

In my code I tried to validate my UDP packet using code like this :

    struct udphdr *udp;
    udp = iph + 1;
    if (udp + 1 > data_end)
        return XDP_DROP;
    __u16 udp_len = bpf_ntohs(udp->len);
    //__u16 udp_len = 8;
    if (udp_len < 8)
        return XDP_DROP;
    if (udp_len > 512) // TODO use a more approriate max value
        return XDP_DROP;
    if ((void *) udp + udp_len > data_end)
        return XDP_DROP;
And the verifier does not like it ..
28: (71) r2 = *(u8 *)(r7 +23)
29: (b7) r0 = 2
30: (55) if r2 != 0x11 goto pc+334
 R0=inv2 R1=pkt_end(id=0,off=0,imm=0) R2=inv17 R3=inv5 R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=34,imm=0) R8=pkt(id=0,off=34,r=34,imm=0) R9=pkt(id=0,off=14,r=34,imm=0) R10=fp0,call_-1
31: (bf) r2 = r8
32: (07) r2 += 8
33: (b7) r0 = 1
34: (2d) if r2 > r1 goto pc+330
 R0=inv1 R1=pkt_end(id=0,off=0,imm=0) R2=pkt(id=0,off=42,r=42,imm=0) R3=inv5 R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=42,imm=0) R8=pkt(id=0,off=34,r=42,imm=0) R9=pkt(id=0,off=14,r=42,imm=0) R10=fp0,call_-1
35: (69) r3 = *(u16 *)(r7 +38)
36: (dc) r3 = be16 r3
37: (bf) r2 = r3
38: (07) r2 += -8
39: (57) r2 &= 65535
40: (b7) r0 = 1
41: (25) if r2 > 0x1f8 goto pc+323
 R0=inv1 R1=pkt_end(id=0,off=0,imm=0) R2=inv(id=0,umax_value=504,var_off=(0x0; 0x1ff)) R3=inv(id=0) R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=42,imm=0) R8=pkt(id=0,off=34,r=42,imm=0) R9=pkt(id=0,off=14,r=42,imm=0) R10=fp0,call_-1
42: (bf) r2 = r7
43: (0f) r2 += r3
math between pkt pointer and register with unbounded min value is not allowed

I'm pretty sure the issue is about udp_len, that's why I tried to validate its value before to use it ... but without success...
When I set udp_len to 8 (just for testing) this seems to works. Any idea about that ?

Full code is available here : https://gist.github.com/sbernard31/d4fee7518a1ff130452211c0d355b3f7

(I'm using python-bpfcc  0.8.0-4 from debian sid with a 4.19.12 kernel)
(I don't know if this is the right place for this kind of question, )

Yonghong Song
 

On Wed, Mar 6, 2019 at 7:08 AM <contact@...> wrote:

I'm playing with bcc to prototype an UDP load balancer.

I'm facing an issue that I didn't succeed to understand...

In my code I tried to validate my UDP packet using code like this :

struct udphdr *udp;
udp = iph + 1;
if (udp + 1 > data_end)
return XDP_DROP;
__u16 udp_len = bpf_ntohs(udp->len);
//__u16 udp_len = 8;
if (udp_len < 8)
return XDP_DROP;
if (udp_len > 512) // TODO use a more approriate max value
return XDP_DROP;
if ((void *) udp + udp_len > data_end)
return XDP_DROP;

And the verifier does not like it ..
This is caused by compiler optimizations.


28: (71) r2 = *(u8 *)(r7 +23)
29: (b7) r0 = 2
30: (55) if r2 != 0x11 goto pc+334
R0=inv2 R1=pkt_end(id=0,off=0,imm=0) R2=inv17 R3=inv5 R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=34,imm=0) R8=pkt(id=0,off=34,r=34,imm=0) R9=pkt(id=0,off=14,r=34,imm=0) R10=fp0,call_-1
31: (bf) r2 = r8
32: (07) r2 += 8
33: (b7) r0 = 1
34: (2d) if r2 > r1 goto pc+330
R0=inv1 R1=pkt_end(id=0,off=0,imm=0) R2=pkt(id=0,off=42,r=42,imm=0) R3=inv5 R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=42,imm=0) R8=pkt(id=0,off=34,r=42,imm=0) R9=pkt(id=0,off=14,r=42,imm=0) R10=fp0,call_-1
35: (69) r3 = *(u16 *)(r7 +38)
36: (dc) r3 = be16 r3
r3 get the value from memory, its value could be any one as permitted
by the type.

37: (bf) r2 = r3
38: (07) r2 += -8
39: (57) r2 &= 65535
40: (b7) r0 = 1
41: (25) if r2 > 0x1f8 goto pc+323
test is done by r2. We indeed get better range for r2 (below:
R2=inv(id=0,umax_value=504,var_off=(0x0; 0x1ff)) )
but r3 range is not tightened.

R0=inv1 R1=pkt_end(id=0,off=0,imm=0) R2=inv(id=0,umax_value=504,var_off=(0x0; 0x1ff)) R3=inv(id=0) R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=42,imm=0) R8=pkt(id=0,off=34,r=42,imm=0) R9=pkt(id=0,off=14,r=42,imm=0) R10=fp0,call_-1
42: (bf) r2 = r7
43: (0f) r2 += r3
math between pkt pointer and register with unbounded min value is not allowed
Here, we use r3 to do arith and the verifier not happy. If we use the
tightened old r2, it may work.
The compiler does the right thing, just verifier is not advanced enough.


I'm pretty sure the issue is about udp_len, that's why I tried to validate its value before to use it ... but without success...
When I set udp_len to 8 (just for testing) this seems to works. Any idea about that ?
Yes, you will need some source workaround. You could try below (untested):

if (udp_len > 512) // TODO use a more approriate max value
return XDP_DROP;
+ udp_len = udp_len & 0x1ff;
if ((void *) udp + udp_len > data_end)
return XDP_DROP;


Full code is available here : https://gist.github.com/sbernard31/d4fee7518a1ff130452211c0d355b3f7

(I'm using python-bpfcc 0.8.0-4 from debian sid with a 4.19.12 kernel)
(I don't know if this is the right place for this kind of question, )

Jiong Wang
 

Yonghong Song writes:

On Wed, Mar 6, 2019 at 7:08 AM <contact@...> wrote:

I'm playing with bcc to prototype an UDP load balancer.

I'm facing an issue that I didn't succeed to understand...

In my code I tried to validate my UDP packet using code like this :

struct udphdr *udp;
udp = iph + 1;
if (udp + 1 > data_end)
return XDP_DROP;
__u16 udp_len = bpf_ntohs(udp->len);
//__u16 udp_len = 8;
if (udp_len < 8)
return XDP_DROP;
if (udp_len > 512) // TODO use a more approriate max value
return XDP_DROP;
if ((void *) udp + udp_len > data_end)
return XDP_DROP;

And the verifier does not like it ..
This is caused by compiler optimizations.


28: (71) r2 = *(u8 *)(r7 +23)
29: (b7) r0 = 2
30: (55) if r2 != 0x11 goto pc+334
R0=inv2 R1=pkt_end(id=0,off=0,imm=0) R2=inv17 R3=inv5 R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=34,imm=0) R8=pkt(id=0,off=34,r=34,imm=0) R9=pkt(id=0,off=14,r=34,imm=0) R10=fp0,call_-1
31: (bf) r2 = r8
32: (07) r2 += 8
33: (b7) r0 = 1
34: (2d) if r2 > r1 goto pc+330
R0=inv1 R1=pkt_end(id=0,off=0,imm=0) R2=pkt(id=0,off=42,r=42,imm=0) R3=inv5 R6=ctx(id=0,off=0,imm=0) R7=pkt(id=0,off=0,r=42,imm=0) R8=pkt(id=0,off=34,r=42,imm=0) R9=pkt(id=0,off=14,r=42,imm=0) R10=fp0,call_-1
35: (69) r3 = *(u16 *)(r7 +38)
36: (dc) r3 = be16 r3
r3 get the value from memory, its value could be any one as permitted
by the type.

37: (bf) r2 = r3
38: (07) r2 += -8
39: (57) r2 &= 65535
40: (b7) r0 = 1
41: (25) if r2 > 0x1f8 goto pc+323
test is done by r2. We indeed get better range for r2 (below:
R2=inv(id=0,umax_value=504,var_off=(0x0; 0x1ff)) )
but r3 range is not tightened.
I had run into similar issue when debugging some other rejection before
JMP32 introduced when LLVM was generating similar sequences under defult
64-bit mode, but IIRC LLVM generates betweer sequences with -mattr=alu32,
under which it will just use w3 (as the type should be optimized into
32-bit) for the comparison.

So, I guess this testcase could have easier sequence for verifier under
ALU32 mode. But for this case, BPF_END is used which doesn't have
sub-register code-gen support inside LLVM for be16 and be32 at the moment
(noticed this several days ago when doing some other benchmarking).

If I have .i file, I could do a quick prototype to see if ALU32 could
improve this.

Regards,
Jiong

Simon
 


35: (69) r3 = *(u16 *)(r7 +38)
36: (dc) r3 = be16 r3
r3 get the value from memory, its value could be any one as permitted
by the type.

Does it mean that r3 is considered as be16 ? I do not understand why as I explicitly convert it in u16.

This output language is a readable format of bpf bytecode, right ? Is there any documentation to lean/understand it ? 

The compiler does the right thing, just verifier is not advanced enough.
Is it worthy to share this issue of verifier.c with bpf maintainers ? The compiler which is used here is clang which is called by bcc, right ?

Yes, you will need some source workaround. You could try below (untested):
+ udp_len = udp_len & 0x1ff;

I tested it and it seems to work. Thx a lot !!

But that means I can not use the u16 max value ?

Yonghong Song
 

On Fri, Mar 8, 2019 at 9:22 AM Simon <contact@...> wrote:


35: (69) r3 = *(u16 *)(r7 +38)
36: (dc) r3 = be16 r3

r3 get the value from memory, its value could be any one as permitted
by the type.

Does it mean that r3 is considered as be16 ? I do not understand why as I explicitly convert it in u16.
The be16 is to convert r3 with big endian encoding. If the host system
is big endian, it will do nothing. Otherwise,
it will convert from little endian to big endian.


This output language is a readable format of bpf bytecode, right ? Is there any documentation to lean/understand it ?
Yes, there is no documentation. It intends to be self explanatory. I
guess "be16" is special and may need some documentation. Otherwise
assembly-style codes should be easy to understand.


The compiler does the right thing, just verifier is not advanced enough.

Is it worthy to share this issue of verifier.c with bpf maintainers ? The compiler which is used here is clang which is called by bcc, right ?
I am also a regular kernel/bpf reviewer. The bpf maintainers/community
are aware of this limitation. As you mentioned, the verifier is
already very complex. To implement complex tracking like described in
this thread will make verifier even more complex, hence this is
delayed. One of reason is that we have reasonable, although
unpleasant, workarounds.

Yes, it is compiled with clang.


Yes, you will need some source workaround. You could try below (untested):
+ udp_len = udp_len & 0x1ff;

I tested it and it seems to work. Thx a lot !!

But that means I can not use the u16 max value ?
You can. I add that because you have a test to limit the range of the
value to 511.