search

p4lang / switch

Consolidated switch repo (API, SAI and Nettlink)
151 stars 72 forks source link

Possible bug in tunnel encapsulation code of switch.p4 #97

Open jafingerhut opened 7 years ago

jafingerhut commented 7 years ago

There seems to be a bug in switch.p4 involving many cases of adding tunnel encapsulation headers.

An example of how switch.p4 code typically does this is given in action inner_ipv4_udp_rewrite, which appears to be a processing step done before the actual new outer headers are filled in.

https://github.com/p4lang/switch/blob/master/p4src/tunnel.p4#L943-L945

That action is one of several similar ones with the same issue, invoked from table tunnel_encap_process_inner, applied inside of control block process_tunnel_encap:

https://github.com/p4lang/switch/blob/master/p4src/tunnel.p4#L1537

That action "pushes down" the outer IPv4 and UDP header (this action should probably only be invoked if the incoming packet had a valid IPv4 and UDP header), copying the header ipv4 over the contents of inner_ipv4, and the header udp over the contents of inner_udp.

That looks good to me, except if inner_ipv4 and/or inner_udp were already valid headers before the action was invoked. That can happen if the incoming packet was already tunnel-encapsulated by an upstream router, but the outer IP destination address is not one that causes decapsulation in this router, but instead causes the packet to be encapsulated into another IP tunnel.

In that case, the statement copy_header(inner_ipv4, ipv4) will overwrite a valid inner_ipv4 value, and the original contents of that header will be lost. The packet sent out will not be a tunnel-encapsulated version of the packet received.

If this is a bug, there doesn't appear to be a small fix. One approach that sounds like a clean fix would be to introduce new "outer_" versions of headers, e.g. outer_ipv4, outer_ipv6, outer_udp, etc. These would never be extracted by the parser. They would be made valid by the tunnel encapsulation code, which would no longer use this "pushing down" technique that it does now. The new "outer" headers would be emitted in an appropriate order in the deparser, before the existing headers.

jafingerhut commented 5 years ago

In a conversation with one of the authors of the paper "Uncovering Bugs in P4 Programs with Assertion-based Verification" published at the ACM SOSR 2018 conference, he mentioned that they had confirmed this is a bug in this open source implementation of switch.p4.

Authors (in case it helps someone else find this paper later): Lucas Freire, Miguel Neves, Lucas Leal, and Alberto Schaeffer-Filho (UFRGS), Kirill Levchenko (UC San Diego), Marinho Barcellos (UFRGS)

https://conferences.sigcomm.org/sosr/2018/program.html