SBIR Phase I: Dynamic Data-Plane Verification in Heterogeneous Networks

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.