Rigorous testing for SMT-based network verifiers

Network verification tools are extremely valuable for network operators as they free them from the fear of introducing outages. As with any complex software, though, they can (and often do) have bugs.

Software testing aims to find such bugs. When it comes to network verifiers, we can test a network verification tool by comparing its output to an emulated network [1]. A problem remains, however: While we can check verifier correctness for a single configuration and environment with each test case, SMT verifiers reason over environment spaces (routing inputs, link failures) [2] that are too large to enumerate and test individually.

This thesis aims to explore what rigorous testing could look like for an SMT-based network verifier. The central question is: which tests are sufficient for ensuring (with reasonably high confidence) that a verifier reasons correctly over a given configuration and environment space? Candidate directions include defining coverage criteria based on the verifier’s symbolic model or on its intended input space.

Milestones

  • Getting familiar with our (simple) SMT verifier, and validating its output using an emulated network.
  • Studying which fidelity bugs can occur in a network verifier [1], and injecting such bugs.
  • Adapting suitable testing techniques to the verifier, and generating tests.
  • Assessing whether the developed testing methods are more effective in surfacing subtle bugs than other baselines (e.g., random testing).

Requirements

  • Basic understanding of network verification and SMT
  • Familiarity with software testing methods would be ideal but not necessary; e.g., participation in the course Rigorous Software Engineering (252-0216-00L).

References

  1. R. Birkner, T. Brodmann, P. Tsankov, L. Vanbever, M. Vechev. Metha: Network Verifiers Need To Be Correct Too! NSDI 2021.
  2. R. Beckett, A. Gupta, R. Mahajan, D. Walker. A General Approach to Network Configuration Verification. SIGCOMM 2017.

Supervisors