Loading...
Thumbnail Image
Item

Identifying equivalent SDN forwarding behaviour

Abstract
Software-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.
Type
Conference Contribution
Type of thesis
Series
Citation
Sanger, 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.3314347
Date
2019
Publisher
ACM
Degree
Supervisors
Rights
© 2019 copyright with the authors.