The security, performance, and availability of our critical network infrastructures relies on the correct implementation of different policy goals. Network operators realize these goals by composing and configuring diverse network appliances such as routers, firewalls, intrusion prevention systems, and web proxies. Unfortunately, this process of managing networks is extremely challenging, error-prone, and entails significant manual effort and operational costs. Configuration and implementation errors could have significant consequences as it can degrade network performance, induce downtime for critical infrastructures, and cause violations of key security postures. Systematically identifying and diagnosing potential violations has been, and continues to be, a fundamental challenge. This project will develop a principled framework to check if a network setup correctly implements a given suite of policies and to help operators proactively and automatically diagnose and localize the sources of policy violations.
Checking policy violations is hard even for simple reachability properties (e.g., can A talk to B) in today's networks. Furthermore, next-generation technologies such as software-defined networking and network functions virtualization are poised to enable richer dynamic policies (e.g., if a host generates too many connections, subject it to deeper inspection) and also introduce new sources of complexity (e.g., elastic scaling, software bugs). Existing approaches in network testing and verification have fundamental expressiveness and scalability challenges in tackling dynamic policies and stateful elements. To address these challenges, the research will include developing a model-based testing framework that will lead to fundamental advances in network semantics, modeling, testing, and diagnosis. To this end, the project will design: (1) new formal semantics to express dynamic policies over stateful networks; (2) expressive-yet-efficient abstractions for modeling the behavior of advanced network functions; (3) techniques to synthesize models of network functions; (4) scalable symbolic execution algorithms to generate test cases; and (5) efficient diagnosis algorithms to validate tests and localize violations.
Broader Impacts: The proposed research and education activities will develop testing tools and abstractions, which is a new capability that bolsters networking education, research, and practice. The project will inspire future educators and practitioners to apply systematic network testing as an integral part of their workflow to guarantee the security, performance, and availability our critical infrastructures. The project will develop new educational modules that will be integrated into the research with undergraduate and graduate-level classes and undergraduate capstone classes. The research and education efforts will engage undergraduates and underrepresented communities. The project will create unique opportunities for interdisciplinary training of the future workforce across the domains of networking, security, programming languages, and formal verification. The project will also design novel security games and education modules for K-12 students and teachers to highlight the importance of network testing for securing our critical infrastructures. Finally, the project deliverables (code, models, and education modules) will be released under open-source licenses as enablers for other researchers and educators, and to help transition the ideas from research to practice.
