Network Verification Papers

Vision for Network Design Automation and Network Verification, G. Varghese

Scaling Network Verification using Symmetry and Surgery, G. Plotkin, N. Bjorner, N. Lopes, A. Rybalchenko, G. Varghese, POPL 2016, to appear. Exploits symmetries in data centers to provide a 65x improvement in verification time.

From Header Space to Control Space: Towards Comprehensive Control Plane Verification, S. Fayaz, A. Fogel, R. Mahajan, T. Millstein, V. Sekar, G. Varghese, in submission, first steps towards automated verification of routing (e.g., BGP) computation

Packet Transactions: A Programming Model for Data-Plane Algorithms at Hardware, Anirudh Sivaraman, Mihai Budiu, Alvin Cheung, Changhoon Kim, Steve Licking, George Varghese, Hari Balakrishnan, Mohammad Alizadeh, Nick McKeown, Speed, in submission (Compiler for router algorithms that manipulate state)

Automatic Verification of Network Invariants in P4 Networks N. Lopes, N. Bjorner, A. Rybalchenko, N. Mckeown, D. Talyaco, G. Varghese, early version, Slides for P4 conference, Stanford, 4th June 2015 . Allows automated verification when the network is reprogrammed, via a new compiler from P4 to Datalog. Provides an operational semantics for P4.

Quantitative Network Verification N. Bjorner, G. Juniwal, R. Mahajan, S. Seshia, G. Varghese, preliminary version Extends network verification to quantities such as bandwidth and latency, unlike earlier work that was limited to Booleans like reachability

Checking Beliefs in Dynamic Networks , N. Lopes, N. Bjorner, P. Godefroid, K. Jayaraman, G. Varghese, NSDI 2015. Network Verification in the face of changing networks and incomplete specifications. Earlier tools such as Veriflow and HSA hardcode the specification and the network model.

Compiling Packet Programs to Reconfigurable Switches, L. Yan, L. Jose, G. Varghese, N. McKeown, NSDI 2015, to appear. Mapping from Logical Tables in a P4 Program to physical tables in a hardware pipeline, a first step to compiling P4 to router microcode

P4: programming protocol-independent packet processors, P. Bosshart, D. Daly, G. Gibb, M. Izzard, N. McKeown, J. Rexford, C .Schlesinger, D. Talayco, A. Vahdat, G. Varghese, D. Walker: Computer Communication Review 44(3): 87-95 (2014) A new language for flexible routers that goes beyond OpenFlow Best of CCR Prize, SIGCOMM 2015

Gestalt: Fast, Unified Fault Localization for Networked Systems, R. Mysore, R. Mahajan, A. Vahdat, G. Varghese: USENIX Annual Technical Conference 2014: 255-267. A taxonomy of fault localization, needed for dynamic network verification

Forwarding Metamorphosis: Flexible Match Action processing for SDNs. P. Bosshart, G. Gibb, H. Kim, G. Varghese, M. Izzard, H. Mujica, M. Horowitz, SIGCOMM 2013. A programmable router architecture which motivated the P4 language

Design Principles for Packet Parsers, G. Gibb, G. Varghese, M. Horowitz, N. Mckeown, ANCS 2013, Best Paper Award Parsing packets at high speeds while allowing new headers to be added, an important component of P4

Real time Network Policy Checking Using Header Space Analysis , P. Kazemanian, M. Chang, H. Zheng, G. Varghese, N. McKeown,S. Whyte, NSDI 2013. Incremental and parallel verification of networks and a new policy language

Header Space Analysis: Static Checking for Networks , P. Kazemanian, G. Varghese, N. McKeown, NSDI 2012. Applied Networking Research Prize by the Internet Society in 2014, and presented to the IETF . A form of symbolic model checking/symbolic execution for networks

Automatic Test Packet Generation , H. Zheng, P. Kazemanian, G. Varghese, N. McKeown, CoNEXT 2012. Using test generation ideas for programs to generate tests for networks; much simpler because there are no cycles in normal operation Fast tracked for IEEE Transactions Networking among best papers of CONEXT 2012 and appeared in IEEE/ACM Trans. Netw. 22(2): 554-566 (2014)

Leaping Multiple Headers in a Single Bound: Wire Speed Parsing using the Kangaroo System, C. Kozanitis, J. Huber, S. Singh G. Varghese, INFOCOM 2010. Making data planes flexible. Most chip vendors and the P4 movement advocate flexible parsers today, but Kangaroo was just a little ahead of its time.

Prepared by George Varghese
Last Modified July 2015