Haohui Mai
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.
Supplemental Material
- JUNOS: MPLS fast reroute solutions, network operations guide. 2007.Google Scholar
- 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.Google Scholar
- E. S. Al-Shaer and H. H. Hamed. Discovery of policy anomalies in distributed firewalls. In Proc. IEEE INFOCOM, 2004.Google ScholarCross Ref
- Apple. What is lights out management?, September 2010. http://support.apple.com/kb/TA24506.Google Scholar
- F. Baccelli, S. Machiraju, D. Veitch, and J. Bolot. The role of PASTA in network measurement. In Proc. ACM SIGCOMM, 2006. Google ScholarDigital Library
- Y. Bartal, A. Mayer, K. Nissim, and A. Wool. Firmato: A novel firewall management toolkit. In Proc. IEEE S&P, 1999.Google ScholarCross Ref
- T. Benson, A. Akella, and D. Maltz. Unraveling the complexity of network management. In Proc. USENIX NSDI, 2009. Google ScholarDigital Library
- A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS, 1999. Google ScholarDigital Library
- R. Brummayer and A. Biere. Boolector: An efficient smt solver for bit-vectors and arrays. In Proc. TACAS, 2009. Google ScholarDigital Library
- R. Bush and T. G. Griffin. Integrity for virtual private routed networks. In Proc. IEEE INFOCOM, 2003.Google ScholarCross Ref
- 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.Google Scholar
- J. Duffy. BGP bug bites Juniper software. Network World, December 2007.Google Scholar
- J. Evers. Trio of Cisco flaws may threaten networks. CNET News, January 2007.Google Scholar
- D. Farinacci, T. Li, S. Hanks, D. Meyer, and P. Traina. Generic Routing Encapsulation (GRE). RFC 2784, March 2000. Google ScholarDigital Library
- N. Feamster and H. Balakrishnan. Detecting BGP configuration faults with static analysis. In Proc. USENIX NSDI, 2005. Google ScholarDigital Library
- N. Feamster and J. Rexford. Network-wide prediction of bgp routes. IEEE/ACM Transactions on Networking, 15:253--266, 2007. Google ScholarDigital Library
- A. Feldmann, O. Maennel, Z. Mao, A. Berger, and B. Maggs. Locating Internet routing instabilities. In Proc. ACM SIGCOMM, 2004. Google ScholarDigital Library
- D. Geels, G. Altekar, P. Maniatis, T. Roscoe, and I. Stoica. Friday: global comprehension for distributed replay. In Proc. USENIX NSDI, 2007. Google ScholarDigital Library
- 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.Google Scholar
- H. Hamed, E. Al-Shaer, and W. Marrero. Modeling and verification of IPSec and VPN security policies. In Proc. ICNP, 2005. Google ScholarDigital Library
- X. Hu and Z. M. Mao. Accurate real-time identification of IP prefix hijacking. In Proc. IEEE S&P, 2007. Google ScholarDigital Library
- M. Lasserre and V. Kompella. Virtual private lan service (VPLS) using label distribution protocol (LDP) signaling. RFC 4762, January 2007.Google Scholar
- C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proc. CGO, 2004. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- R. Mahajan, D. Wetherall, and T. Anderson. Understanding BGP misconfiguration. In Proc. ACM SIGCOMM, 2002. Google ScholarDigital Library
- Y. Mandelbaum, S. Lee, and D. Caldwell. Adaptive parsing of router configuration languages. In Workshop INM, 2008.Google Scholar
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Nagios. http://www.nagios.org.Google Scholar
- Quagga Routing Suite. http://www.quagga.net.Google Scholar
- Quagga Software Routing Suite. Commercial Resources. http://www.quagga.net/commercial.php.Google Scholar
- Renesys. Longer is not always better. http://www.renesys.com/blog/2009/02/longer-is-not-better.shtml.Google Scholar
- T. Roscoe, S. Hand, R. Isaacs, R. Mortier, and P. Jardetzky. Predicate routing: enabling controlled networking. ACM CCR, January 2003. Google ScholarDigital Library
- Ruby-Prolog. https://rubyforge.org/projects/ruby-prolog.Google Scholar
- F. Silveira, C. Diot, N. Taft, and R. Govindan. ASTUTE: Detecting a different class of traffic anomalies. In Proc. ACM SIGCOMM, 2010. Google ScholarDigital Library
- N. Spring, R. Mahajan, and D. Wetherall. Measuring ISP topologies with rocketfuel. In Proc. ACM SIGCOMM, 2002. Google ScholarDigital Library
- P. Tune and D. Veitch. Towards optimal sampling for flow size estimation. In Proc. IMC, 2008. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- Y. Xie and A. Aiken. Saturn: A scalable framework for error detection using boolean satisfiability. Proc. ACM TOPLAS, 29(3), 2007. Google ScholarDigital Library
- Z. Yin, M. Caesar, and Y. Zhou. Towards understanding bugs in open source router software. ACM CCR, June 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- E. Zmijewski. Reckless driving on the Internet. http://www.renesys.com/blog/2009/02/the-flap-heard-around-the-worl.shtml, February 2009.Google Scholar
Index Terms
- Debugging the data plane with anteater
Recommendations
Debugging the data plane with anteater
SIGCOMM '11: Proceedings of the ACM SIGCOMM 2011 conferenceDiagnosing 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 ConferenceBoolean 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