FMitF: Transplanting Syntax-Guided Synthesis to Computer Networks

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

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.