Configuration updates are a common source of instability in networks today, frequently leading to outages, disruptions, and even security vulnerabilities. A key factor that makes updates difficult to implement is that networks are complex systems with many interacting components. A typical datacenter network consists of thousands of devices, a significant challenge for network administrators is that each of these devices must be reconfigured after an update. The goal of this research is to develop new mechanisms for implementing network configuration updates using techniques based on software synthesis.
To meet this goal, the research is developing (i) new synthesis algorithms based on efficient incremental model checking techniques; (ii) extensions that model bandwidth and fault tolerance using quantitative constraints and objective functions; and (iii) theoretical foundations based on connections to concurrent and distributed programming. The project will have broad impact by discovering new techniques that automate a difficult network administration task and by training undergraduate and graduate students with interdisciplinary skills in formal methods and networking.
