TY - JOUR
T1 - Debugging the data plane with anteater
AU - Mai, Haohui
AU - Khurshid, Ahmed
AU - Agarwal, Rachit
AU - Caesar, Matthew
AU - Godfrey, P. Brighten
AU - King, Samuel Talmadge
N1 - Funding Information:
We would like to thank our shepherd, Emin Gün Sirer, and the anonymous reviewers for their valuable comments. We also thank our network operator Debbie Fligor for collecting data and sharing her operational experience. This research was funded by NSF grants CNS 0834738, CNS 0831212, CNS 1040396, and CNS 1053781, grant N0014-09-1-0743 from the Office of Naval Research, AFOSR MURI grant FA9550-09-01-0539, a grant from the Internet Services Research Center (ISRC) of Microsoft Research, and a Fulbright S&T Fellowship.
Funding Information:
This research was funded by NSF grants CNS 0834738, CNS 0831212, CNS 1040396, and CNS 1053781, grant N0014-09-1-0743 from the Office of Naval Research, AFOSR MURI grant FA9550-09-01-0539, a grant from the Internet Services Research Center (ISRC) of Microsoft Research, and a Fulbright S and T Fellowship.
Publisher Copyright:
© 2011 ACM.
PY - 2011/8/15
Y1 - 2011/8/15
N2 - Diagnosing problems in networks is a time-consuming and error-prone process. Existing tools to assist operators primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This paper studies an alternate approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. We present Anteater, a tool for checking invariants in the data plane. Anteater translates high-level network invariants into boolean satisfiability problems (SAT), checks them against network state using a SAT solver, and reports counterexamples if violations have been found. Applied to a large university network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. Nine of these faults are being fixed by campus network operators.
AB - Diagnosing problems in networks is a time-consuming and error-prone process. Existing tools to assist operators primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This paper studies an alternate approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. We present Anteater, a tool for checking invariants in the data plane. Anteater translates high-level network invariants into boolean satisfiability problems (SAT), checks them against network state using a SAT solver, and reports counterexamples if violations have been found. Applied to a large university network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. Nine of these faults are being fixed by campus network operators.
KW - Boolean satisfiability
KW - Data plane analysis
KW - Network troubleshooting
UR - http://www.scopus.com/inward/record.url?scp=85090994739&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85090994739&partnerID=8YFLogxK
U2 - 10.1145/2043164.2018470
DO - 10.1145/2043164.2018470
M3 - Article
AN - SCOPUS:85090994739
SN - 0146-4833
VL - 41
SP - 290
EP - 301
JO - Computer Communication Review
JF - Computer Communication Review
IS - 4
ER -