FMitF: Transplanting Syntax-Guided Synthesis to Computer Networks

计算机网络很难管理，因为在运营商为其网络设定的高级目标（例如，安全性、服务质量等）与必须表达这种意图的异构设备中的低级配置之间存在着巨大的鸿沟。虽然软件定义网络（一种新兴技术，集中控制如何处理流量的决策，并将其与实际转发每个数据包的设备分开）的出现有所帮助，但设计网络的过程仍然是临时的，导致高运营成本，设计错误占网络停机时间的很大一部分，以及代价高昂的安全漏洞。这个项目的动机是网络设计自动化的愿景，受到其他领域（如芯片设计）方法成功的启发。该项目将为网络架构师开发在更高抽象层次上表达其意图的方法，以及自动合成正确有效地实现此意图的低级交换机配置的技术。该项目将通过语法引导合成来解决网络自动化问题，语法引导合成在许多程序合成系统中都是一种流行的范例。该项目不像目前的网络合成工作那样直接合成低级别的交换机流表规则和交换机配置，而是将探索如何从用户提供的草图和规范中合成代码，这些代码与网络编程语言相对应，然后可以将其转换为低级别的交换机配置。这种方法将使人类专家能够传达他们的见解和提示，这对于应用现代合成技术至关重要。该项目将开发一种网络编程语言，该语言既具有表达能力，又具有必要的形式语义，以实现综合，探索网络综合草图的设计空间，并开发提高计算机网络综合性能的方法。这个项目更广泛的影响是提高管理大型网络的抽象水平，导致更低的管理成本，更好的性能，安全性和可靠性。该项目将广泛涉及研究生和本科生，并将新的课程材料纳入编程语言和网络课程。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Computer networks are difficult to manage since there exists a wide gulf between the high-level goals that operators have for their networks (e.g., security, Quality of Service etc.), and the low-level configurations in heterogeneous devices in which such intent must be expressed. While the advent of Software-Defined Networking (an emerging technology that centralizes control decisions regarding how traffic must be handled, and separates them from the devices that actually forward each packet) helps, the process of designing networks is still ad-hoc, leading to high operational costs, design faults that account for a large fraction of network downtime, and costly security breaches. This project is motivated by the vision of design automation for networking, inspired by the success of the approach in other domains such as chip design. The project will develop methods for network architects to express their intent at higher levels of abstraction, and techniques to automatically synthesize low-level switch configurations that realize this intent correctly and efficiently.The project will tackle network automation through syntax-guided synthesis, which has been a popular paradigm embodied in many program synthesis systems. Rather than directly synthesize low-level switch flow-table rules and switch configurations like current network synthesis efforts, the project will explore how to synthesize code from user-provided sketches and specifications, corresponding to a network programming language, which may then be translated into low-level switch configurations. This approach will enable human experts to convey their insights and hints, which are critical for applying modern synthesis techniques. The project will develop a network programming language that is expressive yet has the necessary formal semantics to enable synthesis, explore the design space of sketches for network synthesis, and develop ways to improve the performance of synthesis for computer networks. The broader impact of this project is to raise the level of abstraction for managing large networks, leading to much lower management costs, better performance, security and reliability. The project will extensively involve graduate and undergraduate students, and incorporate new curriculum material in programming language and networking classes.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.