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.