research-article

NetKAT: semantic foundations for networks

Authors:

Carolyn Jane Anderson,

Jean-Baptiste Jeannin,

Cole Schlesinger,

David WalkerAuthors Info & Claims

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 113 - 126

https://doi.org/10.1145/2535838.2535862

Published: 08 January 2014 Publication History

Abstract

Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code.

This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; union and sequential composition operators; and a Kleene star operator that iterates programs. We show that NetKAT is an instance of a canonical and well-studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability, proving non-interference properties that ensure isolation between programs, and establishing the correctness of compilation algorithms.

Supplementary Material

MP4 File (d1_right_t6.mp4)

Download
184.11 MB

References

[1]

Ehab Al-Shaer and Saeed Al-Haj. FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures. In SafeConfig, 2010.

Digital Library

[2]

Allegra Angus and Dexter Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001--1844, Computer Science Department, Cornell University, July 2001.

Digital Library

[3]

Ernie Cohen. Using Kleene algebra to reason about concurrency control. Technical report, Telcordia, Morristown, N.J., 1994.

[4]

John Horton Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.

[5]

Andrew D. Ferguson, Arjun Guha, Chen Liang, Rodrigo Fonseca, and Shriram Krishnamurthi. Participatory networking: An API for application control of SDNs. In SIGCOMM, 2013.

Digital Library

[6]

Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, and David Walker. Frenetic: A network programming language. In ICFP, September 2011.

Digital Library

[7]

Arjun Guha, Mark Reitblatt, and Nate Foster. Machine-verified network controllers. In PLDI, June 2013.

Digital Library

[8]

Stephen Gutz, Alec Story, Cole Schlesinger, and Nate Foster. Splendid isolation: A slice abstraction for software-defined networks. In HotSDN, 2012.

Digital Library

[9]

James Hamilton. Networking: The last bastion of mainframe computing, December 2009. Available at http://tinyurl.com/y9uz64e.

[10]

Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In NSDI, 2012.

Digital Library

[11]

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. VeriFlow: Verifying network-wide invariants in real time. In NSDI, 2013.

Digital Library

[12]

Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. I&C, 110(2):366--390, May 1994.

Digital Library

[13]

Dexter Kozen. Kleene algebra with tests and commutativity conditions. In TACAS, pages 14--33, Passau, Germany, March 1996.

Digital Library

[14]

Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427--443, May 1997.

Digital Library

[15]

Dexter Kozen. Kleene algebras with tests and the static analysis of programs. Technical Report TR2003--1915, Computer Science Department, Cornell University, November 2003.

[16]

Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using Kleene algebra with tests. In CL, July 2000.

Digital Library

[17]

Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In CSL, September 1996.

Digital Library

[18]

Boon Thau Loo, Joseph M. Hellerstein, Ion Stoica, and Raghu Ramakrishnan. Declarative routing: Extensible routing with declarative queries. In SIGCOMM, 2005.

Digital Library

[19]

Haohui Mai, Ahmed Khurshid, Raghit Agarwal, Matthew Caesar, P. Brighten Godfrey, and Samuel Talmadge King. Debugging the data plane with Anteater. In SIGCOMM, 2011.

Digital Library

[20]

James McCauley, Aurojit Panda, Martin Casado, Teemu Koponen, and Scott Shenker. Extending SDN to large-scale networks. In ONS, 2013.

[21]

Nick McKeown, Tom Anderson, Hari Balakrishnan, Guru Parulkar, Larry Peterson, Jennifer Rexford, Scott Shenker, and Jonathan Turner. OpenFlow: Enabling innovation in campus networks. SIGCOMM Computing Communications Review, 38(2):69--74, 2008.

Digital Library

[22]

B. Möller. Calculating with pointer structures. In Algorithmic Languages and Calculi. Proc. IFIP TC2/WG2.1 Working Conference, February 1997.

Digital Library

[23]

Christopher Monsanto, Nate Foster, Rob Harrison, and David Walker. A compiler and run-time system for network programming languages. In POPL, January 2012.

Digital Library

[24]

Christopher Monsanto, Joshua Reich, Nate Foster, Jennifer Rexford, and David Walker. Composing software-defined networks. In NSDI, April 2013.

Digital Library

[25]

Tim Nelson, Arjun Guha, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. A balance of power: Expressive, analyzable controller programming. In HotSDN, 2013.

Digital Library

[26]

Mark Reitblatt, Nate Foster, Jennifer Rexford, Cole Schlesinger, and David Walker. Abstractions for network update. In SIGCOMM, 2012.

Digital Library

[27]

Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003.

Digital Library

[28]

Gunther Schmidt. Relational Mathematics. Cambridge University Press, 2010.

Digital Library

[29]

O. Shmueli. Decidability and expressiveness aspects of logic queries. In PODS, pages 237--249, 1987.

Digital Library

