Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computational Science and Its Applications

ICCSA 2016: Computational Science and Its Applications – ICCSA 2016 pp 223–238Cite as

Computational Verification of Network Programs for Several OpenFlow Switches in Coq

  • Conference paper
  • First Online:

  • 1489 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9787))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. 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)

    Google Scholar 

  2. Garcia, R., Tanter, É., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36(4), 1–44 (2014)

    Article  Google Scholar 

  3. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(19), 576–580 (1969)

    Article  MATH  Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Article  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Google Scholar 

  8. Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: Formal Methods in Computer-Aided Design, pp. 145–148 (2013)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. Siek, J., Taha, W.: Gradual typing for functional languages. In: Proceedings of the Scheme and Functional Programming Workshop, pp. 81–92, September 2006

    Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Tanter, É., Tabareau, N.: Gradual certified programming in Coq. In: Proceedings of the 11th Symposium on Dynamic Languages, pp. 26–40 (2015)

    Google Scholar 

  13. 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

    Article  Google Scholar 

  14. 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)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. The Coq Proof Assistant. https://coq.inria.fr

  17. Haskell. https://www.haskell.org

  18. NEC: “Trema Openflow Controller”. http://trema.github.com/trema/

Download references

Author information

Authors and Affiliations

  1. Department of Information and Computer Sciences, Saitama University, 255, Shimo-ookubo, Sakura-ku, Saitama, Japan

    Hiroaki Date & Noriaki Yoshiura

Authors
  1. Hiroaki Date
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Noriaki Yoshiura
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Noriaki Yoshiura .

Editor information

Editors and Affiliations

  1. University of Perugia , Perugia, Italy

    Osvaldo Gervasi

  2. University of Basilicata , Potenza, Italy

    Beniamino Murgante

  3. Covenant University , Ota, Nigeria

    Sanjay Misra

  4. University of Minho , Braga, Portugal

    Ana Maria A.C. Rocha

  5. Polytechnic University , Bari, Italy

    Carmelo M. Torre

  6. Monash University , Clayton, Victoria, Australia

    David Taniar

  7. Kyushu Sangyo University , Fukuoka, Japan

    Bernady O. Apduhan

  8. Saint Petersburg State University , Saint Petersburg, Russia

    Elena Stankova

  9. Beijing University of Posts & Telecommunication , Beijing, China

    Shangguang Wang

Appendices

A Appendix (Program that Does Not Generate Looping Packets)

figure d

B Appendix (Program that Generates Looping Packets)

figure e

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation