Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Active Learning of Symbolic NetKAT Automata

Mark Moeller, Tiago Ferreira, Thomas Lu, Nate Foster, Alexandra Silva

TL;DR

This work tackles learning models of networks specified in NetKAT by developing active learning algorithms for NetKAT automata. It introduces a NetKAT-specific Myhill-Nerode theory and two learning frameworks: canonical PNKA learning for carry-on-aware automata and symbolic NKL^* learning for dup-free and full NetKAT via Symbolic Packet Programs. The authors prove soundness, implement prototypes, and evaluate on a standard topology benchmark, showing the symbolic approach scales to realistic network configurations. The results demonstrate that symbolic NetKAT learning can produce compact, accurate models of network behavior and policies, enabling automated verification and monitoring, while also revealing NP-hardness inherent in minimizing symbolic representations.

Abstract

NetKAT is a domain-specific programming language and logic that has been successfully used to specify and verify the behavior of packet-switched networks. This paper develops techniques for automatically learning NetKAT models of unknown networks using active learning. Prior work has explored active learning for a wide range of automata (e.g., deterministic, register, Büchi, timed etc.) and also developed applications, such as validating implementations of network protocols. We present algorithms for learning different types of NetKAT automata, including symbolic automata proposed in recent work. We prove the soundness of these algorithms, build a prototype implementation, and evaluate it on a standard benchmark. Our results highlight the applicability of symbolic NetKAT learning for realistic network configurations and topologies.

Active Learning of Symbolic NetKAT Automata

TL;DR

This work tackles learning models of networks specified in NetKAT by developing active learning algorithms for NetKAT automata. It introduces a NetKAT-specific Myhill-Nerode theory and two learning frameworks: canonical PNKA learning for carry-on-aware automata and symbolic NKL^* learning for dup-free and full NetKAT via Symbolic Packet Programs. The authors prove soundness, implement prototypes, and evaluate on a standard topology benchmark, showing the symbolic approach scales to realistic network configurations. The results demonstrate that symbolic NetKAT learning can produce compact, accurate models of network behavior and policies, enabling automated verification and monitoring, while also revealing NP-hardness inherent in minimizing symbolic representations.

Abstract

NetKAT is a domain-specific programming language and logic that has been successfully used to specify and verify the behavior of packet-switched networks. This paper develops techniques for automatically learning NetKAT models of unknown networks using active learning. Prior work has explored active learning for a wide range of automata (e.g., deterministic, register, Büchi, timed etc.) and also developed applications, such as validating implementations of network protocols. We present algorithms for learning different types of NetKAT automata, including symbolic automata proposed in recent work. We prove the soundness of these algorithms, build a prototype implementation, and evaluate it on a standard benchmark. Our results highlight the applicability of symbolic NetKAT learning for realistic network configurations and topologies.

Paper Structure

This paper contains 19 sections, 1 theorem, 20 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Background on NetKAT and NetKAT Automata
  3. Encoding Networks in NetKAT
  4. NetKAT Automata
  5. Myhill-Nerode Theorem for NetKAT and Canonical Automata
  6. Learning Canonical NetKAT Automata
  7. The PNKA Teacher
  8. The Observation Table
  9. Access Prefixes
  10. Distinguishing Sequences
  11. Closed and Consistent Observation Tables
  12. The PNKA Learning Algorithm
  13. Correctness of the Canonical Learner
  14. Learning Symbolic Packet Programs (SPPs)
  15. Background
  16. ...and 4 more sections

Key Result

theorem 1

SmallSPP is NP-hard.

Figures (7)

  • Figure 1: NetKAT syntax and semantics.
  • Figure 2: Algorithm for learning canonical automata (left) and subroutine for update (right).
  • Figure 3: Subroutines used in PNKA learning (\ref{['fig:learncanonical']}): $\textsf{mkClosed} \colon T \rightarrow T$ (left) and $\textsf{mkConsistent} \colon T \rightarrow T$ (right).
  • Figure 4: Algorithm for learning SPPs.
  • Figure 5: Definition of $\mathsf{hyp}_{\mathsf{SPP}}$, for generalizing EPPs to SPPs.
  • ...and 2 more figures

Theorems & Definitions (11)

  • definition 1
  • definition 2
  • definition 3
  • definition 4: MAT Interface
  • definition 5: Packet Table
  • definition 6: Observation Table
  • Remark 1
  • definition 7: Closed Table
  • definition 8: Consistent Table
  • definition 9
  • ...and 1 more