VeriFlow: Verifying Network-Wide Invariants in Real Time

Authors: 

Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey, University of Illinois at Urbana-Champaign

Abstract: 

Networks are complex and prone to bugs. Existing tools that check network configuration files and the data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise.

Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a design, VeriFlow, which achieves this goal. VeriFlow is a layer between a software-defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted, modified or deleted. VeriFlow supports analysis over multiple header fields, and an API for checking custom invariants. Based on a prototype implementation integrated with the NOX OpenFlow controller, and driven by a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion or deletion.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

Khurshid PDF
View the slides

Presentation Video 

Presentation Audio

Public Summary: 

by Richard Mortier

This paper addresses the problem of checking network-wide invariants, allowing detection and prevention of bugs in the network data plane of software defined networks. The key novelty is that VeriFlow allows this verification to be carried out in real time. This extends work presented by the same authors at HotSDN: VeriFlow intercepts communication between the OpenFlow controller and the network to perform its checks.

It achieves real time checking by using trie structures to represent rules so that rules conflicting with a new rule can be detected quickly, and the forwarding graph is built only for the flows that might be affected by the new rule. VeriFlow is evaluated throughimplementation in NOX, run on an emulated Mininet topology driven by Route Views trace data over Rocketfuel topologies.

All reviewers were positive about the paper: it addresses a hard problem, producing a working prototype that achieves good performance. The key concern about the paper was the inability of VeriFlow to check invariants involving rules that re-write packets, but the achievement of real time verification was felt sufficient to outweigh that. A suitable topic for follow-on work perhaps!