Abstract
Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specification of correctness criteria. However, the recent move towards Software Defined Networking (SDN) provides a clean separation between a centralized control plane and a distributed data plane. This provides an opportunity to formally verify critical data plane properties. In this paper, we present a Boolean Satisfiability (SAT) based framework for data plane modeling and checking of key correctness criteria. This provides greater efficiency and/or greater coverage of properties when compared to other existing approaches.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Kerravala, Z.: As the value of enterprise networks escalates, so does the need for configuration management. Technical report, Yankee Group (2004)
Xie, G., Zhan, J., Maltz, D., Zhang, H., Greenberg, A., Hjalmtysson, G., Rexford, J.: On static reachability analysis of ip networks. In: Proceedings IEEE 24th Annual Joint Conference of the IEEE Computer and Communications Societies, INFOCOM 2005, vol. 3, pp. 2170–2183 (March 2005)
Zhang, S., Malik, S., McGeer, R.: Verification of computer switching networks: An overview. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 1–16. Springer, Heidelberg (2012)
McKeown, N., Anderson, T., Balakrishnan, H., Parulkar, G., Peterson, L., Rexford, J., Shenker, S., Turner, J.: Openflow: enabling innovation in campus networks. SIGCOMM Comput. Commun. Rev. 38(2), 69–74 (2008)
Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, NSDI 2012, p. 9. USENIX Association, Berkeley (2012)
Gude, N., Koponen, T., Pettit, J., Pfaff, B., Casado, M., McKeown, N., Shenker, S.: Nox: towards an operating system for networks. SIGCOMM Comput. Commun. Rev. 38(3), 105–110 (2008)
Al-Shaer, E., Al-Haj, S.: Flowchecker: configuration analysis and verification of federated openflow infrastructures. In: Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration, SafeConfig 2010, pp. 37–44. ACM, New York (2010)
Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., David, W.: Abstractions for network update. SIGCOMM Comput. Commun. Rev. (August 2012)
Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with anteater. In: Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM 2011, pp. 290–301. ACM, New York (2011)
Waxman, B.: Routing of multipoint connections. IEEE Journal on Selected Areas in Communications 6(9), 1617–1622 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Zhang, S., Malik, S. (2013). SAT Based Verification of Network Data Planes. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_43
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_43
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)