Abstract
OpenFlow is a network technology that enables to control network equipment centrally, to realize complicated forwarding of packets and to change network topologies flexibly. In OpenFlow networks, network equipment is separated into OpenFlow switches and OpenFlow controllers. OpenFlow switches do not have controllers that usual network equipment has. OpenFlow controllers control OpenFlow switches. OpenFlow controllers are configured by programs. Therefore, network configurations are realized by software. This kind of software can be created by several kinds of programming languages. NetCore is one of them. The verification method of NetCore programs has been introduced. This method uses Coq, which is a formal proof management system. This method, however, deals with only networks that consist of one OpenFlow switch. This paper proposes a methodology that verifies networks that consist of several OpenFlow switches.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Canini, M., Venzano, D., Perešíni, P., Kostić, D., Rexford, J.: A NICE way to test openflow applications. In: Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (2012)
Garcia, R., Tanter, É., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36(4), 1–44 (2014)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(19), 576–580 (1969)
Kuzniar, M., Peresini, P., Canini, M., Venzano, D., Kostic, D.: A SOFT way for openflow switch interoperability testing. In: Proceedings of the 8th International Conference on Emerging Networking Experiments and Technologies, pp. 265–276 (2012)
McKeown, N., Anderson, T., Balakrishnan, H., Parulker, G., Peterson, L., Rexford, J., Shenker, S., Turner, J.: OpenFlow: enabling innovation in campus networks. SIGCOMM Comput. Commun. Rev. 38(2), 69–74 (2008)
Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and runtime system for network programming languages. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 217–230 (2012)
Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, pp. 163–170 (2014)
Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: Formal Methods in Computer-Aided Design, pp. 145–148 (2013)
Sheard, T., Stump, A., Weirich, S.: Language-based verification will change the world. In: Proceedings of the FSE/SDP Workshop on the Future of Sofware Engineering Research, pp. 343–348 (2010)
Siek, J., Taha, W.: Gradual typing for functional languages. In: Proceedings of the Scheme and Functional Programming Workshop, pp. 81–92, September 2006
Stewart, G.: Computational verification of network programs in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 33–49. Springer, Heidelberg (2013)
Tanter, É., Tabareau, N.: Gradual certified programming in Coq. In: Proceedings of the 11th Symposium on Dynamic Languages, pp. 26–40 (2015)
Ball, T., Bjørner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: VeriCon: towards verifying controller programs in software-defined networks. SIGPLAN Not. 49(6), 282–293 (2014). PLDI 2014
Wu, Y., Haeberlen, A., Zhou, W., Loo, B.T.: Answering why-not queries in software-defined networks with negative provenance. In: Proceedings of the Twelfth ACM Workshop on Hot Topics in Networks, pp. 1–7 (2013)
Wundsam, A., Levin, D., Seetharaman, S., Feldmann, A.: OFRewind: enabling record and replay troubleshooting for networks. In: Proceedings of the USENIX Annual Technical Conference (2011)
The Coq Proof Assistant. https://coq.inria.fr
Haskell. https://www.haskell.org
NEC: “Trema Openflow Controller”. http://trema.github.com/trema/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
A Appendix (Program that Does Not Generate Looping Packets)
B Appendix (Program that Generates Looping Packets)
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Date, H., Yoshiura, N. (2016). Computational Verification of Network Programs for Several OpenFlow Switches in Coq. In: Gervasi, O., et al. Computational Science and Its Applications – ICCSA 2016. ICCSA 2016. Lecture Notes in Computer Science(), vol 9787. Springer, Cham. https://doi.org/10.1007/978-3-319-42108-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-42108-7_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42107-0
Online ISBN: 978-3-319-42108-7
eBook Packages: Computer ScienceComputer Science (R0)