Document Open Access Logo

WNetKAT: A Weighted SDN Programming and Verification Language

Authors Kim G. Larsen, Stefan Schmid, Bingtian Xue

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2016.18.pdf
  • Filesize: 0.55 MB
  • 18 pages

Document Identifiers

Author Details

Kim G. Larsen
Stefan Schmid
Bingtian Xue

Cite AsGet BibTex

Kim G. Larsen, Stefan Schmid, and Bingtian Xue. WNetKAT: A Weighted SDN Programming and Verification Language. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.OPODIS.2016.18

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.
Keywords
  • Software-Defined Networking
  • Verification
  • Reachability
  • Stateful Processing
  • Service Chains
  • Weighted Automata
  • Decidability
  • NetKAT

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: Semantic Foundations for Networks. SIGPLAN Not., 49(1), January 2014. URL: http://dx.doi.org/10.1145/2578855.2535862.
  2. Ryan Beckett, Michael Greenberg, and David Walker. Temporal NetKAT. In Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 386-401, 2016. Google Scholar
  3. Giuseppe Bianchi, Marco Bonola, Antonio Capone, and Carmelo Cascone. OpenState: Programming Platform-independent Stateful Openflow Applications Inside the Switch. SIGCOMM Comput. Commun. Rev., 44(2), April 2014. Google Scholar
  4. Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. P4: Programming Protocol-independent Packet Processors. SIGCOMM CCR, 44(3):87-95, 2014. URL: http://dx.doi.org/10.1145/2656877.2656890.
  5. Kenneth L. Calvert, Samrat Bhattacharjee, Ellen Zegura, and James Sterbenz. Directions in active networks. Communications Magazine, IEEE, 36(10):72-78, 1998. Google Scholar
  6. Manfred Droste and Paul Gastin. Weighted automata and weighted logics. In Proc. ICALP, 2005. Google Scholar
  7. Manfred Droste and Doreen Götze. The support of nested weighted automata. In Proc. Workshop on Non-Classical Models for Automata and Applications - (NCMA), 2013. Google Scholar
  8. Manfred Droste and Doreen Heusel. The supports of weighted unranked tree automata. Fundam. Inform., 2015. Google Scholar
  9. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of weighted automata. Springer Science &Business Media, 2009. Google Scholar
  10. Seyed K. Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese. Efficient network reachability analysis using a succinct control plane representation. In Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 217-232, 2016. Google Scholar
  11. Nick Feamster, Jennifer Rexford, and Ellen Zegura. The Road to SDN. Queue, 11(12):20:20-20:40, December 2013. Google Scholar
  12. Andrew D. Ferguson, Arjun Guha, Chen Liang, Rodrigo Fonseca, and Shriram Krishnamurthi. Participatory Networking: An API for Application Control of SDNs. In Proc. ACM SIGCOMM, pages 327-338, 2013. Google Scholar
  13. Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, and David Walker. Frenetic: A network programming language. In Proc. 16th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 279-291, 2011. Google Scholar
  14. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic netkat. In Proc. ESOP, 2016. Google Scholar
  15. Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for NetKAT. In ACM SIGPLAN Notices, 2015. Google Scholar
  16. Sushant Jain, Alok Kumar, Subhasree Mandal, Joon Ong, Leon Poutievski, Arjun Singh, Subbaiah Venkata, Jim Wanderer, Junlan Zhou, Min Zhu, Stephen Stuart Jonathan Zolla, Urs Hölzle, and Amin Vahdat. B4: Experience with a Globally-deployed Software Defined WAN. SIGCOMM Comput. Commun. Rev., 43(4), 2013. URL: http://dx.doi.org/10.1145/2486001.2486019.
  17. Wolfgang John, Konstantinos Pentikousis, George Agapiou, Eduardo Jacob, Mario Kind, Antonio Manzalini, Fulvio Risso, Dimitri Staessens, Rebecca Steinert, and Catalin Meirosu. Research directions in network service chaining. In Proc. IEEE SDN for Future Networks and Services, 2013. URL: http://dx.doi.org/10.1109/SDN4FNS.2013.6702549.
  18. Garvit Juniwal, Nikolaj Bjorner, Ratul Mahajan, Sanjit Seshia, and George Varghese. Quantitative network analysis. Technical Report, 2016. Google Scholar
  19. Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In Proc. USENIX NSDI, 2012. Google Scholar
  20. Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. Veriflow: Verifying network-wide invariants in real time. In Proc. USENIX NSDI, 2013. Google Scholar
  21. Daniel Kirsten. The support of a recognizable series over a zero-sum free, commutative semiring is recognizable. In Developments in Language Theory, 13th International Conference, DLT 2009, Stuttgart, Germany, June 30 - July 3, 2009. Proceedings, pages 326-333, 2009. Google Scholar
  22. Daniel Kirsten and Karin Quaas. Recognizability of the support of recognizable series over the semiring of the integers is undecidable. Inf. Process. Lett., 111(10):500-502, 2011. Google Scholar
  23. Turgay Korkmaz and Marwan Krunz. Multi-constrained optimal path selection. In Proc. IEEE INFOCOM 2001, volume 2, pages 834-843, 2001. Google Scholar
  24. Dexter Kozen. Kleene algebra with tests and commutativity conditions. Springer, 1996. Google Scholar
  25. Kim G. Larsen, Stefan Schmid, and Bingtian Xue. WNetKAT: A Weighted SDN Programming and Verification Language. In ArXiv technical report 1608.08483, 2016. Google Scholar
  26. Tamas Lukovszki and Stefan Schmid. Online admission control and embedding of service chains. In Proc. SIROCCO, 2015. Google Scholar
  27. Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P. Brighten Godfrey, and Samuel Talmadge King. Debugging the data plane with anteater. In Proc. ACM SIGCOMM, 2011. URL: http://dx.doi.org/10.1145/2018436.2018470.
  28. Christopher Monsanto, Nate Foster, Rob Harrison, and David Walker. A compiler and run-time system for network programming languages. In ACM SIGPLAN Notices, 2012. Google Scholar
  29. Christopher Monsanto, Joshua Reich, Nate Foster, Jennifer Rexford, and David Walker. Composing software-defined networks. In Proc. USENIX NSDI, pages 1-14, 2013. Google Scholar
  30. Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, and Sharon Shoham. Decentralizing SDN policies. In ACM SIGPLAN Notices, 2015. Google Scholar
  31. M. Paredes-Farrera, M. Fleury, and M. Ghanbari. Router response to traffic at a bottleneck link. In Proc. TRIDENTCOM, 2006. Google Scholar
  32. Liron Schiff, Michael Borokhovich, and Stefan Schmid. Reclaiming the brain: Useful openflow functions in the data plane. In Proc. ACM HotNets, 2014. Google Scholar
  33. Liron Schiff, Petr Kuznetsov, and Stefan Schmid. In-Band Synchronization for Distributed SDN Control Planes. Proc. ACM SIGCOMM CCR, 2016. Google Scholar
  34. Cole Schlesinger, Hitesh Ballani, Thomas Karagiannis, and Dimitrios Vytiniotis. Quality of service abstractions for software-defined networks. Technical Report, 2016. Google Scholar
  35. David Schneider. The microsecond market. In Proc. IEEE Spectrum, 2012. Google Scholar
  36. Justine Sherry, Shaddi Hasan, Colin Scott, Arvind Krishnamurthy, Sylvia Ratnasamy, and Vyas Sekar. Making middleboxes someone else’s problem: Network processing as a cloud service. In Proc. ACM SIGCOMM 2012, 2012. URL: http://dx.doi.org/10.1145/2342356.2342359.
  37. Ankit Singla, Balakrishnan Chandrasekaran, P. Brighten Godfrey, and Bruce Maggs. The internet at the speed of light. In Proc. ACM HotNets-XIII, 2014. Google Scholar
  38. Jonathan M. Smith and Scott M. Nettles. Active networking: one view of the past, present, and future. Proc. IEEE Transactions on Systems, Man, and Cybernetics: Applications and Reviews, 34(1):4-18, 2004. Google Scholar
  39. Robert Soulé, Shrutarshi Basu, Parisa Jalili Marandi, Fernando Pedone, Robert Kleinberg, Emin Gun Sirer, and Nate Foster. Merlin: A language for provisioning network resources. In Proc. ACM CoNEXT, pages 213-226, 2014. Google Scholar
  40. Richard E. Stearns and Harry B. Hunt. On the equivalence and containment problems for unambiguous regular expressions, grammars, and automata. In Proc. 22nd Annual Symposium on Foundations of Computer Science (SFCS), 1981. Google Scholar
  41. Renata Teixeira, Keith Marzullo, Stefan Savage, and Geoffrey M. Voelker. Characterizing and measuring path diversity of internet topologies. In ACM SIGMETRICS PER, 2003. URL: http://dx.doi.org/10.1145/885651.781069.
  42. Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, and Sharon Shoham. Some complexity results for stateful network verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2016. Google Scholar
  43. Andreas Voellmy, Ashish Agarwal, and Paul Hudak. Nettle: Functional reactive programming for openflow networks. Technical report, Yale University, 2010. Google Scholar
  44. Andreas Voellmy, Junchang Wang, Y Richard Yang, Bryan Ford, and Paul Hudak. Maple: simplifying SDN programming using algorithmic policies. In SIGCOMM CCR, 2013. URL: http://dx.doi.org/10.1145/2534169.2486030.
  45. Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu. Formally verifiable networking. Proc. ACM HotNets, 2009. Google Scholar
  46. Wenxuan Zhou, Dong Jin, Jason Croft, Matthew Caesar, and P. Brighten Godfrey. Enforcing customizable consistency properties in software-defined networks. In Proc. USENIX NSDI, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact