Verification and Synthesis
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.
The three tales of (correct) network operations