NeTS: Medium: From Verification to Synthesis in Software Defined Networks

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

Every aspect of our society, from business, to government, to medicine and the sciences, is now tightly intertwined with the functioning of computer networks such as the Internet. Unfortunately, modern computer networks are extremely complicated, making them prone to implementation errors and misconfigurations, which can lead to vulnerabilities and other avenues to attack. To address this challenge, this project is designing and implementing systems which automatically verify correctness of network behavior, and correct vulnerabilities and errors in operational networks. These systems can provide immediate practical assistance to protecting networks and critical infrastructure against the attacks and cyberthreats we read about in the news every day. The project's technology functions by scanning a network, constructing a formal model of the network's behavior, and using custom formal logic algorithms to automatically derive diagnoses and repairs to network state. The core technical approach is founded on data-plane verification (DPV), which models network-wide properties using a view of the network that is as close as possible to the network's actual running behavior, i.e., the data plane: forwarding tables contained in routers, switches, firewalls, and other networking equipment. This low-level view allows DPV to catch and prevent errors that other tools miss, and provides a framework for the unified analysis of heterogeneous, multi-protocol networks. Intellectual Merit: This research is designing new algorithms to detect, prevent, and repair errors in complex networks. To achieve this, the researchers are developing a new class of formal methods to efficiently model network properties such as reachability, as well as techniques to store and query these models in real time. The researchers are also developing systems based on these algorithms to quickly and correctly localize faults, repair them before they can affect live networks, and deploy operating environments based on software-defined networking that automate application of their techniques. This research is shedding light on the ability to formally model networks, and is building insights into how to design networks and network protocols that have strong security properties from first principles. The work will also help enable interdisciplinary research across formal methods and networking disciplines, with the common goal of enabling highly available networking infrastructures. Broader Impacts: The results of this research will significantly enhance reliability and security of critical network infrastructure, and ease network management tasks. Being able to construct networks that can provide formal guarantees on the correctness and resilience of packet forwarding would have significant economic impact, by making networks more reliable and cost-effective. Networks that can deal reliably with rarely encountered exceptions are an essential component of attack survival and recovery for business and government communication systems. The techniques developed in this research will also improve resilience to misconfigurations, which may accelerate deployment of networks in underdeveloped and rural areas lacking experienced network operators with resources to troubleshoot network problems. Finally, the project is training students on cutting-edge and cross-disciplinary research in networking, formal methods, and security.