CAREER: Checking Dynamic Policies in Stateful Next-Generation Networks

职业：检查有状态的下一代网络中的动态策略

• 批准号: 1552481
• 负责人: Vyas Sekar
• 金额: $ 61.26万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-04-15 至 2022-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1552481&HistoricalAwards=false
• 关键词: CAREER; Checking; Dynamic; Policies; Stateful

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.

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