NetKAT
A Domain-Specific Language for Network Programming with Formal Foundations
NetKAT
A Domain-Specific Language for Network Programming with Formal Foundations
NetKAT is a domain-specific language for specifying and reasoning about packet-forwarding networks. It is grounded in Kleene Algebra with Tests (KAT) and provides a sound and complete equational theory for reasoning about network behavior. NetKAT enables both high-level network programming and automated verification of network properties.
Built on Kleene Algebra with Tests, providing rigorous mathematical foundations for network programming with provable correctness guarantees.
Check network properties like reachability, isolation, and program equivalence automatically using decision procedures and symbolic tools.
Express complex network behaviors using algebraic operators, enabling equational reasoning about network programs.
Learn NetKAT concepts step-by-step with interactive examples, from basic packet tests to advanced verification techniques.
Start TutorialExperiment with NetKAT expressions in an interactive environment with curated examples and exercises.
Open PlaygroundA fast symbolic verifier for NetKAT that efficiently checks program equivalence and network properties.
View on GitHubPLDI 2025 • DOI
Develops algorithms for actively learning NetKAT automata models of unknown networks, facilitating automated inference of network behaviors for verification purposes.
PLDI 2025 • DOI
Introduces StacKAT, an extension of NetKAT with a stack data structure for modeling networks that manipulate packet stacks (e.g. MPLS or tunneling protocols).
PLDI 2024 • DOI
Introduces KATch, a tool for fast symbolic verification of NetKAT programs, enabling efficient checking of program equivalence and other properties using symbolic automata techniques.
Master's Thesis, 2023 (Cornell University) • DOI
Introduces guarded NetKAT (GNetKAT), proves soundness and partial-completeness, and introduces a (almost) linear-time coalgebraic decision procedure for GNetKAT program equivalence.
ESOP 2022 • DOI
Extends NetKAT with constructs for concurrency and stateful interactions, introducing a model based on partially ordered multisets (pomsets) for reasoning about concurrent network behaviors.
FoSSaCS 2022 • DOI
Proposes an extension of NetKAT to handle dynamic network updates and multi-packet interactions, adding constructs for synchronization between control-plane updates and data-plane forwarding.
arXiv preprint, 2021 • arXiv
Proposes methods for explaining safety violations in NetKAT programs by identifying undesired behaviors and providing equational proofs of their occurrence.
arXiv preprint, 2021 • arXiv
Proposes MatchKAT, an extension of NetKAT for modeling match-action packet processing in network switches.
POPL 2020 • DOI
Integrates Probabilistic NetKAT into a functional programming setting, treating network policies as first-class, higher-order functions and extending the language with λ-calculus features.
PLDI 2019 • DOI
Introduces McNetKAT, a model checker for probabilistic NetKAT programs that focuses on the history-free fragment and provides exact analysis using finite-state absorbing Markov chains.
CoNEXT 2019 • DOI
Introduces a variant of NetKAT for specifying normal forms of match-action programs, using ideas from relational databases and formal language theory.
RAMiCS 2018 • DOI
Uses NetKAT to model and analyze the dynamic gossip protocol, where network links appear or disappear as agents share information.
ICFEM 2017 • DOI
Develops an operational semantics for NetKAT and leverages it for verification using the Maude system, enabling automatic analyses such as reachability and temporal property model checking.
arXiv preprint, 2017 • arXiv
Tackles the problem of checking equivalence of Probabilistic NetKAT programs, restricting to the history-free fragment and developing a decision procedure based on constructing and comparing stochastic matrices.
arXiv preprint, 2016 • arXiv
Extends NetKAT to WNetKAT by incorporating weights, enabling the modeling and verification of networks with quantitative attributes like bandwidth and latency.
ESOP 2016 • DOI
Extends NetKAT with probabilistic choice, allowing programs to specify randomized network behaviors. Provides a denotational semantics in terms of distributions on packet histories and a sound and ground-complete equational axiomatization.
PLDI 2016 • DOI
Extends NetKAT with syntactic constructs from past-time, finite-trace linear temporal logic to support writing queries about packet histories.
PLDI 2016 • DOI
Introduces an extension of NetKAT with mutable state to support event-driven network updates, ensuring consistent behavior during dynamic changes.
ICFP 2015 • DOI
Presents a high-performance compiler for NetKAT that handles complex features like regular paths and virtual networks, significantly improving compilation times with optimizations like symbolic automata representations.
POPL 2015 • DOI
Presents a new algorithm for deciding equivalence of NetKAT programs by constructing finite automata (policy automata) for NetKAT terms. Despite NetKAT's equational theory being PSPACE-complete, shows the procedure is efficient in practice.
POPL 2014 • DOI
Introduces NetKAT, a network programming language grounded in Kleene Algebra with Tests (KAT), providing a sound and complete equational theory for reasoning about network behavior.
APLAS 2014 • DOI
An accessible survey and tutorial of NetKAT's design and theory, providing a self-contained introduction to NetKAT's syntax, semantics, and equational reasoning principles.
NetKAT has been developed by researchers from multiple institutions, with significant contributions from Cornell University, Princeton University, Radboud University, and other academic institutions.