Document Open Access Logo

New Directions for Network Verification

Authors Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2015.209.pdf
  • Filesize: 0.64 MB
  • 12 pages

Document Identifiers

Author Details

Aurojit Panda
Katerina Argyraki
Mooly Sagiv
Michael Schapira
Scott Shenker

Cite As Get BibTex

Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, and Scott Shenker. New Directions for Network Verification. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 209-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.SNAPL.2015.209

Abstract

Network verification has recently gained popularity in the programming languages and verification community. Much of the recent work in this area has focused on verifying the behavior of simple networks, whose actions are dictated by static, immutable rules configured ahead of time. However, in reality, modern networks contain a variety of middleboxes, whose behavior is affected both by their configuration and by mutable state updated in response to packets received by them. In this position paper we critically review recent progress on network verification, propose some next steps towards a more complete form of network verification, dispel some myths about networks, provide a more formal description of our approach, and end with a discussion of the formal questions posed to this community by the network verification agenda.

Subject Classification

Keywords
  • Middleboxes
  • Network Verification
  • Mutable Dataplane

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. A scalable, commodity data center network architecture. In SIGCOMM, 2008. Google Scholar
  2. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: Semantic foundations for networks. In POPL, 2014. Google Scholar
  3. Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. In POPL, 1977. Google Scholar
  4. Natasha Gude, Teemu Koponen, Justin Pettit, Ben Pfaff, Martín Casado, Nick McKeown, and Scott Shenker. Nox: towards an operating system for networks. ACM SIGCOMM CCR, 38(3):105-110, 2008. Google Scholar
  5. Arjun Guha, Mark Reitblatt, and Nate Foster. Machine-verified network controllers. In PLDI, 2013. Google Scholar
  6. Swati Gupta, Kristen LeFevre, and Atul Prakash. Span: a unified framework and toolkit for querying heterogeneous access policies. In HotSec, 2009. Google Scholar
  7. Alon Y. Halevy, Inderpal Singh Mumick, Yehoshua Sagiv, and Oded Shmueli. Static analysis in datalog extensions. J. ACM, 48(5):971-1012, September 2001. Google Scholar
  8. Cliff B. Jones. Specification and design of (parallel) programs. In IFIP Congress, 1983. Google Scholar
  9. Peyman Kazemian, Michael Chang, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. Real time network policy checking using header space analysis. In NSDI, 2013. Google Scholar
  10. Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In NSDI, 2012. Google Scholar
  11. Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. Veriflow: Verifying network-wide invariants in real time. In NSDI, 2013. Google Scholar
  12. Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, Brighten Godfrey, and Samuel Talmadge King. Debugging the Data Plane with Anteater. In SIGCOMM, 2011. Google Scholar
  13. Alain Mayer, Avishai Wool, and Elisha Ziskind. Fang: A firewall analysis engine. In Security and Privacy, 2000. Google Scholar
  14. Nick McKeown, Tom Anderson, Hari Balakrishnan, Guru Parulkar, Larry Peterson, Jennifer Rexford, Scott Shenker, and Jonathan Turner. OpenFlow: Enabling Innovation in Campus Networks. In SIGCOMM CCR, 2008. Google Scholar
  15. Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Trans. Software Eng., 7(4):417-426, 1981. Google Scholar
  16. Christopher Monsanto, Joshua Reich, Nate Foster, Jennifer Rexford, David Walker, et al. Composing software defined networks. In NSDI, 2013. Google Scholar
  17. Tim Nelson, Andrew D. Ferguson, Michael J. G. Scheer, and Shriram Krishnamurthi. Tierless programming and reasoning for software-defined networks. In NSDI, 2014. Google Scholar
  18. Tim Nelson, Arjun Guha, Daniel J Dougherty, Kathi Fisler, and Shriram Krishnamurthi. A balance of power: Expressive, analyzable controller programming. In HotSDN, 2013. Google Scholar
  19. Timothy Nelson, Christopher Barratt, Daniel J Dougherty, Kathi Fisler, and Shriram Krishnamurthi. The margrave tool for firewall analysis. In LISA, 2010. Google Scholar
  20. OpenStack. Congress. https://wiki.openstack.org/wiki/Congress; retrieved 01/08/2015.
  21. Rahul Potharaju and Navendu Jain. Demystifying the dark side of the middle: a field study of middlebox failures in datacenters. In IMC, 2013. Google Scholar
  22. Scott Shenker. SDN: Looking Back, Moving Forward. Talk at Interent2 Technology Exchange 2014. Google Scholar
  23. Justine Sherry, Shaddi Hasan, Colin Scott, Arvind Krishnamurthy, Sylvia Ratnasamy, and Vyas Sekar. Making middleboxes someone else’s problem: Network processing as a cloud service. In SIGCOMM, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact