Fast BGP Simulation of Large Datacenters

  • Nuno P. LopesEmail author
  • Andrey Rybalchenko
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)


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.


  1. 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. 2.
    Al-Fares, M., Loukissas, A., Vahdat, A.: A scalable, commodity data center network architecture. In: SIGCOMM (2008)Google Scholar
  3. 3.
    Al-Shaer, E., Al-Haj, S.: FlowChecker: configuration analysis and verification of federated openflow infrastructures. In: SafeConfig (2010)Google Scholar
  4. 4.
    Alim, M.A., Griffin, T.G.: On the interaction of multiple routing algorithms. In: CoNEXT (2011)Google Scholar
  5. 5.
    Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: POPL (2014)Google Scholar
  6. 6.
    Andreyev, A.: Introducing data center fabric, the next-generation Facebook data center network (2014)Google Scholar
  7. 7.
    Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI (2014)CrossRefGoogle Scholar
  8. 8.
    Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: SIGCOMM (2017)Google Scholar
  9. 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. 10.
    Beckett, R., Mahajan, R., Millstein, T., Padhye, J., Walker, D.: Network configuration synthesis with abstract topologies. In: PLDI (2017)Google Scholar
  11. 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). Scholar
  12. 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). Scholar
  13. 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)CrossRefGoogle Scholar
  14. 14.
    Dobrescu, M., Argyraki, K.: Software dataplane verification. In: NSDI (2014)Google Scholar
  15. 15.
    Dynerowicz, S., Griffin, T.G.: On the forwarding paths produced by internet routing algorithms. In: ICNP (2013)Google Scholar
  16. 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. 17.
    Fayaz, S.K., et al.: Efficient network reachability analysis using a succinct control plane representation. In: OSDI (2016)Google Scholar
  18. 18.
    Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: NSDI (2005)Google Scholar
  19. 19.
    Feamster, N., Rexford, J.: Network-wide prediction of BGP routes. IEEE/ACM Trans. Netw. 15(2), 253–266 (2007)CrossRefGoogle Scholar
  20. 20.
    Fogel, A., et al.: A general approach to network configuration analysis. In: NSDI (2015)Google Scholar
  21. 21.
    Gao, L., Rexford, J.: Stable internet routing without global coordination. In: SIGMETRICS (2000)Google Scholar
  22. 22.
    Gember-Jacobson, A., Viswanathan, R., Akella, A., Mahajan, R.: Fast control plane analysis using an abstract representation. In: SIGCOMM (2016)Google Scholar
  23. 23.
    Greenberg, A., et al.: Vl2: a scalable and flexible data center network. In: SIGCOMM (2009)Google Scholar
  24. 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)CrossRefGoogle Scholar
  25. 25.
    Griffin, T.G., Shepherd, F.B., Wilfong, G.T.: Policy disputes in path-vector protocols. In: ICNP (1999)Google Scholar
  26. 26.
    Griffin, T.G., Sobrinho, J.L.: Metarouting. In: SIGCOMM (2005)Google Scholar
  27. 27.
    Hallahan, W.T., Zhai, E., Piskac, R.: Automated repair by example for firewalls. In: FMCAD (2017)Google Scholar
  28. 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. 29.
    Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI (2012)Google Scholar
  30. 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. 31.
    Lahiri, P., et al.: Routing design for large scale data centers: BGP is a better IGP. In: NANOG’55 (2012)Google Scholar
  32. 32.
    Lapukhov, P., Premji, A., Mitchell, J.: RFC 7938: Use of BGP for Routing in Large-Scale Data Centers (2016)Google Scholar
  33. 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). Scholar
  34. 34.
    Liu, H., et al.: CrystalNet: faithfully emulating large production networks. In: SOSP (2017)Google Scholar
  35. 35.
    Lloyd’s. Failure of a top cloud service provider could cost US economy \$15 billion (2018)Google Scholar
  36. 36.
    Lopes, N.P., Bjørner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: NSDI (2015)Google Scholar
  37. 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. 38.
    Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: FMCAD (2014)Google Scholar
  39. 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. 40.
    Quoitin, B., Uhlig, S.: Modeling the routing of an autonomous system with C-BGP. IEEE Netw. 19(6), 12–19 (2005)CrossRefGoogle Scholar
  41. 41.
    Rekhter, Y., Li, T., Hares, S.: RFC 4271: A Border Gateway Protocol 4 (BGP-4) (2006)Google Scholar
  42. 42.
    Rusinovich, M.: TechEd 2013: Windows Azure Internals (2013)Google Scholar
  43. 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)CrossRefGoogle Scholar
  44. 44.
    Sobrinho, J.L.: An algebraic theory of dynamic network routing. IEEE/ACM Trans. Netw. 13, 1160–1173 (2005)CrossRefGoogle Scholar
  45. 45.
    Subramanian, K., D’Antoni, L., Akella, A.: Genesis: synthesizing forwarding tables in multi-tenant networks. In: POPL (2017)Google Scholar
  46. 46.
    Wang, Y., et al.: TenantGuard: scalable runtime verification of cloud-wide VM-level network isolation. In: NDSS (2017)Google Scholar
  47. 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. 48.
    Xie, G.G., et al.: On static reachability analysis of IP networks. In: INFOCOM (2005)Google Scholar
  49. 49.
    Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. In: ICNP (2013)Google Scholar
  50. 50.
    Zhang, S., Mahmoud, A., Malik, S., Narain, S.: Verification and synthesis of firewalls using SAT and QBF. In: ICNP (2012)Google Scholar
  51. 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). Scholar
  52. 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). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Microsoft ResearchCambridgeUK

Personalised recommendations