Automatically verifying reachability and well-formedness in P4 Networks

P4 allows a new level of dynamism for routers beyond OpenFlow 1.4 by allowing headers and tables to
be modified by software in the field. Without care, P4 can unleash a new wave of software bugs. Existing tools (e.g., VeriFlow, NetPlumber, Hassel, NoD) cannot model changes to forwarding behaviors without reprogramming tool internals or having users manually add new forwarding models. Further, a P4 network can introduce a new class of bugs (not tested for by existing tools) wherein the P4 network creates malformed packets.

To attack these two problems, we provide an operational semantics for P4 constructs and use it to compile P4 to Datalog so that the verification model can be automatically updated as the network changes. We demonstrate this vision by compiling the mTag example in the P4 specification
(and a new sTag security example) on a sample network and by automatically detecting forwarding bugs. Efficiently verifying (across all table entries and packet headers) that a P4 network only delivers well-formed packets takes a few seconds.