WNetKAT: A Weighted SDN Programming and Verification Language

Publication: Research - peer-reviewArticle in proceeding

Abstract

Programmability and verifiability lie at the heart of the software-defined networking paradigm. While
OpenFlow and its match-action concept provide primitive operations to manipulate hardware configurations,
over the last years, several more expressive network programming languages have been developed.
This paper presents WNetKAT, the first network programming language accounting for the fact that networks
are inherently weighted, and communications subject to capacity constraints (e.g., in terms of
bandwidth) and costs (e.g., latency or monetary costs). WNetKAT is based on a syntactic and semantic
extension of the NetKAT algebra. We demonstrate several relevant applications for WNetKAT, including
cost- and capacity-aware reachability, as well as quality-of-service and fairness aspects. These applications
do not only apply to classic, splittable and unsplittable (s, t)-flows, but also generalize to more
complex (and stateful) network functions and service chains. For example, WNetKAT allows to model
flows which need to traverse certain waypoint functions, which can change the traffic rate. This paper
also shows the relationship between the equivalence problem of WNetKAT and the equivalence problem
of the weighted finite automata, which implies undecidability of the former. However, this paper
also shows the decidability of whether an expression equals to 0, which is sufficient in many practical
scenarios, and we initiate the discussion of decidable subsets of the whole language.
Close

Details

Programmability and verifiability lie at the heart of the software-defined networking paradigm. While
OpenFlow and its match-action concept provide primitive operations to manipulate hardware configurations,
over the last years, several more expressive network programming languages have been developed.
This paper presents WNetKAT, the first network programming language accounting for the fact that networks
are inherently weighted, and communications subject to capacity constraints (e.g., in terms of
bandwidth) and costs (e.g., latency or monetary costs). WNetKAT is based on a syntactic and semantic
extension of the NetKAT algebra. We demonstrate several relevant applications for WNetKAT, including
cost- and capacity-aware reachability, as well as quality-of-service and fairness aspects. These applications
do not only apply to classic, splittable and unsplittable (s, t)-flows, but also generalize to more
complex (and stateful) network functions and service chains. For example, WNetKAT allows to model
flows which need to traverse certain waypoint functions, which can change the traffic rate. This paper
also shows the relationship between the equivalence problem of WNetKAT and the equivalence problem
of the weighted finite automata, which implies undecidability of the former. However, this paper
also shows the decidability of whether an expression equals to 0, which is sufficient in many practical
scenarios, and we initiate the discussion of decidable subsets of the whole language.
Original languageEnglish
Title of host publication20th International Conference on Principles of Distributed Systems (OPODIS)
PublisherSchloss Dagstuhl. Leibniz-Zentrum für Informatik
Publication date2017
ISBN (print)978-3-95977-031-6
StatePublished - 2017
Event20th International Conference on Principles of Distributed Systems (OPODIS) - Madrid, Spain

Conference

Conference20th International Conference on Principles of Distributed Systems (OPODIS)
Nummer20th
LandSpain
ByMadrid
Periode13/12/201616/12/2016
Internetadresse
SeriesLeibniz International Proceedings in Informatics
Number70
ISSN1868-8969
ID: 249325429