Skip to main content
SpringerLink
Log in

Witnessing Network Transformations

  • Conference paper
  • First Online:
Book cover Runtime Verification (RV 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10548))

Included in the following conference series:

Abstract

Software-defined networking (SDN) is transforming the way networks are managed, as fixed distributed protocols give way to flexible route calculation software. The shift brings to the forefront the issue of software errors, which may produce wrong routes, and cause significant network disruption. We propose a run-time certification mechanism that rejects any wrongly calculated route before it is installed in the network. Certification is done through a strategy called witnessing, where a witness (i.e., a justification) is generated by the software for each routing decision. The witness provided for a route change is validated against the original user request, using a formal network model, before the change is installed on the real network. Witnessing shifts trust away from the complex system software to a relatively simple witness checker. We define a formal language to specify connection-based user requests (“intents”), witnesses for each type of intent, and the checking algorithm. We also formulate a notion of refinement between networks, and show that it preserves the realizability of intents across abstraction levels.

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

Access this chapter

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

Institutional subscriptions

References

  1. ONOS: Open Network Operating System. http://onosproject.org/

  2. Open Daylight. https://www.opendaylight.org/

  3. RFC 6241 - Network Configuration Protocol (NETCONF). https://tools.ietf.org/html/rfc6241

  4. Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273–303 (2001). doi:10.1145/503502.503503

    Article  Google Scholar 

  5. Anderson, C.J., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, January 20–21, 2014, pp. 113–126. ACM (2014). doi:10.1145/2535838.2535862

  6. Canini, M., Venzano, D., Peresíni, P., Kostic, D., Rexford, J.: A NICE way to test openflow applications. In: Gribble and Katabi [11], pp. 127–140. https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/canini

  7. Deng, C., Namjoshi, K.S.: Witnessing network transformations (2017). Extended version of this paper, at http://cs.nyu.edu/~deng/

  8. Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Karp, R. (ed.) Complexity of Computation, SIAM-AMS Proc., pp. 27–41 (1974)

    Google Scholar 

  9. Feamster, N., Rexford, J., Zegura, E.W.: The road to SDN: an intellectual history of programmable networks. Comput. Commun. Rev. 44(2), 87–98 (2014). doi:10.1145/2602204.2602219

    Article  Google Scholar 

  10. Fortune, S.: Equivalence and generalization in a layered network model. J. Comput. Syst. Sci. 81(8), 1698–1714 (2015). doi:10.1016/j.jcss.2015.06.004

    Article  MathSciNet  MATH  Google Scholar 

  11. Gribble, S.D., Katabi, D. (eds.) Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012, San Jose, CA, USA, April 25–27, 2012. USENIX Association (2012). https://www.usenix.org/publications/proceedings/?f[0]=im_group_audience%3A279

  12. Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: Boehm, H., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16–19, 2013, pp. 483–494. ACM (2013). doi:10.1145/2462156.2462178

  13. Kang, N., Liu, Z., Rexford, J., Walker, D.: Optimizing the “one big switch” abstraction in software-defined networks. In: Almeroth, K.C., Mathy, L., Papagiannaki, K., Misra, V. (eds.) Conference on emerging Networking Experiments and Technologies, CoNEXT 2013, Santa Barbara, CA, USA, December 9–12, 2013, pp. 13–24. ACM (2013). doi:10.1145/2535372.2535373

  14. Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: Gribble and Katabi[11], pp. 113–126. https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/kazemian

  15. Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: Veriflow: Verifying network-wide invariants in real time. In: Feamster, N., Mogul, J.C. (eds.) Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, April 2–5, 2013, pp. 15–27. USENIX Association (2013). https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/khurshid

  16. Lopes, N.P., Bjørner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4–6, 2015, pp. 499–512. USENIX Association (2015). https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/lopes

  17. Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, B., King, S.T.: Debugging the data plane with Anteater. In: Keshav, S., Liebeherr, J., Byers, J.W., Mogul, J.C. (eds.) Proceedings of the ACM SIGCOMM 2011 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Toronto, ON, Canada, August 15–19, 2011, pp. 290–301. ACM (2011). doi:10.1145/2018436.2018470

  18. McKeown, N., Anderson, T., Balakrishnan, H., Parulkar, G.M., Peterson, L.L., Rexford, J., Shenker, S., Turner, J.S.: Openflow: enabling innovation in campus networks. Comput. Commun. Rev. 38(2), 69–74 (2008). doi:10.1145/1355734.1355746

    Article  Google Scholar 

  19. Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304–323. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_17

    Chapter  Google Scholar 

  20. Necula, G.: Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI) 2000, pp. 83–95 (2000)

    Google Scholar 

  21. Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: OSDI (1996)

    Google Scholar 

  22. Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool (CVT) - automatic verification of a compilation process. Softw. Tools Technol. Transf. 2(2), 192–201 (1998)

    Article  MATH  Google Scholar 

  23. Rinard, M.C., Marinov, D.: Credible compilation with pointers. In: FLoC Workshop on Run-Time Result Verification (1999)

    Google Scholar 

  24. Shenker, S., Casado, M., Koponen, T., McKeown, N.: The future of networking and the past of protocols. Open Networking Summit (2011)

    Google Scholar 

  25. Simsarian, J.E., Choi, N., Kim, Y.J., Fortune, S., Thottan, M.K.: Netgraph data model applied to multilayer carrier networks. In: OFC (2016). doi:10.1364/OFC.2016.Th4G.2

  26. Smolka, S., Eliopoulos, S.A., Foster, N., Guha, A.: A fast compiler for netkat. In: Fisher, K., Reppy, J.H. (eds.) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1–3, 2015, pp. 328–341. ACM (2015). doi:10.1145/2784731.2784761

  27. Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223–247 (2003)

    Google Scholar 

Download references

Acknowledgements

We wish to thank colleagues at Bell Labs for many helpful comments. Kedar Namjoshi was supported, in part, by NSF grant CCF-1563393 during the preparation of this paper.

Author information

Authors and Affiliations

  1. New York University, New York, USA

    Chaoqiang Deng

  2. Bell Laboratories, Nokia, Murray Hill, USA

    Kedar S. Namjoshi

Authors
  1. Chaoqiang Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kedar S. Namjoshi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kedar S. Namjoshi .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Deng, C., Namjoshi, K.S. (2017). Witnessing Network Transformations. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation