Dataplane equivalence and its applications

We present the design and implementation of netdiff, an algorithm that uses symbolic execution to check the equivalence of two network dataplanes modeled in SEFL. We use netdiff to find new bugs in Openstack Neutron, to test the differences between related P4 programs and to check the equivalence of FIB updates in a production network. Our evaluation highlights that equivalence is an easy way to find bugs, scales well to relatively large programs and uncovers subtle issues otherwise difficult to find.