Blueswitch: an OpenFlow switch providing provably correct forwarding
Blueswitch is an OpenFlow hardware switch design that supports a transactional configuration mechanism, and thus a packet-consistent configuration: all packets traversing the datapath encounter either the old configuration or the new one, and never an inconsistent mix of the two.
Papers
Blueswitch: Enabling Provably Consistent Configuration of Network Switches
Jong Hun Han (University of Cambridge), Prashanth Mundkur (SRI International), Charalampos Rotsos (University of Cambridge), Gianni Antichi (University of Cambridge), Nirav Dave (SRI International), Andrew W. Moore (University of Cambridge), Peter G. Neumann (SRI International), ACM/IEEE ANCS, Oakland, CA, USA, 7-8 May, to appear
Abstract: Previous research on consistent updates for distributed network configurations has focused on solutions for centralized network- configuration controllers. However, such work does not address the complexity of modern switch datapaths. Modern commodity switches expose opaque configuration mechanisms, with minimal guarantees for datapath consistency and with unclear configuration semantics. Furthermore, would-be solutions for distributed consis- tent updates must take into account the configuration guarantees provided by each individual switch – plus the compositional prob- lems of distributed control and multi-switch configurations that considerably transcend the single-switch problems. In this paper, we focus on the behavior of individual switches, and demonstrate that even simple rule updates result in inconsistent packet switching in multi-table datapaths. We demonstrate that consistent configu- ration updates require guarantees of strong switch-level atomicity from both hardware and software layers of switches – even in a single switch. In short, the multiple-switch problems cannot be reasonably approached until single-switch consistency can be re- solved.
We present a hardware design that supports a transactional con- figuration mechanism, and provides packet-consistent configura- tion: all packets traversing the datapath will encounter either the old configuration or the new one, and never an inconsistent mix of the two. Unlike previous work, our design does not require mod- ifications to network packets. We precisely specify the hardware- software protocol for switch configuration; this enables us to prove the correctness of the design, and to provide well-specified invari- ants that the software driver must maintain for correctness. We implement our prototype switch design using the NetFPGA-10G hardware platform, and evaluate our prototype against commercial off-the-shelf switches.
Items related to the paper
Acknowledgements
This work was jointly supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-11-C-0249. The views, opinions, and/or findings contained in this article/presentation are those of the author/ presenter and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. We also acknowledge the support of the UK EPSRC for contributing to parts of our work, through grant EP/H040536/1.