skip to main content
10.1145/2676726.2676990acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Decentralizing SDN Policies

Published: 14 January 2015 Publication History

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.

Supplementary Material

MPG File (p663-sidebyside.mpg)

References

[1]
The Open Networking Foundation. http://opennetworking.org.
[2]
OpenFlow Switch Specification, Oct. 2013. Version 1.4.0.
[3]
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.
[4]
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.
[5]
CANINI, M., VENZANO, D., PERES, P., KOSTIC, D., AND REXFORD, J. A NICE Way to Test OpenFlow Applications. In NSDI (2012).
[6]
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.
[7]
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.
[8]
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).
[9]
KAZEMIAN, P., VARGHESE, G., AND MCKEOWN, N. Header Space Analysis: Static Checking For Networks. In NSDI (2012).
[10]
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).
[11]
KUPERSTEIN, M., VECHEV, M. T., AND YAHAV, E. Automatic inference of memory fences. SIGACT News 43, 2 (2012), 108--123.
[12]
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.
[13]
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.
[14]
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.
[15]
REITBLATT, M., FOSTER, N., REXFORD, J., SCHLESINGER, C., AND WALKER, D. Abstractions for network update. In ACM SIGCOMM (2012), pp. 323--334.
[16]
SKOWYRA, R., LAPETS, A., BESTAVROS, A., AND KFOURY, A. A verification platform for sdn-enabled applications. In HiCoNS (2013).
[17]
THECOQ DEVELOPMENT TEAM. The Coq proof assistant reference manual. TypiCal Project (formerly LogiCal), 2012. Version 8.4.
[18]
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.

Cited By

View all
  • (2024)SDN-Based Load Balancing to Achieve Energy Efficiency in Enterprise Networks2024 Global Conference on Wireless and Optical Technologies (GCWOT)10.1109/GCWOT63882.2024.10805670(1-6)Online publication date: 25-Sep-2024
  • (2024)Prenex Universal First-order Safety PropertiesInformation Processing Letters10.1016/j.ipl.2024.106488(106488)Online publication date: Feb-2024
  • (2020)AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTLComputer Aided Verification10.1007/978-3-030-53291-8_5(64-76)Online publication date: 21-Jul-2020
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. distributed systems
  2. logic programming
  3. network programming languages
  4. software-defined networking
  5. synthesis

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)8
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)SDN-Based Load Balancing to Achieve Energy Efficiency in Enterprise Networks2024 Global Conference on Wireless and Optical Technologies (GCWOT)10.1109/GCWOT63882.2024.10805670(1-6)Online publication date: 25-Sep-2024
  • (2024)Prenex Universal First-order Safety PropertiesInformation Processing Letters10.1016/j.ipl.2024.106488(106488)Online publication date: Feb-2024
  • (2020)AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTLComputer Aided Verification10.1007/978-3-030-53291-8_5(64-76)Online publication date: 21-Jul-2020
  • (2019)Model Checking Data Flows in Concurrent Network UpdatesAutomated Technology for Verification and Analysis10.1007/978-3-030-31784-3_30(515-533)Online publication date: 28-Oct-2019
  • (2018)Efficient Loop-Free Rerouting of Multiple SDN FlowsIEEE/ACM Transactions on Networking10.1109/TNET.2018.281064026:2(948-961)Online publication date: 1-Apr-2018
  • (2017)Genesis: synthesizing forwarding tables in multi-tenant networksACM SIGPLAN Notices10.1145/3093333.300984552:1(572-585)Online publication date: 1-Jan-2017
  • (2017)Genesis: synthesizing forwarding tables in multi-tenant networksProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009845(572-585)Online publication date: 1-Jan-2017
  • (2017)Outsmarting Network Security with SDN Teleportation2017 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP.2017.21(563-578)Online publication date: Apr-2017
  • (2017)Synchronization Synthesis for Network ProgramsComputer Aided Verification10.1007/978-3-319-63390-9_16(301-321)Online publication date: 13-Jul-2017
  • (2016)Temporal NetKATACM SIGPLAN Notices10.1145/2980983.290810851:6(386-401)Online publication date: 2-Jun-2016
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media