Generalizing SMT Models for Networking Problems

Recent publications in Internet networks rely on Satisfiability Modulo Theories (SMT) models. Most verification systems [1,2,3] but also other problems that can be phrased into a synthesis question[4,5,6,7,8] are solved using SMT solvers. However, these SMT models vary significantly due to different requirements and problem statements, making it challenging to design a single SMT model that can be universally applied. As a result, there is a need for a flexible interface that allows users to easily create customized SMT models for their specific networking problems.

The goal of this thesis is to design an interface that allows for the quick creation of customized SMT models for network control planes. The interface should provide abstractions that enable users to specify which protocols should be encoded, how they should be encoded, and which aspects should be fixed versus encoded using symbolic variables. During the last couple of years, we developed a discrete-event BGP simulator BGPSim. We propose to integrate the interface into BGPSim, leveraging its capabilities and providing a comprehensive tool for network verification and synthesis. This integration will enable users to not only create simulate and evaluate network configurations but also to create customized SMT models and analyze the resulting counter-example using the existing capabilities of BGPSim.

Milestones

  • WP1: Familiarize yourself with recent publications on network verification and synthesis, and find similarities and differences between the SMT models they create.
  • WP2: Design an interface to create customized SMT models. The interface should offer both high-level (quick and easy) methods for creating basic SMT models while providing lower-level tools to precisely control the generated model.
  • WP3: Implement the interface as an extension of the existing BGPSim library.

Requirements

  • Interest in formal methods
  • Basic knowledge of network verification and SMT solvers (watch the recording of our 2023 lecture on Advanced Topics in Communication Networks, Weeks 6 [first 45 minutes], 7, and 8)
  • General programming skills, ideally some familiarity with the Rust programming language.

References

  1. R. Beckett, A. Gupta, R. Mahajan, and D. Walker. A General Approach to Network Configuration Verification. ACM SIGCOMM (2017).
  2. T.A. Thijm, R. Beckett, A. Gupta, and D. Walker. Modular Control Plane Verification via Temporal Invariants. ACM PLDI (2023).
  3. A. Tang, R. Beckett, S. Benaloh, K. Jayaraman, T. Patil, T. Millstein, and G. Varghese. Lightyear: Using Modularity to Scale BGP Control Plane Verification. ACM SIGCOMM (2023).
  4. A. Gember-Jacobson, A. Akella, R. Mahajan, and H. Harry Liu. Automatically Repairing Network Control Planes Using an Abstract Representation. ACM SOSP (2017).
  5. A. El-Hassany, P. Tsankov, L. Vanbever, and M. Vechev. NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. USENIX NSDI (2018).
  6. K. Subramanian, L. D’Antoni, and A. Akella. Synthesis of fault-tolerant distributed router configurations. ACM MACS (2018).
  7. R. Birkner, D. Drachsler-Cohen, L. Vanbever, and M. Vechev. Config2Spec: Mining Network Specifications from Network Configurations . USENIX NSDI (2020).
  8. A. Gember-Jacobson, R. Shrestha, and X. Sun. Localizing Router Configuration Errors Using Minimal Correction Sets. arXiv preprint (2022).

Supervisors

Tibor Schneider
PhD student