FMitF: OpenRDC: A Framework for Implementing Open, Reliable, Distributed, Network Control

计算机网络，无论是连接跨数据中心的服务器还是连接全球用户，都是社会关键基础设施的重要组成部分。然而，现有的网络协议和服务根本不值得社会现在对它们的信任。今天的网络受到性能差、网络攻击、配置错误、软件错误等问题的困扰，给消费者、企业和政府都带来了严重的后果。该项目的目标是实现更好的网络设计和运行，这需要同时实现创新（创建更好的协议和服务）和验证（确保这些服务正常工作）。网络功能的一个主要部分依赖于运行在控制平面上的软件，它计算路由，收集和分析网络测量数据，平衡多个路径或服务器甚至主机网络应用程序的负载。本项目涉及OpenRDC的理论、设计和实现，OpenRDC是一个为可靠的分布式网络控制平面编程而构建的新平台。OpenRDC的技术核心围绕稳定信息树（sit）的计算展开，稳定信息树通过网络传递信息（例如，交通状况、故障信息、可用的外部路由、终端主机作业统计等），然后执行本地操作来改变网络功能或记录收集到的信息。这些结构化计算足以表达核心控制平面算法，但也可以转换为逻辑表示，可用于验证操作网络的各种重要属性，从可达性到访问控制再到多路径一致性。OpenRDC平台将同时：(1)允许研究人员开发新的控制平面算法，(2)启用网络属性的自动验证，(3)利用新兴的可编程交换机功能。该项目涉及通过网络编程的新抽象来加速新的控制平面算法的开发。该项目还将定义新的编译器技术，用于将这些抽象转换为可编程的网络硬件。此外，它的开源基础设施将为学术和工业参与以及学生培训奠定基础。该项目还将对形式化方法产生影响，为基于抽象和模块化分解的面向图形的编程语言提供新的验证算法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Computer networks, whether connecting servers across a data center or users across the globe, are an important part of society's critical infrastructure. However, existing network protocols and services are simply not worthy of the trust society now places in them. Today's networks suffer from poor performance, cyberattacks, configuration errors, software bugs, and more, leading to serious consequences for consumers, businesses, and governments alike. The goal of this project is to enable the design and operation of better networks which requires enabling both innovation (to create better protocols and services) and verification (to ensure these services work correctly). A major part of the functionality of the network depends on the software running in the control plane, which computes routes, collects and analyzes network measurement data, balances load over multiple paths or servers and even hosts in-network applications. This project involves the theory, design, and implementation of OpenRDC, a new platform constructed for programming reliable, distributed network control planes. The technical core of OpenRDC centers around computations of Stable Information Trees (SITs) that communicate information (e.g., traffic conditions, failure information, available external routes, end-host job statistics, etc.) across a network, and then perform local actions to change network functionality or record information gathered. These structured computations suffice to express core control plane algorithms and yet can also be converted into logical representations that can be used to verify a variety of important properties of operational networks ranging from reachability to access control to multi-path consistency. The OpenRDC platform will simultaneously: (1) allow researchers to develop new control-plane algorithms, (2) enable automatic verification of network properties, and (3) make use of emerging programmable switch capabilities. The project involves acceleration of the development of new control-plane algorithms, via new abstractions for network programming. The project will also define new compiler technology for translating these abstractions to programmable network hardware. In addition, its open source infrastructure will lay a foundation for academic and industrial engagement and for the training of students. The project will also have impact on formal methods, with new algorithms for the verification of graph-oriented programming languages based on abstraction and modular decomposition.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.