Committee

  • Aarti Gupta (advisor)
  • David Walker
  • Mae Milano

Title

Modular Verification and Repair for Networks

Abstract

Large industrial networks connect millions of servers with hundreds of thousands of network devices. To improve these systems’ reliability, researchers have turned to modular verification techniques to break these large networks into smaller pieces to analyze independently. Unfortunately, in doing so, researchers face tradeoffs. More expressive frameworks can verify a wider range of properties, but often place a greater burden on the user to describe network behavior at the interfaces between components. We present CB-graphs, a new framework for modular network control plane verification that navigates these tradeoffs using graph-based abstractions, allowing it to verify a rich set of properties while simplifying the interfaces a user must supply. Users construct CB-graphs that describe which network devices converge before others. Interfaces between nodes in these graphs may contain more or less information, depending on what is convenient and needed to prove the desired properties. We develop a theory of CB-graph-based verification and prove it sound via a formalization in the Lean theorem prover. We exploit our framework to develop a new, scalable method for local repair of network configurations. We implement our verification and repair algorithms in a tool called CB-Ver, and evaluate its performance on a range of benchmarks.

Reading List

Books

  1. Aaron R. Bradley, Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification.
    • Chapters 1-6, 12
  2. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
    • Chapters 1-3, 5-6, 8-9, 11-16, 22-23

Papers

Network Verification
  1. A. Fogel et al., "A general approach to network configuration analysis," in Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation, in NSDI'15. USA: USENIX Association, May 2015, pp. 469–483.
  2. R. Beckett, A. Gupta, R. Mahajan, and D. Walker, "A General Approach to Network Configuration Verification," in Proceedings of the Conference of the ACM Special Interest Group on Data Communication, Aug. 2017, pp. 155–168. (link)
  3. T. G. Griffin and J. L. Sobrinho, "Metarouting," in Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications, Aug. 2005, pp. 1–12. (link)
  4. A. Tang et al., "Lightyear: Using Modularity to Scale BGP Control Plane Verification," in Proceedings of the ACM SIGCOMM 2023 Conference, Sep. 2023, pp. 94–107. (link)
  5. C. J. Anderson et al., "NetKAT: semantic foundations for networks," SIGPLAN Not., vol. 49, no. 1, pp. 113–126, Jan. 2014. (link)
  6. H. Yang and S. S. Lam, "Scalable Verification of Networks With Packet Transformers Using Atomic Predicates," IEEE/ACM Transactions on Networking, vol. 25, no. 5, pp. 2900–2915, Oct. 2017. (link)
Formal Verification
  1. R. Alur et al., "Syntax-guided synthesis," in 2013 Formal Methods in Computer-Aided Design, Oct. 2013, pp. 1–8. (link)
  2. I. Dillig, T. Dillig, B. Li, and K. McMillan, "Inductive invariant generation via abductive inference," SIGPLAN Not., vol. 48, no. 10, pp. 443–456, Nov. 2013. (link)
  3. C. Barrett and C. Tinelli, "Satisfiability Modulo Theories," in Handbook of Model Checking, 2018, pp. 305–343. (link)

Slides

They can be found here in PDF format.

Questions

  1. (Prof. Milano) How can a user write CB-graphs to verify end-to-end reachability for all pairs? (Prof. Walker) Is the number of CB-graphs O(N) or O(N^2) (N is the number of nodes)?
  2. (Prof. Milano) What is BGP? What happens if an operator wants to add a new router into a network and forward to Disney?
  3. (Prof. Walker) Write down the syntax and typing rules for STLC with subtyping. If I change the subtyping rule for function types to be covariant on the first argument, show an example that violates the soundness.
  4. (Prof. Gupta) What is SyGuS and how can you do SyGuS? How can you use SyGuS in CBGraphs to synthesize the P,Q interfaces? What's the syntax you will give? (Prof. Milano) How would you compare traditional SyGuS with modern techniques like using LLM for synthesis?
  5. (Prof. Walker) Write down the syntax of Kleene algebra. What makes it Kleene algebra (answer: Kleene algebra axioms)? How to extend it to KAT?