[30]

The Frenetic Project, 2013. See http://frenetic-lang.org.

[31]

Andreas Voellmy and Paul Hudak. Nettle: Functional reactive programming of OpenFlow networks. In PADL, 2011.

[32]

Andreas Voellmy, Junchang Wang, Y. Richard Yang, Bryan Ford, and Paul Hudak. Maple: Simplifying SDN programming using algorithmic policies. In SIGCOMM, 2013.

Digital Library

[33]

Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu. Formally verifiable networking. In HotNets, 2009.

[34]

Minlan Yu, Jennifer Rexford, Xin Sun, Sanjay G. Rao, and Nick Feamster. A survey of virtual LAN usage in campus networks. IEEE Communications Magazine, 49(7):98--103, 2011.

Cited By

Campbell EHojjat HFoster N(2024)Computing Precise Control Interface SpecificationsProceedings of the ACM on Programming Languages10.1145/36897438:OOPSLA2(905-934)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689743
Gao XGao JG KZhai ENarayana SSivaraman A(2024)Cross-Platform Transpilation of Packet-Processing Programs using Program SynthesisProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663419(74-80)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663419
Różowski WSilva ASobocinski PLago UEsparza J(2024)A Completeness Theorem for Probabilistic Regular ExpressionsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662084(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662084
Show More Cited By

Index Terms

NetKAT: semantic foundations for networks
1. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Specialized application languages

Recommendations

A Coalgebraic Decision Procedure for NetKAT
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

NetKAT is a domain-specific language and logic for specifying and verifying network packet-processing functions. It consists of Kleene algebra with tests (KAT) augmented with primitives for testing and modifying packet headers and encoding network ...
A fast compiler for NetKAT
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

High-level programming languages play a key role in a growing number of networking platforms, streamlining application development and enabling precise formal reasoning about network behavior. Unfortunately, current compilers only handle "local" ...
NetKAT: semantic foundations for networks
POPL '14

Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2014

702 pages

ISBN:9781450325448

DOI:10.1145/2535838

General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

ACM SIGPLAN Notices Volume 49, Issue 1
POPL '14
January 2014
661 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2578855
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '14

Sponsor:

SIGPLAN

POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 22 - 24, 2014

California, San Diego, USA

Acceptance Rates

POPL '14 Paper Acceptance Rate 51 of 220 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

286
Total Citations
View Citations
1,954
Total Downloads

Downloads (Last 12 months)228
Downloads (Last 6 weeks)39

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Campbell EHojjat HFoster N(2024)Computing Precise Control Interface SpecificationsProceedings of the ACM on Programming Languages10.1145/36897438:OOPSLA2(905-934)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689743
Gao XGao JG KZhai ENarayana SSivaraman A(2024)Cross-Platform Transpilation of Packet-Processing Programs using Program SynthesisProceedings of the 8th Asia-Pacific Workshop on Networking10.1145/3663408.3663419(74-80)Online publication date: 3-Aug-2024
https://dl.acm.org/doi/10.1145/3663408.3663419
Różowski WSilva ASobocinski PLago UEsparza J(2024)A Completeness Theorem for Probabilistic Regular ExpressionsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662084(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662084
Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Cutler JWatson CNkurumeh EHilliard PGoldstein HStanford CPierce B(2024)Stream TypesProceedings of the ACM on Programming Languages10.1145/36564348:PLDI(1412-1436)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656434
Wang CScazzariello MFarshin AFerlin SKostić DChiesa M(2024)NetConfEval: Can LLMs Facilitate Network Configuration?Proceedings of the ACM on Networking10.1145/36562962:CoNEXT2(1-25)Online publication date: 13-Jun-2024
https://dl.acm.org/doi/10.1145/3656296
Xu XYuan YKincaid ZKrishnamurthy AMahajan RWalker DZhai ESekar VYu MSeneviratne AVeitch D(2024)Relational Network VerificationProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672238(213-227)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672238
Chu DPanchapakesan RLaddad SKatahanas LLiu CShivakumar KCrooks NHellerstein JHoward H(2024)Optimizing Distributed Protocols with Query RewritesProceedings of the ACM on Management of Data10.1145/36392572:1(1-25)Online publication date: 26-Mar-2024
https://dl.acm.org/doi/10.1145/3639257
Qin XO’Connor Lvan Glabbeek RHöfner PKammar OSteuwer M(2024)Shoggoth: A Formal Foundation for Strategic RewritingProceedings of the ACM on Programming Languages10.1145/36332118:POPL(61-89)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633211
Feng HBonsangue MHong JPark J(2024)Concurrent NetKAT with PortsProceedings of the 39th ACM/SIGAPP Symposium on Applied Computing10.1145/3605098.3636048(1722-1730)Online publication date: 8-Apr-2024
https://dl.acm.org/doi/10.1145/3605098.3636048
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents