Network verification

Network controllers are complex software systems that must simultaneously implement a wide range of policies and services on top of a highly asynchronous environment (the network). As any complex software systems, network controllers are likely to be plagued by bugs that must be discovered and fixed. While discovering these bugs is often hard, fixing them is even harder. As network controllers are critical entity, they cannot simply be "rebooted", they must run at all time to ensure smooth and continuous network operations. As such, network controllers need also to be upgraded on-the-fly.

Our group is involved in verifying that network controllers are correct through static and dynamic analysis. We are also studying how we can make network controller "hot-swappable", enabling controllers to be upgraded at runtime without creating any disruption.

People

Projects

Publications

Config2Spec: Mining Network Specifications from Network Configurations

Rüdiger Birkner, Dana Drachsler Cohen, Laurent Vanbever, Martin Vechev

USENIX NSDI 2020. Santa Clara, California, USA (February 2020).

Integrating Verification and Repair into the Control Plane

Aaron Gember-Jacobson, Costin Raiciu, Laurent Vanbever

ACM HotNets 2017. Palo Alto, California, USA (November 2017).

BigBug: Practical Concurrency Analysis for SDN.

Roman May, Ahmed El-Hassany, Laurent Vanbever, Martin Vechev

ACM SOSR 2017. Santa Clara, CA, USA (April 2017).

SDNRacer: Concurrency Analysis for Software-Defined Networks.

Ahmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, Martin Vechev

ACM PLDI 2016. Santa Barbara, CA, USA (June 2016).

Safe and Flexible Controller Upgrades for SDNs.

Karla Saur, Joseph Collard, Nate Foster, Arjun Guha, Laurent Vanbever, Michael Hicks

ACM SOSR 2016. Santa Clara, CA, USA (March 2016).

SDNRacer: Detecting Concurrency Violations in Software-Defined Networks.

Jeremie Miserez, Pavol Bielik, Ahmed El-Hassany, Laurent Vanbever, Martin Vechev

ACM SOSR 2015. Santa Clara, CA, USA (June 2015).