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.