research-article

Free access

Debugging the data plane with anteater

Authors:

Ahmed Khurshid,

Rachit Agarwal,

Matthew Caesar,

P. Brighten Godfrey,

Samuel Talmadge KingAuthors Info & Claims

SIGCOMM '11: Proceedings of the ACM SIGCOMM 2011 conference

Pages 290 - 301

https://doi.org/10.1145/2018436.2018470

Published: 15 August 2011 Publication History

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

Supplementary Material

MP4 File (sigcomm_9_2.mp4)

Download
196.51 MB

References

[1]

JUNOS: MPLS fast reroute solutions, network operations guide. 2007.

[2]

The all new 2010 Intel Core vPro processor family: Intelligence that adapts to your needs (whitepaper). 2010. http://www.intel.com/Assets/PDF/whitepaper/311710.pdf.

[3]

E. S. Al-Shaer and H. H. Hamed. Discovery of policy anomalies in distributed firewalls. In Proc. IEEE INFOCOM, 2004.

[4]

Apple. What is lights out management?, September 2010. http://support.apple.com/kb/TA24506.

[5]

F. Baccelli, S. Machiraju, D. Veitch, and J. Bolot. The role of PASTA in network measurement. In Proc. ACM SIGCOMM, 2006.

Digital Library

[6]

Y. Bartal, A. Mayer, K. Nissim, and A. Wool. Firmato: A novel firewall management toolkit. In Proc. IEEE S&P, 1999.

[7]

T. Benson, A. Akella, and D. Maltz. Unraveling the complexity of network management. In Proc. USENIX NSDI, 2009.

Digital Library

[8]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS, 1999.

Digital Library

[9]

R. Brummayer and A. Biere. Boolector: An efficient smt solver for bit-vectors and arrays. In Proc. TACAS, 2009.

Digital Library

[10]

R. Bush and T. G. Griffin. Integrity for virtual private routed networks. In Proc. IEEE INFOCOM, 2003.

[11]

Cisco Systems Inc. Spanning tree protocol problems and related design considerations. http://www.cisco.com/en/US/tech/tk389/tk621/technologies_tech_note09186%a00800951ac.shtml, August 2005. Document ID 10556.

[12]

J. Duffy. BGP bug bites Juniper software. Network World, December 2007.

[13]

J. Evers. Trio of Cisco flaws may threaten networks. CNET News, January 2007.

[14]

D. Farinacci, T. Li, S. Hanks, D. Meyer, and P. Traina. Generic Routing Encapsulation (GRE). RFC 2784, March 2000.

Digital Library

[15]

N. Feamster and H. Balakrishnan. Detecting BGP configuration faults with static analysis. In Proc. USENIX NSDI, 2005.

Digital Library

[16]

N. Feamster and J. Rexford. Network-wide prediction of bgp routes. IEEE/ACM Transactions on Networking, 15:253--266, 2007.

Digital Library

[17]

A. Feldmann, O. Maennel, Z. Mao, A. Berger, and B. Maggs. Locating Internet routing instabilities. In Proc. ACM SIGCOMM, 2004.

Digital Library

[18]

D. Geels, G. Altekar, P. Maniatis, T. Roscoe, and I. Stoica. Friday: global comprehension for distributed replay. In Proc. USENIX NSDI, 2007.

Digital Library

[19]

G. Goodell, W. Aiello, T. Griffin, J. Ioannidis, P. McDaniel, and A. Rubin. Working around BGP: An incremental approach to improving security and accuracy of interdomain routing. In Proc. NDSS, 2003.

[20]

H. Hamed, E. Al-Shaer, and W. Marrero. Modeling and verification of IPSec and VPN security policies. In Proc. ICNP, 2005.

Digital Library

[21]

X. Hu and Z. M. Mao. Accurate real-time identification of IP prefix hijacking. In Proc. IEEE S&P, 2007.

Digital Library

[22]

M. Lasserre and V. Kompella. Virtual private lan service (VPLS) using label distribution protocol (LDP) signaling. RFC 4762, January 2007.

[23]

C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proc. CGO, 2004.

Digital Library

[24]

X. Liu, Z. Guo, X. Wang, F. Chen, X. Lian, J. Tang, M. Wu, M. F. Kaashoek, and Z. Zhang. D3S: Debugging deployed distributed systems. In Proc. USENIX NSDI, 2008.

Digital Library

[25]

R. Mahajan, D. Wetherall, and T. Anderson. Understanding BGP misconfiguration. In Proc. ACM SIGCOMM, 2002.

Digital Library

[26]

Y. Mandelbaum, S. Lee, and D. Caldwell. Adaptive parsing of router configuration languages. In Workshop INM, 2008.

[27]

Z. M. Mao, D. Johnson, J. Rexford, J. Wang, and R. Katz. Scalable and accurate identification of AS-level forwarding paths. In Proc. IEEE INFOCOM, 2004.

[28]

N. McKeown, T. Anderson, H. Balakrishnan, G. Parulkar, L. Peterson, J. Rexford, and S. Shenker. OpenFlow: Enabling innovation in campus networks. ACM CCR, April 2008.

Digital Library

[29]

Nagios. http://www.nagios.org.

[30]

Quagga Routing Suite. http://www.quagga.net.

[31]

Quagga Software Routing Suite. Commercial Resources. http://www.quagga.net/commercial.php.

[32]

Renesys. Longer is not always better. http://www.renesys.com/blog/2009/02/longer-is-not-better.shtml.

[33]

T. Roscoe, S. Hand, R. Isaacs, R. Mortier, and P. Jardetzky. Predicate routing: enabling controlled networking. ACM CCR, January 2003.

Digital Library

[34]

Ruby-Prolog. https://rubyforge.org/projects/ruby-prolog.

[35]

F. Silveira, C. Diot, N. Taft, and R. Govindan. ASTUTE: Detecting a different class of traffic anomalies. In Proc. ACM SIGCOMM, 2010.

Digital Library

[36]

N. Spring, R. Mahajan, and D. Wetherall. Measuring ISP topologies with rocketfuel. In Proc. ACM SIGCOMM, 2002.

Digital Library

[37]

P. Tune and D. Veitch. Towards optimal sampling for flow size estimation. In Proc. IMC, 2008.

Digital Library

[38]

J. Wu, Z. M. Mao, J. Rexford, and J. Wang. Finding a needle in a haystack: Pinpointing significant BGP routing changes in an IP network. In Proc. USENIX NSDI, 2005.

Digital Library

[39]

G. G. Xie, J. Zhan, D. A. Maltz, H. Zhang, A. Greenberg, G. Hjalmtysson, and J. Rexford. On static reachability analysis of IP networks. In Proc. IEEE INFOCOM, 2005.

[40]

Y. Xie and A. Aiken. Saturn: A scalable framework for error detection using boolean satisfiability. Proc. ACM TOPLAS, 29(3), 2007.

Digital Library

[41]

Z. Yin, M. Caesar, and Y. Zhou. Towards understanding bugs in open source router software. ACM CCR, June 2010.

Digital Library

[42]

D. Yuan, H. Mai, W. Xiong, L. Tan, Y. Zhou, and S. Pasupathy. SherLog: Error diagnosis by connecting clues from run-time logs. In ASPLOS, 2010.

Digital Library

[43]

L. Yuan, J. Mai, Z. Su, H. Chen, C.-N. Chuah, and P. Mohapatra. FIREMAN: A toolkit for FIREwall Modeling and ANalysis. In Proc. IEEE S&P, 2006.

Digital Library

[44]

E. Zmijewski. Reckless driving on the Internet. http://www.renesys.com/blog/2009/02/the-flap-heard-around-the-worl.shtml, February 2009.

Cited By

Dozier KBeltran JBerg KMatousek HSalamatian LKatz-Bassett ERubenstein D(2024)Toward Applying Quantum Computing to Network VerificationProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696891(221-228)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696891
Kou TSun HZhuang ZQi QWang JLiao J(2024)Accelerating ACL Configuration Update through Data Plane AnalysisProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673888(48-50)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673888
Xu XYuan YKincaid ZKrishnamurthy AMahajan RWalker DZhai ESekar VYu MSeneviratne AVeitch D(2024)Relational Network VerificationProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672238(213-227)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672238
Show More Cited By

Index Terms

Debugging the data plane with anteater
1. Networks
  1. Network services
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Debugging the data plane with anteater
SIGCOMM '11

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, ...
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
DAC '09: Proceedings of the 46th Annual Design Automation Conference

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and ...
On the power of clause-learning SAT solvers as resolution engines

