Committee

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

Title

A hiding algorithm for automatically discovering abstractions during network verification

Abstract

In the modern age of internet communication and data centers, network failures are both costly and unfortunately common. Accordingly, there has been much work on developing tools for automatic verification of computer networks in the past decade. However, building and maintaining these tools is made difficult by the complexity of network configuration languages. In this talk I will present my work on NV, an intermediate language for verification of network control planes, which can be used as an intermediate representation for verification tools. I will also present a novel algorithm, dubbed hiding, for speeding up NV’s SMT analyses by removing variables and iteratively re-adding them when they are discovered to be relevant. Although this refinement loop does not directly result in speedups, it opens up opportunities for future work in automatically discovering program abstractions for increasing scalability.

Reading List

Papers

  1. Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram Rajamani. PLDI 2002. (link)
  2. Lazy Abstraction with Interpolants. Kenneth L. McMillan. CAV 2006. (link)
  3. Detecting BGP Configuration Faults with Static Analysis. Nick Feamster, Hari Balakrishnan. NSDI 2005. (link)
  4. Graph-Based Algorithms for Boolean Function Manipulation. Randal E. Bryant. IEEE Transactions on Computers 1986. (link)
  5. Kleene Algebra with Tests. Dexter Kozen. ACM Transactions on Programming Languages and Systems 1997. (link)
  6. An Algebraic Theory of Dynamic Network Routing. João Luís Sobrinho. IEEE/ACM Transactions on Networking 2004. (link)
  7. A General Approach to Network Configuration Analysis. Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, Todd Millstein. NSDI 2015. (link)
  8. Growing Solver-Aided Languages with ROSETTE. Emina Torlak, Rastislav Bodik. Onward! 2013. (link)
  9. Fast Control Plane Analysis Using an Abstract Representation. Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. SIGCOMM 2016. (link)
  10. NetKAT: Semantic Foundations for Networks. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. POPL 2014. (link)

Textbooks

  1. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
  2. Andrew W. Appel. Compiling with Continuations. 1992.

Slides

They can be found here in PDF format.

Questions

(including follow-up questions)
  1. (Dave): Write down the syntax for the simply-typed lambda calculus with subtyping, two base types, and tuples; then write down the typing and subtyping rules for it
  2. (Zak): How does Lazy Abstraction with Interpolants compare to regular abstraction? What's the benefit? What is an interpolant, how do they use them? Do a simple example interpolant.
  3. (Aarti): How does the abstraction used in the ARC paper compare to the one you presented about? How does it work, and what are its main benefits/drawbacks? For what sort of properties might you choose to use ARC over other tools?
  4. (Dave)
    1. Write a simple OCaml function to reverse a list first directly, then using continuation-passing-style, then write an example function which uses the continuation-passing version.
    2. What are the benefits of using continuation-passing style (at least the ones that are listed in the textbook), and do you agree with them?