Debugging the data plane with Anteater

Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P. Brighten Godfrey, Samuel T. King

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 instances of 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.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11
Pages290-301
Number of pages12
DOIs
StatePublished - 2011
EventACM SIGCOMM 2011 Conference, SIGCOMM'11 - Toronto, ON, Canada
Duration: Aug 15 2011Aug 19 2011

Publication series

NameProceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11

Other

OtherACM SIGCOMM 2011 Conference, SIGCOMM'11
Country/TerritoryCanada
CityToronto, ON
Period8/15/118/19/11

Keywords

  • Boolean satisfiability
  • Data plane analysis
  • Network troubleshooting

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design

Fingerprint

Dive into the research topics of 'Debugging the data plane with Anteater'. Together they form a unique fingerprint.

Cite this