Possible bug in tunnel encapsulation code of switch.p4

[jafingerhut]

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]

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