Metha: Network Verifiers Need To Be Correct Too!
summary
Metha automatically tests network analysis tools by generating syntactically and semantically valid configurations in a two‑stage generator, running each config both in the tool under test and in a virtualized GNS3 oracle with real Cisco and Juniper images, and reporting discrepancies. It narrows the huge search space with boundary‑value reduction and pairwise combinatorial testing, applies grammar‑based fuzzing, and uses delta debugging to produce minimal reproductions. Evaluation runs about 1,800 pairwise tests (~2 minutes each), finds multiple confirmed silent correctness bugs in Batfish cBGP and NV.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:53The Problem
- 1:46Metha
- 3:02Overview
- 3:31Configuration Generation
- 4:25Configuration Method
- 5:21Configuration Space
- 6:05Limit Options
- 7:01combinatorial testing
- 8:05how Metha performs
- 11:34Summary
related talks
01h 01mNetwork Verification: Past, Present, and Future
16mTest Coverage for Network Configurations
18mMESSI: Behavioral Testing of BGP Implementations
27mNetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion
38mThe Verification of a Distributed System
21mConfig2Spec: Mining Network Specifications from Network Configurations
18mPreview: Verification (Correctness & Debugging)
27mMolecule for Testing Network Automation Ansible Projects