Committee

  • Aarti Gupta (advisor)
  • David Walker
  • Jennifer Rexford

Title

An Abstraction for Network Control Plane Verification

Abstract

We address the formal verification of distributed control planes in networks. This is a challenging problem and prior efforts have proposed the use of SMT-based techniques that can handle a wide range of network design features and correctness properties, but are limited in scalability. We make two distinct contributions to improve scalability. Our first contribution is a novel abstraction where each router makes a nondeterministic choice among neighboring routers that have an available route, i.e., each router picks any available route, not necessarily the best route according to the protocol. This results in an over-approximation that is provably sound and is often precise. Our second contribution is an effective SMT encoding where we use symbolic graphs to encode all possible stable routing trees that are compliant with the given network control plane configurations. This enables the use of SMT solvers that support specialized predicates for graph properties in addition to standard SMT solvers. We have implemented our abstraction and SMT-based encodings in a prototype tool. Our evaluations show that our abstraction can provide significant relative speed-ups (up to 12X) in performance, and our tool can scale up to large networks (with more than 10,000 routers) for verifying reachability.

Reading List

Papers

  1. Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories, Handbook of Model Checking, pages 305 – 343. Springer International Publishing, Cham, 2018.
  2. Sam Bayless, Noah Bayless, Holger H. Hoos, and Alan J. Hu. Sat modulo monotonic theories. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI’15, page 3702–3709, 2015.
  3. Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Abstract interpretation of distributed network control planes. Proc. ACM Program. Lang., 4(POPL), December 2019.
  4. Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. Fast control plane analysis using an abstract representation. In SIGCOMM, 2016.
  5. Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. A general approach to network configuration analysis. In NSDI, 2015.
  6. Timothy G. Griffin, F. Bruce Shepherd, and Gordon Wilfong. The stable paths problem and interdomain routing. IEEE/ACM Trans. Networking, 10(2), 2002.
  7. Jõao Luís Sobrinho. An algebraic theory of dynamic network routing. IEEE/ACM Trans. Netw., 13(5):1160–1173, October 2005.
  8. Kenneth L. McMillan. Interpolation and Model Checking, Handbook of Model Checking, pages 421–446. Springer International Publishing, Cham, 2018.
  9. Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. Predicate Abstraction for Program Verification, pages 447–491. Springer International Publishing, Cham, 2018.
  10. Anduo Wang, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov, and Carolyn L. Talcott. FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing. IEEE/ACM Transactions on Networking (ToN), 2012.
  11. Chen Chen, Lay Kuan Loh, Limin Jia, Wenchao Zhou, and Boon Thau Loo. Automated Verification of Safety Properties in Declarative Networking Programs. International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), July, 2015.

Textbooks

  1. “Types and Programming Languages” by Benjamin Pierce (chapters 1-11, 13-19, 22-25, 29-30)
  2. “The Calculus of Computation: Decision Procedures with Applications to Verification” by Aaron R. Bradley and Zohar Manna (chapters 1- 6, 12)

Questions

(including follow-up questions)
  1. (Rexford) How would your approach change if each router picked best routes for each neighboring router instead of the best route overall? How would you modify the encoding to handle multipath routing?
  2. (Walker) Write down the types and expressions in System F.
  3. (Gupta) In your talk you mentioned abstraction refinement using CEGAR as an extension for future work. Could you give us more details about how you would use CEGAR for abstraction refinement?
  4. (Rexford) Could you give an instance of the Stable Paths Problem that has no solution, and one that has multiple solutions?
  5. (Walker) How does your approach handle instances that have no stable solution or multiple stable solutions? (Follow-up to Q.4)
  6. (Walker) What is the main approach of the paper "Automated Verification of Safety Properties in Declarative Networking Programs"? How does SMT-based control plane verification compare with simulation-based techniques that can detect property violations in transient states of a network?