Ahmed Khurshid
ABSTRACT
Networks are complex and prone to bugs. Existing tools that check configuration files and data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise.
Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a preliminary design, VeriFlow, which suggests that this goal is achievable. VeriFlow is a layer between a software-defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted. Based on an implementation using a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion.
Supplemental Material
- Mininet: Rapid prototyping for software defined networks. http://yuba.stanford.edu/foswiki/bin/view/OpenFlow/Mininet.Google Scholar
- OpenFlow switch specification. http://www.openflow.org/documents/openflow-spec-v1.1.0.pdf.Google Scholar
- Rocketfuel: An ISP topology mapping engine. http://www.cs.washington.edu/research/networking/rocketfuel/.Google Scholar
- University of Oregon Route Views Project. http://www.routeviews.org/.Google Scholar
- Al-Shaer, E., and Al-Haj, S. FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures. In SafeConfig (2010). Google ScholarDigital Library
- Al-Shaer, E., Marrero, W., El-Atawy, A., and ElBadawi, K. Network configuration in a box: Towards end-to-end verification of network reachability and security. In ICNP (2009).Google Scholar
- Canini, M., Venzano, D., Peresini, P., Kostic, D., and Rexford, J. A NICE way to test OpenFlow applications. In NSDI (2012). Google ScholarDigital Library
- Feamster, N., and Balakrishnan, H. Detecting BGP configuration faults with static analysis. In NSDI (2005). Google ScholarDigital Library
- Foster, N., Harrison, R., Freedman, M. J., Monsanto, C., Rexford, J., Story, A., and Walker, D. Frenetic: A network programming language. In ICFP (2011). Google ScholarDigital Library
- Gude, N., Koponen, T., Pettit, J., Pfaff, B., Casado, M., McKeown, N., and Shenker, S. NOX: Towards an operating system for networks. In SIGCOMM CCR (2008). Google ScholarDigital Library
- Kazemian, P., Varghese, G., and McKeown, N. Header space analysis: Static checking for networks. In NSDI (2012). Google ScholarDigital Library
- Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P. B., and King, S. T. Debugging the data plane with Anteater. In SIGCOMM (2011). Google ScholarDigital Library
- McKeown, N., Anderson, T., Balakrishnan, H., Parulkar, G., Peterson, L., Rexford, J., and Shenker, S. OpenFlow: Enabling innovation in campus networks. In SIGCOMM CCR (2008). Google ScholarDigital Library
- Reitblatt, M., Foster, N., Rexford, J., and Walker, D. Consistent updates for software-defined networks: Change you can believe in! In HotNets (2011). Google ScholarDigital Library
- Sherwood, R., Gibb, G., Yap, K.-K., Appenzeller, G., Casado, M., McKeown, N., and Parulkar, G. Can the production network be the testbed? In OSDI (2010). Google ScholarDigital Library
- Tavakoli, A., Casado, M., Koponen, T., and Shenker, S. Applying NOX to the datacenter. In HotNets (2009).Google Scholar
- Varghese, G. Network Algorithmics: An interdisciplinary approach to designing fast networked devices, 2004. Google ScholarDigital Library
- Yuan, L., Mai, J., Su, Z., Chen, H., Chuah, C.-N., and Mohapatra, P. FIREMAN: A toolkit for firewall modeling and analysis. In IEEE SnP (2006). Google ScholarDigital Library
Index Terms
- VeriFlow: verifying network-wide invariants in real time
Recommendations
Veriflow: verifying network-wide invariants in real time
Special october issue SIGCOMM '12Networks are complex and prone to bugs. Existing tools that check configuration files and data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise.
Is it possible to check network-wide ...
VeriFlow: verifying network-wide invariants in real time
nsdi'13: Proceedings of the 10th USENIX conference on Networked Systems Design and ImplementationNetworks are complex and prone to bugs. Existing tools that check network configuration files and the data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise.
Is it possible to check network-...
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