Arjun Guha
Nate Foster
Abstract
In many areas of computing, techniques ranging from testing to formal modeling to full-blown verification have been successfully used to help programmers build reliable systems. But although networks are critical infrastructure, they have largely resisted analysis using formal techniques. Software-defined networking (SDN) is a new network architecture that has the potential to provide a foundation for network reasoning, by standardizing the interfaces used to express network programs and giving them a precise semantics.
This paper describes the design and implementation of the first machine-verified SDN controller. Starting from the foundations, we develop a detailed operational model for OpenFlow (the most popular SDN platform) and formalize it in the Coq proof assistant. We then use this model to develop a verified compiler and run-time system for a high-level network programming language. We identify bugs in existing languages and tools built without formal foundations, and prove that these bugs are absent from our system. Finally, we describe our prototype implementation and our experiences using it to build practical applications.
- E. Al-Shaer and S. Al-Haj. FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures. In SafeConfig, 2010. Google Scholar
Digital Library
- A. W. Appel. Verified software toolchain. In ESOP, 2011. Google ScholarDigital Library
- M. Canini, D. Venzano, P. Peresíni, D. Kostić, and J. Rexford. A NICE way to test OpenFlow applications. In NSDI, 2012. Google ScholarDigital Library
- chen:coolaidX. Chen, Y. Mao, Z. M. Mao, and J. van der Merwe. Declarative configuration managaement for complex and dynamic networks. In CoNEXT, 2010. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, 2011. Google ScholarDigital Library
- A. D. Ferguson, A. Guha, C. Liang, R. Fonseca, and S. Krishnamurthi. Hierarchical policies for software defined networks. In HotSDN, 2012. Google ScholarDigital Library
- N. Foster, R. Harrison, M. J. Freedman, C. Monsanto, J. Rexford, A. Story, and D. Walker. Frenetic: A network programming language. In ICFP, 2011. Google ScholarDigital Library
- P. Gill, N. Jain, and N. Nagappan. Understanding network failures in data centers: measurement, analysis, and implications. In SIGCOMM, 2011. Google ScholarDigital Library
- N. Handigol, B. Heller, V. Jeyakumar, B. Lantz, and N. McKeown. Reproducible network experiments using container-based emulation. In CoNEXT, 2012. Google ScholarDigital Library
- T. L. Hinrichs, N. S. Gude, M. Casado, J. C. Mitchell, and S. Shenker. Practical declarative network management. In phWREN, 2009. Google ScholarDigital Library
- T. Hoare. The verifying compiler: A grand challenge for computing research. JACM, 50 (1): 63--69, Jan 2003. Google ScholarDigital Library
- P. Kazemian, G. Varghese, and N. McKeown. Header space analysis: Static checking for networks. In NSDI, 2012. Google ScholarDigital Library
- A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. B. Godfrey. Veriflow: Verifying network-wide invariants in real time. In NSDI, 2013. Google ScholarDigital Library
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. sel4: Formal verification of an OS kernel. In SOSP, 2009. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. CACM, 52 (7): 107--115, Jul 2009. Google ScholarDigital Library
- A. Madhavapeddy, R. Mortier, C. Rotsos, D. Scott, B. Singh, T. Gazagnaire, S. Smith, S. Hand, and J. Crowcroft. Unikernels: Library operating systems for the cloud. In ASPLOS, 2013. Google ScholarDigital Library
- H. Mai, A. Khurshid, R. Agarwal, M. Caesar, P. B. Godfrey, and S. T. King. Debugging the data plane with Anteater. In SIGCOMM, 2011. Google ScholarDigital Library
- G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky. Towards a verified relational database management system. In POPL, 2010. Google ScholarDigital Library
- A. Markopoulou, G. Iannaccone, S. Bhattacharyya, C.-N. Chuah, Y. Ganjali, and C. Diot. Characterization of failures in an operational IP backbone network. IEEE/ACM Transactions on Networking, 16 (4): 749--762, Aug 2008. Google ScholarDigital Library
- A. McCreight, T. Chevalier, and A. Tolmach. A certified framework for compiling and executing garbage-collected languages. In ICFP, 2010. 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. SIGCOMM CCR, 38 (2): 69--74, 2008. Google ScholarDigital Library
- C. Monsanto, N. Foster, R. Harrison, and D. Walker. A compiler and run-time system for network programming languages. In POPL, 2012. Google ScholarDigital Library
- G. Morrisett, G. Tan, J. Tassarotti, J.-B. Tristan, and E. Gan. RockSalt: Better, faster, stronger SFI for the x86. In phPLDI, 2012. Google ScholarDigital Library
- R. C. Scott, A. Wundsam, K. Zarifis, and S. Shenker. What, Where, and When: Software Fault Localization for SDN. Technical Report UCB/EECS-2012--178, EECS Department, University of California, Berkeley, 2012.Google Scholar
- P.-Y. Strub, N. Swamy, C. Fournet, and J. Chen. Self-certification: Bootstrapping certified typecheckers in F* with Coq. In POPL, 2012. Google ScholarDigital Library
- A. Tootoonchian, S. Gorbunov, Y. Ganjali, M. Casado, and R. Sherwood. On controller performance in software-defined networks. In HotICE, 2012. Google ScholarDigital Library
- A. Voellmy and P. Hudak. Nettle: Functional reactive programming of OpenFlow networks. In PADL, 2011.Google Scholar
- A. Wang, L. Jia, C. Lio, B. T. Loo, O. Sokolsky, and P. Basu. Formally verifiable networking. In HotNets, 2009.Google Scholar
- G. G. Xie, J. Zhan, D. A. Maltz, H. Zhang, A. G. Greenberg, G. Hjálmtýsson, and J. Rexford. On static reachability analysis of IP networks. In phINFOCOM, 2005.Google Scholar
- Z. Yin, M. Caesar, and Y. Zhou. Towards understanding bugs in open source router software. In SIGCOMM CCR, 2010. Google ScholarDigital Library
- W. Young. Verified compilation in micro-Gypsy. In TAV, 1989. Google ScholarDigital Library
- H. Zeng, P. Kazemian, G. Varghese, and N. McKeown. Automatic test packet generation. In CoNEXT, 2012. Google ScholarDigital Library
- J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In POPL, 2012. Google ScholarDigital Library
Index Terms
- Machine-verified network controllers
Recommendations
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 ...
Machine-verified network controllers
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationIn many areas of computing, techniques ranging from testing to formal modeling to full-blown verification have been successfully used to help programmers build reliable systems. But although networks are critical infrastructure, they have largely ...
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 ...
Comments