NetKAT — A Formal System for the Verification of Networks

  • Dexter Kozen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


This paper presents a survey of recent work in the development of NetKAT, a formal system for reasoning about packet switching networks, and its role in the emerging area of software-defined networking.


Kleene algebra Kleene algebra with tests NetKAT software defined networking packet switching OpenFlow Frenetic 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Anderson, C.J., Foster, N., Guha, A., Jeannin, J.-B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. In: Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL 2014), San Diego, California, USA, pp. 113–126. ACM (January 2014)Google Scholar
  2. 2.
    Ball, T., Bjorner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: Towards verifying controller programs in software-defined networks. In: PLDI (to appear, 2014)Google Scholar
  3. 3.
    Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proc. 40th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL 2013, pp. 457–468. ACM (2013)Google Scholar
  4. 4.
    Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Logical Methods in Computer Science 8(1:16), 1–42 (2012)MathSciNetGoogle Scholar
  5. 5.
    Canini, M., Venzano, D., Perešíni, P., Kostić, D., Rexford, J.: A NICE way to test OpenFlow applications. In: NSDI (2012)Google Scholar
  6. 6.
    Chen, H., Pucella, R.: A coalgebraic approach to Kleene algebra with tests. Electronic Notes in Theoretical Computer Science 82(1) (2003)Google Scholar
  7. 7.
    Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests. Technical Report TR96-1598, Computer Science Department, Cornell University (July 1996)Google Scholar
  8. 8.
    Ferguson, A.D., Guha, A., Liang, C., Fonseca, R., Krishnamurthi, S.: Participatory networking: An API for application control of SDNs. In: SIGCOMM (2013)Google Scholar
  9. 9.
    Foster, N., Harrison, R., Freedman, M.J., Monsanto, C., Rexford, J., Story, A., Walker, D.: Frenetic: A network programming language. In: ICFP (September 2011)Google Scholar
  10. 10.
    Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. Technical Report, Computing and Information Science, Cornell University (March 2014),, POPL 2015 (to appear)
  11. 11.
    Open Networking Foundation. Software-defined networking: The new norm for networks. White paper (2012),
  12. 12.
    Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: PLDI (June 2013)Google Scholar
  13. 13.
    Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical Report 71-114. University of California (1971)Google Scholar
  14. 14.
    Jain, S., Kumar, A., Mandal, S., Ong, J., Poutievski, L., Singh, A., Venkata, S., Wanderer, J., Zhou, J., Zhu, M., Zolla, J., Hölzle, U., Stuart, S., Vahdat, A.: B4: Experience with a globally-deployed software defined WAN. In: SIGCOMM (2013)Google Scholar
  15. 15.
    Katz-Bassett, E., Scott, C., Choffnes, D.R., Cunha, Í., Valancius, V., Feamster, N., Madhyastha, H.V., Anderson, T., Krishnamurthy, A.: Lifeguard: Practical repair of persistent route failures. In: SIGCOMM (2012)Google Scholar
  16. 16.
    Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: Static checking for networks. In: NSDI (2012)Google Scholar
  17. 17.
    Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: Verifying network-wide invariants in real time. In: NSDI (2013)Google Scholar
  18. 18.
    Kim, H., Feamster, N.: Improving network management with software defined networking. IEEE Communications Magazine 51(2), 114–119 (2013)CrossRefGoogle Scholar
  19. 19.
    Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, pp. 3–41. Princeton University Press, Princeton (1956)Google Scholar
  20. 20.
    Koponen, T., Amidon, K., Balland, P., Casado, M., Chanda, A., Fulton, B., Ganichev, I., Gross, J., Gude, N., Ingram, P., Jackson, E., Lambeth, A., Lenglet, R., Li, S.-H., Padmanabhan, A., Pettit, J., Pfaff, B., Ramanathan, R., Shenker, S., Shieh, A., Stribling, J., Thakkar, P., Wendlandt, D., Yip, A., Zhang, R.: Network virtualization in multi-tenant datacenters. In: NSDI (2014)Google Scholar
  21. 21.
    Koponen, T., Casado, M., Gude, N., Stribling, J., Poutievski, L., Zhu, M., Ramanathan, R., Iwata, Y., Inoue, H., Hama, T., Shenker, S.: Onix: A distributed control platform for large-scale production networks. In: OSDI (2010)Google Scholar
  22. 22.
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput. 110(2), 366–390 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Kozen, D.: Kleene algebra with tests. Transactions on Programming Languages and Systems 19(3), 427–443 (1997)CrossRefGoogle Scholar
  24. 24.
    Kozen, D.: On the coalgebraic theory of Kleene algebra with tests. Technical Report. Computing and Information Science, Cornell University (March 2008),
  25. 25.
    Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  26. 26.
    Loo, B.T., Hellerstein, J.M., Stoica, I., Ramakrishnan, R.: Declarative routing: Extensible routing with declarative queries. In: SIGCOMM (2005)Google Scholar
  27. 27.
    Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with Anteater. In: SIGCOMM (2011)Google Scholar
  28. 28.
    Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: POPL (January 2012)Google Scholar
  29. 29.
    Monsanto, C., Reich, J., Foster, N., Rexford, J., Walker, D.: Composing software-defined networks. In: NSDI (April 2013)Google Scholar
  30. 30.
    Nelson, T., Guha, A., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: A balance of power: Expressive, analyzable controller programming. In: HotSDN (2013)Google Scholar
  31. 31.
    Pous, D.: Relational algebra and KAT in Coq (February 2013),
  32. 32.
    Rutten, J.J.M.M.: Universal coalgebra: A theory of systems. Theoretical Computer Science 249, 3–80 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 194–218. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  34. 34.
    Scott, R.C., Wundsam, A., Zarifis, K., Shenker, S.: What, Where, and When: Software Fault Localization for SDN. Technical Report UCB/EECS-2012-178, EECS Department, University of California, Berkeley (2012)Google Scholar
  35. 35.
    Silva, A.: Kleene Coalgebra. PhD thesis, University of Nijmegen (2010)Google Scholar
  36. 36.
    Voellmy, A., Hudak, P.: Nettle: Functional reactive programming of OpenFlow networks. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 235–249. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  37. 37.
    Voellmy, A., Wang, J., Yang, Y.R., Ford, B., Hudak, P.: Maple: Simplifying SDN programming using algorithmic policies. In: SIGCOMM (2013)Google Scholar
  38. 38.
    Xie, G.G., Zhan, J., Maltz, D.A., Zhang, H., Greenberg, A.G., Hjálmtýsson, G., Rexford, J.: On static reachability analysis of IP networks. In: INFOCOM (2005)Google Scholar
  39. 39.
    Zeng, H., Kazemian, P., Varghese, G., McKeown, N.: Automatic test packet generation. In: CoNEXT (2012)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Dexter Kozen
    • 1
  1. 1.Cornell UniversityIthacaUSA

Personalised recommendations