Skip to main content
SpringerLink
Log in

Fast BGP Simulation of Large Datacenters

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11388))

Abstract

Frequent configuration churn caused by maintenance, upgrades, hardware and firmware failures regularly leads to costly outages. Preventing network outages caused by misconfigurations is important for ensuring high network availability. Dealing with production datacenters with thousands of routers is a major challenge.

Network verification inspects the forwarding tables of routers. These tables are determined by the so-called control plane, which is given by the steady state of the routing protocols. The ability to simulate routing protocols given router configuration files and thus obtain the control plane is a key enabling technology.

In this paper, we present FastPlane, an efficient BGP simulator. BGP support is mandated by modern datacenter designs, which choose BGP as the routing protocol. The key to FastPlane’s performance is our insight into the routing policy of cloud datacenters that allows the usage of a generalized Dijkstra’s algorithm. The insight reveals that these networks are monotonic, i.e., route advertisements decrease preference when propagated through the network.

The evaluation on real world, production datacenters of a major cloud provider shows that FastPlane (1) is two orders of magnitude faster than the state-of-the-art on small and medium datacenters, and (2) goes beyond the state-of-the-art by scaling to large datacenters. FastPlane was instrumental in finding several production bugs in router firmware, routing policy, and network architecture.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Adão, P., Bozzato, C., Rossi, G.D., Focardi, R., Luccio, F.L.: Mignis: a semantic based tool for firewall configuration. In: CSF (2014)

    Google Scholar 

  2. Al-Fares, M., Loukissas, A., Vahdat, A.: A scalable, commodity data center network architecture. In: SIGCOMM (2008)

    Google Scholar 

  3. Al-Shaer, E., Al-Haj, S.: FlowChecker: configuration analysis and verification of federated openflow infrastructures. In: SafeConfig (2010)

    Google Scholar 

  4. Alim, M.A., Griffin, T.G.: On the interaction of multiple routing algorithms. In: CoNEXT (2011)

    Google Scholar 

  5. Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: POPL (2014)

    Google Scholar 

  6. Andreyev, A.: Introducing data center fabric, the next-generation Facebook data center network (2014)

    Google Scholar 

  7. Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI (2014)

    Article  Google Scholar 

  8. Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: SIGCOMM (2017)

    Google Scholar 

  9. Beckett, R., Mahajan, R., Millstein, T., Padhye, J., Walker, D.: Don’t mind the gap: bridging network-wide objectives and device-level configurations. In: SIGCOMM (2016)

    Google Scholar 

  10. Beckett, R., Mahajan, R., Millstein, T., Padhye, J., Walker, D.: Network configuration synthesis with abstract topologies. In: PLDI (2017)

    Google Scholar 

  11. Bjørner, N., Jayaraman, K.: Checking cloud contracts in Microsoft Azure. In: Natarajan, R., Barua, G., Patra, M.R. (eds.) ICDCIT 2015. LNCS, vol. 8956, pp. 21–32. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-14977-6_2

    Chapter  Google Scholar 

  12. Bjørner, N., Juniwal, G., Mahajan, R., Seshia, S.A., Varghese, G.: ddNF: an efficient data structure for header spaces. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 49–64. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49052-6_4

    Chapter  Google Scholar 

  13. Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng. 1(1), 146–166 (1989)

    Article  Google Scholar 

  14. Dobrescu, M., Argyraki, K.: Software dataplane verification. In: NSDI (2014)

    Google Scholar 

  15. Dynerowicz, S., Griffin, T.G.: On the forwarding paths produced by internet routing algorithms. In: ICNP (2013)

    Google Scholar 

  16. El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.: SDNRacer: concurrency analysis for software-defined networks. In: PLDI (2016)

    Google Scholar 

  17. Fayaz, S.K., et al.: Efficient network reachability analysis using a succinct control plane representation. In: OSDI (2016)

    Google Scholar 

  18. Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: NSDI (2005)

    Google Scholar 

  19. Feamster, N., Rexford, J.: Network-wide prediction of BGP routes. IEEE/ACM Trans. Netw. 15(2), 253–266 (2007)

    Article  Google Scholar 

  20. Fogel, A., et al.: A general approach to network configuration analysis. In: NSDI (2015)

    Google Scholar 

  21. Gao, L., Rexford, J.: Stable internet routing without global coordination. In: SIGMETRICS (2000)

    Google Scholar 

  22. Gember-Jacobson, A., Viswanathan, R., Akella, A., Mahajan, R.: Fast control plane analysis using an abstract representation. In: SIGCOMM (2016)

    Google Scholar 

  23. Greenberg, A., et al.: Vl2: a scalable and flexible data center network. In: SIGCOMM (2009)

    Google Scholar 

  24. Griffin, T.G., Shepherd, F.B., Wilfong, G.: The stable paths problem and interdomain routing. IEEE/ACM Trans. Netw. 10(2), 232–243 (2002)

    Article  Google Scholar 

  25. Griffin, T.G., Shepherd, F.B., Wilfong, G.T.: Policy disputes in path-vector protocols. In: ICNP (1999)

    Google Scholar 

  26. Griffin, T.G., Sobrinho, J.L.: Metarouting. In: SIGCOMM (2005)

    Google Scholar 

  27. Hallahan, W.T., Zhai, E., Piskac, R.: Automated repair by example for firewalls. In: FMCAD (2017)

    Google Scholar 

  28. Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: NSDI (2013)

    Google Scholar 

  29. Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI (2012)

    Google Scholar 

  30. Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: verifying network-wide invariants in real time. In: NSDI (2013)

    Google Scholar 

  31. Lahiri, P., et al.: Routing design for large scale data centers: BGP is a better IGP. In: NANOG’55 (2012)

    Google Scholar 

  32. Lapukhov, P., Premji, A., Mitchell, J.: RFC 7938: Use of BGP for Routing in Large-Scale Data Centers (2016)

    Google Scholar 

  33. Lengauer, T., Theune, D.: Efficient algorithms for path problems with general cost criteria. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 314–326. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54233-7_144

    Chapter  MATH  Google Scholar 

  34. Liu, H., et al.: CrystalNet: faithfully emulating large production networks. In: SOSP (2017)

    Google Scholar 

  35. Lloyd’s. Failure of a top cloud service provider could cost US economy \$15 billion (2018)

    Google Scholar 

  36. Lopes, N.P., Bjørner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: NSDI (2015)

    Google Scholar 

  37. Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with anteater. In: SIGCOMM (2011)

    Google Scholar 

  38. Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: FMCAD (2014)

    Google Scholar 

  39. Plotkin, G.D., Bjørner, N., Lopes, N.P., Rybalchenko, A., Varghese, G.: Scaling network verification using symmetry and surgery. In: POPL (2016)

    Google Scholar 

  40. Quoitin, B., Uhlig, S.: Modeling the routing of an autonomous system with C-BGP. IEEE Netw. 19(6), 12–19 (2005)

    Article  Google Scholar 

  41. Rekhter, Y., Li, T., Hares, S.: RFC 4271: A Border Gateway Protocol 4 (BGP-4) (2006)

    Google Scholar 

  42. Rusinovich, M.: TechEd 2013: Windows Azure Internals (2013)

    Google Scholar 

  43. Sobrinho, J.L.: Algebra and algorithms for QoS path computation and hop-by-hop routing in the internet. IEEE/ACM Trans. Netw. 10(4), 541–550 (2002)

    Article  Google Scholar 

  44. Sobrinho, J.L.: An algebraic theory of dynamic network routing. IEEE/ACM Trans. Netw. 13, 1160–1173 (2005)

    Article  Google Scholar 

  45. Subramanian, K., D’Antoni, L., Akella, A.: Genesis: synthesizing forwarding tables in multi-tenant networks. In: POPL (2017)

    Google Scholar 

  46. Wang, Y., et al.: TenantGuard: scalable runtime verification of cloud-wide VM-level network isolation. In: NDSS (2017)

    Google Scholar 

  47. Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Scalable verification of border gateway protocol configurations with an SMT solver. In: OOPSLA (2016)

    Google Scholar 

  48. Xie, G.G., et al.: On static reachability analysis of IP networks. In: INFOCOM (2005)

    Google Scholar 

  49. Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. In: ICNP (2013)

    Google Scholar 

  50. Zhang, S., Mahmoud, A., Malik, S., Narain, S.: Verification and synthesis of firewalls using SAT and QBF. In: ICNP (2012)

    Google Scholar 

  51. Zhang, S., Malik, S.: SAT based verification of network data planes. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 496–505. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_43

    Chapter  Google Scholar 

  52. Zhang, S., Malik, S., McGeer, R.: Verification of computer switching networks: an overview. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 1–16. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33386-6_1

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Nuno P. Lopes & Andrey Rybalchenko

Authors
  1. Nuno P. Lopes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrey Rybalchenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nuno P. Lopes .

Editor information

Editors and Affiliations

  1. IRIF, University Paris Diderot and CNRS, Paris, France

    Constantin Enea

  2. Yale University, New Haven, CT, USA

    Ruzica Piskac

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lopes, N.P., Rybalchenko, A. (2019). Fast BGP Simulation of Large Datacenters. In: Enea, C., Piskac, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2019. Lecture Notes in Computer Science(), vol 11388. Springer, Cham. https://doi.org/10.1007/978-3-030-11245-5_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-11245-5_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-11244-8

  • Online ISBN: 978-3-030-11245-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation