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

FMITF：OpenRDC：实现开放、可靠、分布式网络控制的框架

• 批准号: 1837030
• 负责人: Aarti Gupta
• 金额: $ 100万
• 依托单位: Princeton University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1837030&HistoricalAwards=false
• 关键词: FMitF; OpenRDC; Framework; Implementing; Open

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.

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

项目成果

Switch Code Generation Using Program Synthesis

• DOI: 10.1145/3387514.3405852
• 发表时间: 2020-07
• 期刊: Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication
• 作者: Xiangyu Gao;Taegyun Kim;Michael D. Wong;Divya Raghunathan;A. Varma;Pravein G. Kannan;Anirudh Sivaraman;S. Narayana;Aarti Gupta

Abstract interpretation of distributed network control planes

• DOI: 10.1145/3371110
• 发表时间: 2019-12
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ryan Beckett;Aarti Gupta;Ratul Mahajan;D. Walker

NV: an intermediate language for verification of network control planes

NV：用于验证网络控制平面的中间语言

• DOI: 10.1145/3385412.3386019
• 发表时间: 2020
• 期刊: PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Giannarakis, Nick;Loehr, Devon;Beckett, Ryan;Walker, David
• 通讯作者: Walker, David

CaT: A Solver-Aided Compiler for Packet-Processing Pipelines

• DOI: 10.1145/3582016.3582036
• 发表时间: 2023-03
• 期刊: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3
• 作者: Xiangyu Gao;Divya Raghunathan;Rui Fang;Tao Wang;Xiaotong Zhu;Anirudh Sivaraman;S. Narayana;Aarti Gupta

NAP: Programming Data Planes with Approximate Data Structures

NAP：使用近似数据结构对数据平面进行编程

• DOI: 10.1145/3630047.3630196
• 发表时间: 2023
• 期刊: ACM
• 作者: Pan, Mengying;Kim, Hyojoon;Rexford, Jennifer;Walker, David
• 通讯作者: Walker, David