Sanger, RichardLuckie, Matthew JohnNelson, Richard2019-05-0120192019-05-012019Sanger, R., Luckie, M. J., & Nelson, R. (2019). Identifying equivalent SDN forwarding behaviour. In Proceedings of 2019 ACM Symposium on SDN Research (SOSR ’19) (pp. 127–139). New York, NY, USA: ACM. https://doi.org/10.1145/3314148.3314347978-1-4503-6710-3https://hdl.handle.net/10289/12499Software-Defined Networking (SDN) enables network operators the flexibility to program their own forwarding rules, providing more than one way to achieve the same behaviour. Verifying equivalence between rulesets is a fundamental analysis and verification building block for SDN as it can be used to: (1) confirm a ruleset optimised for power efficiency or table occupancy remains equivalent, (2) verify a ruleset modified for new hardware, (3) regression test an SDN application to detect bugs early. We present a practical and novel canonical Multi-Terminal Binary Decision Diagram (MTBDD) representation of OpenFlow 1.3 ruleset forwarding behaviour which can be trivially compared for equivalence. Basing our representation on an MTBDD provides a proven canonical form which is also compact. In this paper, we present the algorithms required to correctly flatten multi-table pipelines into an equivalent single-table, resolve equivalences in OpenFlow actions, and build the final MTBDD representation from a priority ordered ruleset. OpenFlow rulesets can typically be converted to an MTBDD within tens of seconds. We release our opensource implementation to the SDN community.application/pdfen© 2019 copyright with the authors.computer sciencenetworksprogrammable networkcomputing methodologiesmodel verification and validationConference Contribution10.1145/3314148.3314347