Skip to main content
SpringerLink
Log in

ddNF: An Efficient Data Structure for Header Spaces

  • Conference paper
  • First Online:
Hardware and Software: Verification and Testing (HVC 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10028))

Included in the following conference series:

Abstract

Network Verification is emerging as a critical enabler to manage large complex networks. In order to scale to data-center networks found in Microsoft Azure we developed a new data structure called ddNF, disjoint difference Normal Form, that serves as an efficient container for a small set of equivalence classes over header spaces. Our experiments show that ddNFs outperform representations proposed in previous work, in particular representations based on BDDs, and is especially suited for incremental verification. The advantage is observed empirically; in the worst case ddNFs are exponentially inferior than using BDDs to represent equivalence classes. We analyze main characteristics of ddNFs to explain the advantages we are observing.

S.A. Seshia—UC Berkeley authors supported in part by the NSF ExCAPE project (CCF-1139138).

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

Notes

  1. 1.

    Also called “cubes” in the VLSI CAD literature.

References

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

    Google Scholar 

  2. Bosshart, P., Daly, D., Gibb, G., Izzard, M., McKeown, N., Rexford, J., Schlesinger, C., Talayco, D., Vahdat, A., Varghese, G., Walker, D.: P4: programming protocol-independent packet processors. SIGCOMM Comput. Commun. Rev. 44(3), 87–95 (2014)

    Article  Google Scholar 

  3. Bosshart, P., Gibb, G., Kim, H.-S., Varghese, G., McKeown, N., Izzard, M., Mujica, F., Horowitz, M.: Forwarding metamorphosis: fast programmable match-action processing in hardware for SDN. In: SIGCOMM (2013)

    Google Scholar 

  4. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  5. Greenberg, A., Hamilton, J., Maltz, D.A., Patel, P.: The cost of a cloud: research problems in data center networks. SIGCOMM Comput. Commun. Rev. 39(1), 68–73 (2008)

    Article  Google Scholar 

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

  7. Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI, pp. 113–126 (2012)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

  11. McKeown, N.: Mind the gap. In: SIGCOMM (2012). http://youtu.be/Ho239zpKMwQ

  12. Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The margrave tool for firewall analysis. In: LISA (2010)

    Google Scholar 

  13. Pathak, A., Zhang, M., Hu, Y.C., Mahajan, R., Maltz, D.: Latency inflation in MPLS-based traffic engineering. In: Internet Measurement Conference (IMC) (2011)

    Google Scholar 

  14. Plotkin, G.D., Bjørner, N., Lopes, N.P., Rybalchenko, A., Varghese, G.: Scaling network verification using symmetry and surgery. In: Bodík, R., Majumdar R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016, pp. 69–83. ACM (2016)

    Google Scholar 

  15. The BuDDy BDD package. http://buddy.sourceforge.net/manual/main.html

  16. Xie, G.G., Zhan, J., Maltz, D.A., Zhang, H., Greenberg, A.G., Hjálmtýsson, G., Rexford, J.: On static reachability analysis of IP networks. In: INFOCOM (2005)

    Google Scholar 

  17. Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. In: ICNP, pp. 1–11 (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, USA

    Nikolaj Bjørner & Ratul Mahajan

  2. University of California, Berkeley, USA

    Garvit Juniwal & Sanjit A. Seshia

  3. University of California, Los Angeles, USA

    George Varghese

Authors
  1. Nikolaj Bjørner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Garvit Juniwal
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ratul Mahajan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sanjit A. Seshia
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. George Varghese
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nikolaj Bjørner .

Editor information

Editors and Affiliations

  1. IAIK, Graz University of Technology, Graz, Austria

    Roderick Bloem

  2. IBM Research Labs, Haifa, Israel

    Eli Arbel

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Bjørner, N., Juniwal, G., Mahajan, R., Seshia, S.A., Varghese, G. (2016). ddNF: An Efficient Data Structure for Header Spaces. In: Bloem, R., Arbel, E. (eds) Hardware and Software: Verification and Testing. HVC 2016. Lecture Notes in Computer Science(), vol 10028. Springer, Cham. https://doi.org/10.1007/978-3-319-49052-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-49052-6_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-49051-9

  • Online ISBN: 978-3-319-49052-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation