Metha: Network Verifiers Need To Be Correct Too!
OPEN ACCESS
Author / Producer
Date
2021-04
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Network analysis and verification tools are often a godsend for network operators as they free them from the fear of introducing outages or security breaches. As with any complex software though, these tools can (and often do) have bugs. For the operators, these bugs are not necessarily problematic except if they affect the precision of the model as it applies to their specific network. In that case, the tool output might be wrong: it might fail to detect actual configuration errors and/or report non-existing ones.
In this paper, we present Metha, a framework that systematically tests network analysis and verification tools for bugs in their network models. Metha automatically generates syntactically- and semantically-valid configurations; compares the tool's output to that of the actual router software; and detects any discrepancy as a bug in the tool's model. The challenge in testing network analyzers this way is that a bug may occur very rarely and only when a specific set of configuration statements is present. We address this challenge by leveraging grammar-based fuzzing together with combinatorial testing to ensure thorough coverage of the search space and by identifying the minimal set of statements triggering the bug through delta debugging.
We implemented Metha and used it to test three well-known tools. In all of them, we found multiple (new) bugs in their models, most of which were confirmed by the developers.
Permanent link
Publication status
published
External links
Editor
Book title
Proceedings of the 18th USENIX Symposium on Networked System Design and Implementation
Journal / series
Volume
Pages / Article No.
99 - 113
Publisher
USENIX Association
Event
18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
09477 - Vanbever, Laurent / Vanbever, Laurent
03948 - Vechev, Martin / Vechev, Martin
Notes
Conference lecture held on April 12, 2021
Funding
851809 - From Network Verification to Synthesis: Breaking New Ground in Network Automation (EC)