Committee

  • David Walker (advisor)
  • Zak Kincaid
  • Maria Apostalaki

Title

Relational Netkat1

Abstract

Modern networks are complex, dynamic, and large-scale, making network verification a critical challenge. Relational NetKAT extends traditional NetKAT by providing an expressive and efficient framework for reasoning about network behavior under path changes, forwarding table modifications, and network topology updates. It enables all-path verification, ensuring that network-wide invariants hold across diverse changes such as load balancing and routing updates. Compared to sample-based verification of Rela, which fails to cover all possible paths, Relational NetKAT provides a mathematically sound and scalable approach to checking network correctness.

Reading List

Papers

NetKAT, Kleene Algebra and Automata Theory
  1. Xieyang Xu, Yifei Yuan, Zachary Kincaid, Arvind Krishnamurthy, Ratul Mahajan, David Walker, and Ennan Zhai. "Relational Network Verification." 2024.
  2. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. "NetKAT: semantic foundations for networks." 2014.
  3. Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. "A Coalgebraic Decision Procedure for NetKAT." 2015.
  4. Damien Pous. "Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests." 2015.
BDD and Model Checking
  1. Bryant Randy. "Symbolic Boolean manipulation with ordered binary-decision diagrams." 1992.
  2. Kathi Fisler and Moshe Y. Vardi. "Bisimulation Minimization and Symbolic Model Checking." 2002.
Network Verification
  1. H. Yang and S. S. Lam. "Real-time verification of network properties using Atomic Predicates." 2013.
  2. Peyman Kazemian, George Varghese, and Nick McKeown. "Header space analysis: static checking for networks." 2012.
  3. Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. "Veriflow: verifying network-wide invariants in real time." 2012.

Textbooks

  • Pierce, Benjamin C., and C. Benjamin. Types and programming languages. MIT press, 2002.
  • Clarke, Edmund M., Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). "Chapter 7.8." Handbook of Model Checking. Springer, 2018.

Slides

They can be found here in PDF format.

Questions

  1. (Prof. Walker) Can you give the syntax of system F? What are the typing rules for system F? How do you define the type soundness? How would you exactly prove the type soundness (list the steps of induction). Can you give the syntax and typing rules for system F-omega? What is the typing context of system F-omega? What would happen if you omit the well-formedness condition of big lambda abstraction rules in system F and F-omega?
  2. (Prof. Apostalaki) What is the header space analysis? How do you compare it with the Veriflow? What is their design purpose? In which condition would you use which one of these? What is the trie data structure in veriflow? What is trie designed for? In what situation would you change the field order in trie?
  3. (Prof. Kincaid) Give the definition of NFA (non-deterministic finite automata). What is the definition of language equivalence? What is the definition of bisimilarity? There are a bunch of bisimilar relations satisfying such a definition, which one would we use? Give an example which is language equivalent but not bisimilar.