CAREER: Checking Dynamic Policies in Stateful Next-Generation Networks

我们关键网络基础设施的安全性、性能和可用性依赖于不同策略目标的正确实施。网络运营商通过组合和配置各种网络设备（如路由器、防火墙、入侵防御系统和Web代理）来实现这些目标。不幸的是，这种管理网络的过程极具挑战性，容易出错，并且需要大量的手动工作和运营成本。配置和实施错误可能会造成严重后果，因为它会降低网络性能，导致关键基础设施停机，并导致违反关键安全状况。系统地查明和诊断潜在的违规行为一直是并将继续是一项根本性挑战。该项目将开发一个原则性的框架，以检查网络设置是否正确地实现了给定的一套政策，并帮助运营商主动自动诊断和定位违反政策的来源。 即使对于简单的可达性属性（例如，在今天的网络中，A可以和B交谈。 此外，诸如软件定义网络和网络功能虚拟化之类的下一代技术准备启用更丰富的动态策略（例如，如果主机生成太多连接，则使其经受更深的检查）并且还引入新的复杂性源（例如，弹性缩放、软件错误）。现有的网络测试和验证方法在处理动态策略和有状态元素时具有基本的表达性和可扩展性挑战。为了应对这些挑战，研究将包括开发一个基于模型的测试框架，这将导致网络语义，建模，测试和诊断的根本性进步。 为此，该项目将设计：（1）新的形式语义来表达有状态网络上的动态策略;（2）用于建模高级网络功能行为的表达性但有效的抽象;（3）合成网络功能模型的技术;（4）可扩展的符号执行算法来生成测试用例;（5）有效的诊断算法来验证测试和定位违规。 更广泛的影响：拟议的研究和教育活动将开发测试工具和抽象，这是一种新的能力，支持网络教育，研究和实践。该项目将激励未来的教育工作者和从业者将系统的网络测试作为其工作流程的一个组成部分，以保证我们关键基础设施的安全性，性能和可用性。该项目将开发新的教育模块，这些模块将与本科生和研究生级别的课程以及本科生顶点课程相结合。研究和教育工作将吸引本科生和代表性不足的社区。该项目将为跨网络，安全，编程语言和正式验证领域的未来劳动力的跨学科培训创造独特的机会。 该项目还将为K-12学生和教师设计新颖的安全游戏和教育模块，以强调网络测试对保护我们的关键基础设施的重要性。最后，项目的可交付成果（代码、模型和教育模块）将在开源许可下发布，作为其他研究人员和教育工作者的推动者，并帮助将想法从研究转化为实践。

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.