NeTS: Medium: From Verification to Synthesis in Software Defined Networks

NeTS：媒介：软件定义网络从验证到综合

• 批准号: 1513906
• 负责人: Philip Godfrey
• 金额: $ 120万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-10-01 至 2020-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1513906&HistoricalAwards=false
• 关键词: NeTS; Medium; Verification; Synthesis; Software

Every aspect of our society, from business, to government, to medicine and the sciences, is now tightly intertwined with the functioning of computer networks such as the Internet. Unfortunately, modern computer networks are extremely complicated, making them prone to implementation errors and misconfigurations, which can lead to vulnerabilities and other avenues to attack. To address this challenge, this project is designing and implementing systems which automatically verify correctness of network behavior, and correct vulnerabilities and errors in operational networks. These systems can provide immediate practical assistance to protecting networks and critical infrastructure against the attacks and cyberthreats we read about in the news every day.The project's technology functions by scanning a network, constructing a formal model of the network's behavior, and using custom formal logic algorithms to automatically derive diagnoses and repairs to network state. The core technical approach is founded on data-plane verification (DPV), which models network-wide properties using a view of the network that is as close as possible to the network's actual running behavior, i.e., the data plane: forwarding tables contained in routers, switches, firewalls, and other networking equipment. This low-level view allows DPV to catch and prevent errors that other tools miss, and provides a framework for the unified analysis of heterogeneous, multi-protocol networks.Intellectual Merit: This research is designing new algorithms to detect, prevent, and repair errors in complex networks. To achieve this, the researchers are developing a new class of formal methods to efficiently model network properties such as reachability, as well as techniques to store and query these models in real time. The researchers are also developing systems based on these algorithms to quickly and correctly localize faults, repair them before they can affect live networks, and deploy operating environments based on software-defined networking that automate application of their techniques. This research is shedding light on the ability to formally model networks, and is building insights into how to design networks and network protocols that have strong security properties from first principles. The work will also help enable interdisciplinary research across formal methods and networking disciplines, with the common goal of enabling highly available networking infrastructures.Broader Impacts: The results of this research will significantly enhance reliability and security of critical network infrastructure, and ease network management tasks. Being able to construct networks that can provide formal guarantees on the correctness and resilience of packet forwarding would have significant economic impact, by making networks more reliable and cost-effective. Networks that can deal reliably with rarely encountered exceptions are an essential component of attack survival and recovery for business and government communication systems. The techniques developed in this research will also improve resilience to misconfigurations, which may accelerate deployment of networks in underdeveloped and rural areas lacking experienced network operators with resources to troubleshoot network problems. Finally, the project is training students on cutting-edge and cross-disciplinary research in networking, formal methods, and security.

从商业，政府到医学和科学的各个方面，现在与计算机网络（例如互联网）的运作紧密相连。不幸的是，现代的计算机网络非常复杂，使它们容易实现错误和配置错误，这可能导致脆弱性和其他攻击途径。为了应对这一挑战，该项目正在设计和实施系统，这些系统会自动验证网络行为的正确性，并在操作网络中纠正漏洞和错误。这些系统可以为保护网络和关键基础架构提供即时实用的帮助，以防止我们每天在新闻中阅读的攻击和网络策略，通过扫描网络，构建网络行为的正式模型，并使用自定义形式的正式逻辑算法来自动诊断和重复网络状态来发挥作用。核心技术方法建立在数据平面验证（DPV）上，该方法使用网络的视图对网络范围的属性进行建模，该网络的视图与网络的实际运行行为尽可能近，即数据平面：路由器，交换机，防火墙和其他网络设备中包含的转发表：转发表。这种低级视图使DPV能够捕获和防止其他工具错过的错误，并为统一分析异质，多协议网络提供了一个框架。Intellectual功绩：这项研究是在设计复杂网络中检测，预防和修复错误的新算法。为了实现这一目标，研究人员正在开发一种新的形式方法，以有效地对网络属性进行建模，例如可及性，以及实时存储和查询这些模型的技术。研究人员还根据这些算法开发系统，以快速，正确地本地化故障，在影响实时网络之前修复它们，并根据软件定义的网络部署操作环境，从而自动化其技术的应用。这项研究阐明了正式建模网络的能力，并正在建立有关如何设计网络和网络协议的洞察力，这些网络和网络协议具有很强的第一原则。这项工作还将有助于跨正式方法和网络学科启用跨学科研究，并具有实现高可用的网络基础架构的共同目标。Broader的影响：这项研究的结果将显着提高关键网络基础架构的可靠性和安全性，并降低网络管理任务。能够通过使网络更加可靠和成本效益来构建可以为数据包转发的正确性和弹性提供正式保证的网络。可以可靠地处理很少遇到的例外的网络是攻击生存和企业和政府通信系统恢复的重要组成部分。这项研究中开发的技术还将提高对错误配置的弹性，这可能会加速在不发达和农村地区的网络部署，而这些网络缺乏经验丰富的网络运营商，这些网络运营商拥有资源来解决网络问题。最后，该项目是在网络，正式方法和安全性方面培训学生的尖端和跨学科研究。