SHF:Small:Collaborative Research:Practical Synthesis of Network Updates

点击翻译按钮获取中文摘要

Configuration updates are a common source of instability in networkstoday, frequently leading to outages, disruptions, and even securityvulnerabilities. A key factor that makes updates difficult toimplement is that networks are complex systems with many interactingcomponents. A typical datacenter network consists ofthousands of devices, a significant challenge for network administratorsis 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 synthesisalgorithms based on efficient incremental model checking techniques;(ii) extensions that model bandwidth and fault tolerance usingquantitative constraints and objective functions; and (iii)theoretical foundations based on connections to concurrent anddistributed programming. The project will have broad impact bydiscovering new techniques that automate a difficult networkadministration task and by training undergraduate and graduatestudents with interdisciplinary skills in formal methods andnetworking.