Computer networks are now, arguably, the United States' most critical infrastructure. They control all communication amongst our citizenry, our businesses, our government, and our military. Worryingly, however, today's networks are remarkably unreliable and insecure. A significant source of vulnerability is the fact that the underlying network equipment (e.g., routers and switches) run complicated programs written in obtuse, low-level programming languages, which makes managing networks a difficult and error-prone task. Simple mistakes can have disastrous consequences including making the network vulnerable to denial-of-service attacks, hijackings, and wide-scale outages.
The goal of this research is to transform the way that networks are managed by introducing a new class of network programming languages with the following essential features: (i) network-wide, correct-by-construction abstractions; (ii) support for fault-tolerance and scalability; (iii) coordination with end-hosts and independently-administered networks, as well as mechanisms for establishing trust between them; (iv) formal verification tools based on rigorous semantic foundations; and (v) compilers capable of generating efficient and portable code that runs on heterogeneous equipment. To demonstrate how to build a language with these features, the researchers are designing a language for OpenFlow networks called Frenetic, and evaluating it on several novel security applications. This project will have broad impact by (i) discovering key techniques for increasing the reliability of our networks, (ii) opening up the interfaces used to program networks, thereby enabling grass-roots innovation where it was previously not possible, and (iii) educating a new community of researchers with advanced skills in both networking and programming languages.