Everyone is invited to attend his talk. The talk title and abstract follow below.
Abstract:
In recent years network misconfiguration-induced outages have become rampant
both in frequency and impact. Misconfigurations often occur in the control
plane, a distributed system responsible for exchanging routing information among
routers. To configure routing policies, operators have to issue per-device
configurations in low-level languages, while accounting for interactions with
external networks, as well as potential device or link failures. For large
networks --- which may involve millions of lines of configuration spread across
thousands of devices --- this is a challenging task. To aid operators,
researchers have developed a range of static analysis tools to establish
correctness properties of network control planes. However, developing and
maintaining such tools is an enormous undertaking because of the complexity of
configuration languages and the plethora of features the protocols pack.
Inspired by prior work on intermediate languages for verification such as Boogie
and Why3, I will describe the design and implementation of NV, an intermediate
language for verification of routing protocols and their configurations. NV was
designed to strike a balance between expressiveness, tractability and ease of
use. I will explain how to leverage NV's design to develop efficient implementations (often
outperforming the current state-of-the-art by an order of magnitude) of network
analyses such as simulation and SMT-based verification. Beyond these
standard techniques, NV also facilitates the rapid development of new analyses;
I will describe the key insights behind a highly scalable fault tolerance
analysis, and present its implementation in the NV language. Finally, I will present a new
approach to network compression, implemented on top of NV, and suitable for reasoning
about fault-tolerance properties.