CNS Core: Small: Towards a universal network verification framework

Johns Hopkins University, Baltimore MD

Investigators

Abstract

The reliability of computer networks is becoming ever more critical as networks increasingly perform mission critical functions such as intrusion detection and prevention. Verifying today's complex and large-scale computer networks, however, remains a challenging task. Existing network verification tools focus almost exclusively on different variants of reachability, e.g., is point A reachable from point B? Thus, they are incapable of providing strong reliability guarantees for modern networks. This project strives to provide a general framework for efficiently verifying desired properties for today's networks. Achieving this goal requires addressing fundamental open problems related to reasoning about the behavior of the large-scale dynamic systems. In addition to tackling these problems, the project supports education as its various sub-problems can be defined as intellectually stimulating research projects for undergraduate and graduate students. Towards the goal of enabling efficient verification of correctness properties, this project provides compositional programming abstractions that allow network operators to express their network functions and desired properties. It will also provide an automata-theoric framework that decomposes any arbitrary property into safety and liveness properties. Verifying the total correctness of a firewall, for example, involves verifying that its output actions such as blocking hosts meet its specification (a safety property) and that it actually takes action, e.g., by blocking malicious traffic (a liveness property). Fundamentally, then, fast verification reduces to efficiently verifying safety and liveness properties. Alas, efficient verification of general safety and liveness properties for large-scale stateful networks is an open problem. While existing network verifiers can efficiently verify some classes of invariants such as loop-freedom, they are not general and cannot verify all safety properties. Plus, existing verification techniques do not scale to verify liveness properties fast -- verifying these properties is algorithmically challenging and in some cases undecidable. This project strives to bridge this gap by providing algorithms for general and scalable safety and liveness verification for stateful networks, e.g., by modeling the network behavior as compact Boolean formulas. While fast, such abstract models are known to over-approximate the system's behavior and a property violated in the abstract model may hold in the original program. Thus, one of the goals of the project is to formally prove the correctness of verification on these compact models, i.e., a property holds on them if and only if it holds on the actual program. Finally, a compiler will be provided to translate the verified programs to code runnable on existing application-specific integrated circuits. The project website, which will include its publications, code, results, and data, will be publicly available at http://cs.jhu.edu/~soudeh/research/verification.html and will be maintained for at least three years after the project is completed. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.