We will develop and evaluate algorithms for a system, Veriflow, which can automatically reason about security and correctness of computer networks in real time. Veriflow operates 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 inconsistencies, errors, or violations of specified invariants. Veriflow will confirm correctness, or provide a specific example vulnerability if one exists. Moreover, our algorithms are real-time: Veriflow can vet networks continuously as the network state evolves, detect transient errors and signal immediate alarms, and scale to large and highly dynamic environments. The key personnel are well-qualified. We previously developed two prototype network verification systems. Initial evaluations of our systems have found 23 real bugs in a real operational network of 178 routers, and scaled to networks of a several hundred devices while performing network-wide checks in less than one millisecond. This proposal will extend these prototypes with verifiers for a much richer set of policies and algorithms to support a much wider range of devices, providing a flexible platform for reasoning about network behavior. We will also extensively evaluate our algorithms using real operational network snapshots, ensuring millisecond-level verification latency.
Benefit: Veriflow will deliver a novel technology to localize and diagnose faults in operational networks. The competitive advantage of our product is fourfold. First, our system builds on formal logic, enabling it to provide strong results that are provably correct. Second, our novel algorithms enable our system to perform checking at extremely high speeds. Third, our system is general, allowing it to diagnose a large class of faults that affect operational correctness and performance, and to interoperate with a variety of heterogeneous network technologies. Finally, our tool is automatic, enabling it to
Keywords: scalable, scalable, network analysis, real-time, diagnostic algorithms., localization and diagnosis, security, Formal methods, data-plane
