Oded Padon
Neil Immerman
Aleksandr Karbyshev
Ori Lahav
Abstract
Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" --- software that operates independently of the network hardware. Network operators can run both in-house and third-party SDN programs on top of the controller, e.g., to specify routing and access control policies.
In practice, having the controller handle events limits the network scalability. Therefore, the feasibility of SDN depends on the ability to efficiently decentralize network event-handling by installing forwarding rules on the switches. However, installing a rule too early or too late may lead to incorrect behavior, e.g., (1) packets may be forwarded to the wrong destination or incorrectly dropped; (2) packets handled by the switch may hide vital information from the controller, leading to incorrect forwarding behavior. The second issue is subtle and sometimes missed even by experienced programmers.
The contributions of this paper are two fold. First, we formalize the correctness and optimality requirements for decentralizing network policies. Second, we identify a useful class of network policies which permits automatic synthesis of a controller which performs optimal forwarding rule installation.
Supplemental Material
- The Open Networking Foundation. http://opennetworking.org.Google Scholar
- OpenFlow Switch Specification, Oct. 2013. Version 1.4.0.Google Scholar
- ANDERSON, C. J., FOSTER, N., GUHA, A., JEANNIN, J.-B., KOZEN, D., SCHLESINGER, C., AND WALKER, D. NetKAT: Semantic foundations for networks. In POPL (2014), S. Jagannathan and P. Sewell, Eds., ACM, pp. 113--126. Google ScholarDigital Library
- BALL, T., BJØRNER, N., GEMBER, A., ITZHAKY, S., KARBYSHEV, A., SAGIV, M., SCHAPIRA, M., AND VALADARSKY, A. Vericon: Towards verifying controller programs in software-defined networks. In PLDI (June 2014), SIGPLAN, ACM. Google ScholarDigital Library
- CANINI, M., VENZANO, D., PERES, P., KOSTIC, D., AND REXFORD, J. A NICE Way to Test OpenFlow Applications. In NSDI (2012). Google ScholarDigital Library
- FOSTER, N., GUHA, A., REITBLATT, M., STORY, A., FREEDMAN, M. J., KATTA, N. P., MONSANTO, C., REICH, J., REXFORD, J., SCHLESINGER, C., WALKER, D., AND HARRISON, R. Languages for software-defined networks. IEEE Communications Magazine 51, 2 (2013), 128--134.Google ScholarCross Ref
- HUANG, S. S., GREEN, T. J., AND LOO, B. T. Datalog and emerging applications: an interactive tutorial. In Proceedings of the 2011 ACM SIGMOD International Conference on Management of Data (2011), ACM, pp. 1213--1216. Google ScholarDigital Library
- KATTA, N. P., REXFORD, J., AND WALKER, D. Logic programming for software-defined networks. In ACM SIGPLAN Workshop on Cross- model Language Design and Implementation (Sept. 2012).Google Scholar
- KAZEMIAN, P., VARGHESE, G., AND MCKEOWN, N. Header Space Analysis: Static Checking For Networks. In NSDI (2012). Google ScholarDigital Library
- KOPONEN, T., AMIDON, K., BALLAND, P., CASADO, M., CHANDA, A., FULTON, B., GANICHEV, I., GROSS, J., GUDE, N., INGRAM, P.,JACKSON, E., LAMBETH, A., LENGLET, R., LI, S.-H., PADMANAB-HAN, A., PETTIT, J., PFAFF, B., RAMANATHAN, R., S HENKER, S., SHIEH, A., STRIBLING, J., THAKKAR, P., WENDLANDT, D., YIP, A., AND ZHANG, R. Network virtualization in multi-tenant datacenters. In NSDI (2014). Google ScholarDigital Library
- KUPERSTEIN, M., VECHEV, M. T., AND YAHAV, E. Automatic inference of memory fences. SIGACT News 43, 2 (2012), 108--123. Google ScholarDigital Library
- KUZNIAR, M., PERESINI, P., CANINI, M., VENZANO, D., AND KOSTIC, D. A SOFT Way for OpenFlow Switch Interoperability Testing. In CoNEXT (2012), pp. 265--276. Google ScholarDigital Library
- MONSANTO, C., FOSTER, N., HARRISON, R., AND WALKER, D. A compiler and run-time system for network programming languages. SIGPLAN Not. 47, 1 (Jan. 2012), 217--230. Google ScholarDigital Library
- NELSON, T., FERGUSON, A. D., SCHEER, M. J. G., AND KRISHNA-MURTHI, S. Tierless programming and reasoning for software-defined networks. In NSDI (2014), USENIX Association, pp. 519--531. Google ScholarDigital Library
- REITBLATT, M., FOSTER, N., REXFORD, J., SCHLESINGER, C., AND WALKER , D. Abstractions for network update. In ACM SIGCOMM (2012), pp. 323--334. Google ScholarDigital Library
- SKOWYRA, R., LAPETS, A., BESTAVROS, A., AND KFOURY, A. A verification platform for sdn-enabled applications. In HiCoNS (2013).Google Scholar
- THECOQ DEVELOPMENT TEAM. The Coq proof assistant reference manual. TypiCal Project (formerly LogiCal), 2012. Version 8.4.Google Scholar
- VOELLMY, A., WANG, J., YANG, Y. R., FORD, B., AND HUDAK, P. Maple: simplifying SDN programming using algorithmic policies. In ACM SIGCOMM (2013), pp. 87--98. Google ScholarDigital Library
Index Terms
- Decentralizing SDN Policies
Recommendations
Scenario-based programming for SDN policies
CoNEXT '15: Proceedings of the 11th ACM Conference on Emerging Networking Experiments and TechnologiesRecent emergence of software-defined networks offers an opportunity to design domain-specific programming abstractions aimed at network operators. In this paper, we propose scenario-based programming, a framework that allows network operators to program ...
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot ...
Maple: simplifying SDN programming using algorithmic policies
Software-Defined Networking offers the appeal of a simple, centralized programming model for managing complex networks. However, challenges in managing low-level details, such as setting up and maintaining correct and efficient forwarding tables on ...
Comments