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 [42]. 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.