Paper Info
Title
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 open-source implementation to the SDN community.
Year
DOI
Venue
2019
10.1145/3314148.3314347
SOSR
Field
DocType
ISBN
Circuit switching,Computer science,Binary decision diagram,Network topology,Canonical form,Regression testing,Equivalence (measure theory),OpenFlow,Operator (computer programming),Distributed computing
Conference
978-1-4503-6710-3
Citations 
PageRank 
References 
0
0.34
0
Authors
3
Name
Order
Citations
PageRank
Richard Sanger131.06
Matthew Luckie239226.34
Richard Nelson341.74