In this work, we improve on existing results on the relationship between proof systems obtained from conflict-driven clause-learning SAT solvers and general resolution. Previous contributions such as those by Beame et al. (2004), Hertel et al. (2008), ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SIGCOMM '11: Proceedings of the ACM SIGCOMM 2011 conference

August 2011

502 pages

ISBN:9781450307970

DOI:10.1145/2018436

General Chairs:
Srinivasan Keshav
University of Waterloo, Canada
,
Jörg Liebeherr
University of Toronto, Canada
,
Program Chairs:
John Byers
Boston University, USA
,
Jeffrey Mogul
HP Labs, USA

ACM SIGCOMM Computer Communication Review Volume 41, Issue 4
SIGCOMM '11
August 2011
480 pages
ISSN:0146-4833
DOI:10.1145/2043164
Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 August 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SIGCOMM '11

Sponsor:

SIGCOMM

SIGCOMM '11: ACM SIGCOMM 2011 Conference

August 15 - 19, 2011

Ontario, Toronto, Canada

Acceptance Rates

SIGCOMM '11 Paper Acceptance Rate 32 of 223 submissions, 14%;

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

347
Total Citations
View Citations
1,761
Total Downloads

Downloads (Last 12 months)185
Downloads (Last 6 weeks)16

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dozier KBeltran JBerg KMatousek HSalamatian LKatz-Bassett ERubenstein D(2024)Toward Applying Quantum Computing to Network VerificationProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696891(221-228)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696891
Kou TSun HZhuang ZQi QWang JLiao J(2024)Accelerating ACL Configuration Update through Data Plane AnalysisProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673888(48-50)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673888
Xu XYuan YKincaid ZKrishnamurthy AMahajan RWalker DZhai ESekar VYu MSeneviratne AVeitch D(2024)Relational Network VerificationProceedings of the ACM SIGCOMM 2024 Conference10.1145/3651890.3672238(213-227)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3651890.3672238
Guo ZLi FShen JWang X(2024)NetCR: Knowledge-Graph-Based Recommendation Framework for Manual Network ConfigurationIEEE Internet of Things Journal10.1109/JIOT.2023.333701711:7(12941-12952)Online publication date: 1-Apr-2024
https://doi.org/10.1109/JIOT.2023.3337017
Sakurada HSakurai K(2024)Research Directions in Formal Verification of Network Configurations Toward Verification of Mobile NetworksMobile Internet Security10.1007/978-981-97-4465-7_18(248-259)Online publication date: 12-Jul-2024
https://doi.org/10.1007/978-981-97-4465-7_18
Liao JHe BWang JWang JQi QLiao JHe BWang JWang JQi Q(2024)Intelligent Allocation Technologies for All-Scenario KDN ResourcesKey Technologies for On-Demand 6G Network Services10.1007/978-3-031-70606-6_7(163-201)Online publication date: 26-Sep-2024
https://doi.org/10.1007/978-3-031-70606-6_7
Ruffy FLiu JKotikalapudi PHavel VTavante HSherwood RDubina VPeschanenko VSivaraman AFoster NSchulzrinne HKohler EMaltz DMisra V(2023)P4Testgen: An Extensible Test Oracle For P4-16Proceedings of the ACM SIGCOMM 2023 Conference10.1145/3603269.3604834(136-151)Online publication date: 10-Sep-2023
https://dl.acm.org/doi/10.1145/3603269.3604834
Li YHu XJia CWang KLi J(2023)Kano: Efficient Cloud Native Network Policy VerificationIEEE Transactions on Network and Service Management10.1109/TNSM.2022.322967520:3(3747-3764)Online publication date: Sep-2023
https://doi.org/10.1109/TNSM.2022.3229675
Alaraj ABock KLevin DWustrow E(2023)A Global Measurement of Routing Loops on the InternetPassive and Active Measurement10.1007/978-3-031-28486-1_16(373-399)Online publication date: 21-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-28486-1_16
Guo DChen SGao KXiang QZhang YYang YKuipers FOrda A(2022)FlashProceedings of the ACM SIGCOMM 2022 Conference10.1145/3544216.3544246(314-335)Online publication date: 22-Aug-2022
https://dl.acm.org/doi/10.1145/3544216.3544246
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents