Metha: Network Verifiers Need To Be Correct Too!
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.
Research Area: Verification and Synthesis
People
BibTex
@INPROCEEDINGS{birkner2021metha,
isbn = {978-1-939133-21-2},
copyright = {In Copyright - Non-Commercial Use Permitted},
year = {2021-04},
booktitle = {Proceedings of the 18th USENIX Symposium on Networked System Design and Implementation},
type = {Conference Paper},
institution = {EC},
author = {Birkner, Rüdiger and Brodmann, Tobias and Tsankov, Petar and Vanbever, Laurent and Vechev, Martin},
size = {15 p. accepted version},
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.},
language = {en},
address = {Berkeley, CA},
publisher = {USENIX Association},
DOI = {10.3929/ethz-b-000491509},
title = {Metha: Network Verifiers Need To Be Correct Too!},
PAGES = {99 - 113},
Note = {18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2021); Conference Location: Online; Conference Date: April 12–14, 2021; Conference lecture held on April 12, 2021}
}Research Collection: 20.500.11850/499146