The innovation of this work is a platform for automatic verification of network behavior. Every aspect of our society is now tightly intertwined with the functioning of computer networks such as the Internet. Unfortunately, modern networks are also extremely complex, leading to a rich variety of failure modes and outages. These errors have very high costs for businesses, including lost revenue and customers, fines from violating regulations such as HIPAA, leaks of sensitive information, and decline in corporate image. Automated tools to help operators by verifying network-wide correctness do not exist. To address this need, Veriflow will build a system, which automatically verifies security and correctness of computer networks in real time, discovers vulnerabilities, and assists network operators in determining their cause. Veriflow functions by scanning a network, constructing a formal model of the network's behavior, and using custom formal logic algorithms to automatically derive whether the network contains faults. Veriflow's algorithms are real-time, able to vet networks continuously as the network state evolves, detect transient errors and signal immediate alarms, and scale to large and highly dynamic environments.
The broader/commercial impact of Veriflow's work will significantly enhance reliability and security of critical network infrastructure, and ease network management tasks. The strong formal foundations of our tool coupled with its high-speed and advanced scaling properties will enable us to gain an important part of this emerging market. The company's past research has demonstrated potential of the system through two working prototypes, which have found 23 real bugs in a campus deployment serving over 70,000 machines, and perform real-time network-wide verification within one millisecond. Veriflow's work will produce new tools and implementations which Veriflow will make freely available for non-commercial use. Veriflow also hopes this work will serve towards enabling interdisciplinary research across formal methods and networking, with the common goal of enabling highly available networking infrastructures. Veriflow will work with the University of Illinois CITES group to deploy the system in their campus network, and in the Urbana-Champaign Big Broadband (UC2B) network, a community broadband project to provide gigabit fiber-to-the-premise to 2700 under-served residences and 350 community anchor institutions. Veriflow has also established working relationships with several large companies that serve large user populations as well as provide outreach to academic and research institutions.
Computer networks are incredibly crucial to our modern society. They have revolutionized the way we learn, play, work, and communicate. As critical societal infrastructures increasingly move online, from voice and emergency response services, to power grid and critical infrastructures, to medical and telesurgery networks, and financial networks moving trillions of dollars a day, making sure networks work properly is of increasingly critical importance to the functioning of our society. Unfortunately, our daily news is rife with stories of the failures of networks, from major leaks of sensitive and private data, to massive damage and outages, to infiltration and compromise of critical systems, on an array of governmental, commercial, and personal systems and data. Operators of these networks have access to extremely talented and sophisticated engineers, and the most advanced in network analysis tools and auditing practice. The problem is running a network correctly is hard. Networks are composed of a complex intertwining of hardware devices, protocols, management systems, and configurations, all of which need to be implemented and work properly together for the entire system to work. Like any complex system built by humans, computer networks are subject to errors, including misconfigurations, software bugs, cross-dependencies, and vendor incompatibility. The large size of many deployments means errors happen continuously and have large impact. Unfortunately, the extreme value networks makes them an attractive target for adversaries -- network crime is a $114B industry, and entire governments are funding cyberwarfare, bringing massive capital to find exploits and vulnerabilities. To address this, this project investigated the feasibility of a fundamentally new approach to protecting computer networks. We constructed a prototype of a tool, called Veriflow, which provides a real-time situational awareness of what your network "really" doing. Veriflow provides the ability to conduct rigorous checks, in a highly scalable fashion, of the network's data-plane, the low level instructions used to program the network hardware. Veriflow is capable of performing real-time analysis, enabling the tool to vet networks continuously as the network state evolves, detect transient errors and signal immediate alarms, guarantee compliance with regulatory requirements and security policies, and scale to large and highly dynamic environments. Since it is able to find problems in a fraction of a second, Veriflow can guard against disruptions in network service and avoid lost revenue or opportunities. This technology is possible through (1) our novel approach of network-wide analysis of data-plane instructions, not adopted in current network management tools, and (2) custom real-time verification algorithms, 100-1000 times faster than past techniques, developed in our lab at the University of Illinois over the last four years. This work has already realized real-world benefits. We have conducted pilot deployments of our system on production networks, where our tool has found a number of highly serious errors and vulnerabilities that were missed by existing state-of-the-art auditing techniques and monitoring tools. Our tool performed real-time network-wide verification within one millisecond, providing strong validation of its strong formal foundations and high speed and advanced scaling properties. We have also provided service to (1) Urbana-Champaign Big Broadband (UC2B), a community broadband network expected to provide gigabit fiber-to-the-premise to 2700 low-income residences and 350 community anchor institutions, along with communications for emergency response services. (2) the Global Environment for Network Innovations (GENI), which is building a collaborative and exploratory network environment for academia, industry, and the public to catalyze groundbreaking discoveries and innovation in emerging global networks. Our work will conduct additional deployments as well, which will serve larger user populations as well as provide outreach to academic and research institutions. Longer-term, our work stands to significantly enhance reliability and security of critical network infrastructure, and ease network management tasks. Building more reliable networks 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 disaster survival and recovery for business and government communication systems. Our proposed techniques 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. We also hope our work will serve as a key step towards enabling interdisciplinary research across formal methods and networking disciplines, with the common goal of enabling highly available networking infrastructures.
