Committee

  • Aarti Gupta (advisor)
  • David Walker
  • Zak Kincaid

Title

Kirigami, The Verifiable Art of Network Cutting1

Abstract

Existing network verification techniques do not scale to large, real-world networks. We investigate partitioning a network into multiple components to reduce the burden of verification of the stable routing problem (SRP), by cutting the network into multiple composable partitions, calculating separate solutions and then verifying them individually to obtain a proof for the original SRP instance.

We propose a generalized model for "open SRPs", which are a superset of regular (closed) SRPs, which allow us to define compositions and partitions of open SRPs in terms of interfaces. We show that given a correct interface, we can check SRP properties for partitioned SRPs and reconnect the partitions without invalidating the property. We provide a concrete semantics for open SRPs and their compositions, and we show that the SRP interfaces form a complete lattice, enabling us to apply abstract interpretation techniques to approximate correct interfaces. We connect these semantics to rely-guarantee reasoning and show how our interfaces function as invariants over the cross-partition edges of the SRP.
We provide some examples of these processes from nv, a programming language for simulating and verifying synthetic networks. We develop an extension, Kirigami, which allows an nv programmer to write and check these interfaces.

Reading List

Papers

  • Fogel, Ari, et al. "A general approach to network configuration analysis." 12th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 15). 2015.
  • Griffin, Timothy G., F. Bruce Shepherd, and Gordon Wilfong. "The stable paths problem and interdomain routing." IEEE/ACM Transactions On Networking 10.2 (2002): 232-243.
  • Jayaraman, Karthick, et al. "Validating datacenters at scale." Proceedings of the ACM Special Interest Group on Data Communication. 2019. 200-213.
  • Barrett, Clark, et al. "Satisfiability Modulo Theories, Handbook of Satisfiability, chapter 12." (2008): 737-797.
  • Giannakopoulou, Dimitra, Kedar S. Namjoshi, and Corina S. Păsăreanu. "Compositional reasoning." Handbook of Model Checking. Springer, Cham, 2018. 345-383.
  • Jhala, Ranjit, and Rupak Majumdar. "Software model checking." ACM Computing Surveys (CSUR) 41.4 (2009): 1-54.
  • Torlak, Emina, and Rastislav Bodik. "A lightweight symbolic virtual machine for solver-aided host languages." ACM SIGPLAN Notices 49.6 (2014): 530-541.
  • Milner, Robin, and Mads Tofte. "Co-induction in relational semantics." Theoretical computer science 87.1 (1991): 209-220.
  • Xu, Qiwen, Willem-Paul de Roever, and Jifeng He. "The rely-guarantee method for verifying shared variable concurrent programs." Formal Aspects of Computing 9.2 (1997): 149-174.

Textbooks

  • Pierce, Benjamin C., and C. Benjamin. Types and programming languages. MIT press, 2002.
  • Bradley, Aaron R., and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007.

Slides

They can be found here in Keynote format.

Questions

(including follow-up questions)
  1. Zak: explain how an SMT solver uses something like DPLL(T) to prove a statement in LIA. What does it look like, why do we look at satisfying assignments to the skeleton of the formula rather than the formula with LIA? What kind of method could you use (that Calculus of Computations shows) to check a bunch of LIA-theory formulas? (Cooper’s method, I did not remember the details very well, but Zak helped me along)
  2. Dave: give me the types and expressions of System F. (I got coached through the type variables a bit) What is an expression in System F that is not a legal expression in OCaml’s type system, and what is it called? (I did know it was Hindley-Milner, although Dave gave me the answer to the first part before I said that when I struggled with writing out the expression he was looking for -- a polymorphic function not in prenex normal form)
  3. Aarti: since you read Software Model Checking, explain what an interpolant is and what you use it for. (Took me a while to get the second part, but eventually got there).

1 See here for an explanation of the title.