Stephen Gutz
Cole Schlesinger
Nate Foster
ABSTRACT
The correct operation of many networks depends on keeping certain kinds of traffic isolated from others, but achieving isolation in networks today is far from straightforward. To achieve isolation, programmers typically resort to low-level mechanisms such as Virtual LANs, or they interpose complicated hypervisors into the control plane. This paper presents a better alternative: an abstraction that supports programming isolated slices of the network. The semantics of slices ensures that the processing of packets on a slice is independent of all other slices. We define our slice abstraction precisely, develop algorithms for compiling slices, and illustrate their use on examples. In addition, we describe a prototype implementation and a tool for automatically verifying formal isolation properties.
Supplemental Material
- Martí n Casado, Teemu Koponen, Rajiv Ramanathan, and Scott Shenker. Virtualizing the network forwarding plane. In Workshop on Programmable Routers for Extensible Services of Tomorrow (PRESTO), Philadelphia, PA, 2010. Google Scholar
Digital Library
- Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In International Conference on Computer Aided Verification (CAV), Copenhagen, Denmark, pages 359--364, July 2002. Google ScholarDigital Library
- E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244--263, 1986. Google ScholarDigital Library
- N. C. Fernandes and O. C. M. B. Duarte. XNetMon: A network monitor for securing virtual networks. In International Conference on Communications (ICC), Kyoto Japan, pages 1--5, June 2011.Google ScholarCross Ref
- FlowVisor. Bug report, March 2012. See https://openflow.stanford.edu/bugs/browse/FLOWVISOR-171.Google Scholar
- Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, and David Walker. Frenetic: A network programming language. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Tokyo, Japan, pages 279--291, September 2011. Google ScholarDigital Library
- Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), San Jose, CA, April 2012. Google ScholarDigital Library
- Georgia Kontesidou and Kyriakos Zarifis. OpenFlow virtual networking: A flow-based network virtualization. Master's thesis, KTH Royal Institute of Technology, 2009.Google Scholar
- Los Alamos National Laboratory. NetworkX, November 2011. Available from http://networkx.lanl.gov.Google Scholar
- Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, Brighten Godfrey, and Samuel Talmadge King. Debugging the data plane with Anteater. In ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (SIGCOMM), Toronto, Canada, pages 290--301, August 2011. Google ScholarDigital Library
- N. McKeown, T. Anderson, H. Balakrishnan, G. Parulkar, L. Peterson, J. Rexford, S. Shenker, and J. Turner. Openflow: Enabling innovation in campus networks. ACM SIGCOMM Computer Communications Review (CCR), 38(2):69--74, 2008. Google ScholarDigital Library
- Christopher Monsanto, Nate Foster, Rob Harrison, and David Walker. A compiler and run-time system for network programming languages. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, PA, pages 217--230, January 2012. Google ScholarDigital Library
- Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Lisbon, Portugal, pages 151--166, March 1998. Google ScholarDigital Library
- Joshua Reich, Nate Foster, Jennifer Rexford, and David Walker. Toward a language for network virtualization. Draft, April 2012.Google Scholar
- Mark Reitblatt, Nate Foster, Jennifer Rexford, Cole Schlesinger, and David Walker. Abstractions for network update. In ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (SIGCOMM), Helsinki, Finland, August 2012. To appear. Google ScholarDigital Library
- Rob Sherwood, Michael Chan, Adam Covington, Glen Gibb, Mario Flajslik, Nikhil Handigol, Te-Yuan Huang, Peyman Kazemian, Masayoshi Kobayashi, Jad Naous, Srinivasan Seetharaman, David Underhill, Tatsuya Yabe, Kok-Kiong Yap, Yiannis Yiakoumis, Hongyi Zeng, Guido Appenzeller, Ramesh Johari, Nick McKeown, and Guru Parulkar. Carving research slices out of your production networks with openflow. ACM SIGCOMM Computer Communications Review (CCR), 40(1):129--130, January 2010. Google ScholarDigital Library
Index Terms
- Splendid isolation: a slice abstraction for software-defined networks
Recommendations
A compiler and run-time system for network programming languages
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesSoftware-defined networks (SDNs) are a new kind of network architecture in which a controller machine manages a distributed collection of switches by instructing them to install or uninstall packet-forwarding rules and report traffic statistics. The ...
A compiler and run-time system for network programming languages
POPL '12Software-defined networks (SDNs) are a new kind of network architecture in which a controller machine manages a distributed collection of switches by instructing them to install or uninstall packet-forwarding rules and report traffic statistics. The ...
Language support for verifiable SDNs
SPLASH Companion 2016: Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for HumanityProgramming languages for Software-Defined Networks (SDNs) provide higher abstractions on top of hardware-based APIs like OpenFlow. Researchers started to develop SDN programming languages based on mathematical foundations, which makes these languages ...
Comments