Diagnose network failures via data-plane analysis

Data-Plane Analysis;Network Failure;Satisfiability

Mai, Haohui ; King, Samuel T. ; King ; Samuel T.

关键词: Data-Plane Analysis;    Network Failure;    Satisfiability;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/18419/Mai_Haohui.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

Diagnosing problems in networks is a time-consuming and error-prone process. Previous tools to assist operators primarily focus on analyzing controlplane configuration. Configuration analysis is limited in that it cannot findbugs in router software, and is harder to generalize across protocols since itmust model complex configuration languages and dynamic protocol behavior.This paper studies an alternate approach: diagnosing problems throughstatic analysis of the data plane. This approach can catch bugs that areinvisible at the level of configuration files, and simplifies unified analysis of anetwork across many protocols and implementations. We present Anteater, atool for checking invariants in the data plane. Anteater translates high-levelnetwork invariants into boolean satisfiability problems, checks them againstnetwork state using a SAT solver, and reports counterexamples if violationshave been found. Applied to a large campus network, Anteater revealed 23bugs, including forwarding loops and stale ACL rules, with only five falsepositives. Nine of these faults are being fixed by campus network operators.