SHF: Medium: A Balance of Power: Programming and Reasoning for Software-Defined Networks

计算机网络使用交换机、路由器和其他设备来处理和转发流量。在传统网络中，这些设备协调一致，以商定流量应如何转发。软件定义网络（SDN）用逻辑上集中的控制器程序来代替这种分布式控制，该控制器程序通过安装规则来规定向每个设备的转发行为，该规则可以包括将某些流量发送到控制器以进行处理或通知的指令。不正确的规则可能会导致控制器错过重要的通知，使其对网络状态的看法不正确，并可能损害网络功能。另一方面，如果流量被不必要地发送到控制器，性能可能会受到影响。本项目正在开发Flowlog，一种无层次的SDN编程语言。无层次语言统一了SDN的不同编程层：控制器程序本身、交换机转发规则和控制器的内部状态。Flowlog安全地自动处理交换机上的规则管理，而无需程序员的任何干预。这不仅简化了开发，而且还防止了手动规则安装可能引起的上述错误。最后，Flowlog程序可以与任意其他程序进行交互，即使是那些不是用Flowlog编写的程序。由于控制器程序中的故障可能危及整个网络，因此程序可靠性至关重要。因此，Flowlog旨在实现对程序的自动推理，并且该项目正在构建支持程序验证（针对特定网络和一般网络），差分分析，容错测试，甚至自动修复错误程序。

Computer networks use switches, routers, and other devices to process and forward traffic. In a traditional network, these devices coordinate to agree on how traffic should be forwarded. Software-defined networks (SDN) replace this distributed control with a logically centralized controller program which dictates forwarding behavior to each device by installing rules which can include instructions to send certain traffic to the controller for processing or notification. Incorrect rules can lead to the controller missing vital notifications, giving it an incorrect view of the network's state and potentially harming network functionality. On the other hand, if traffic is sent to the controller needlessly, performance can suffer.This project is developing Flowlog, a tierless SDN programming language. A tierless language unifies the disparate layers of programming for SDNs: the controller program itself, switch forwarding rules, and the controller's internal state. Flowlog safely handles rule-management on the switches automatically, without any intervention from the programmer. This not only simplifies development, but also prevents the above bugs that can arise from manual rule-installation. Finally, Flowlog programs can interact with arbitrary other programs, even those not written in Flowlog. Since a failure in a controller program can compromise the entire network, program reliability is of central importance. Thus, Flowlog is designed to enable automatic reasoning about programs, and the project is building in support for program verification (both for a specific network and in general), differential analysis, fault-tolerance testing, and even automated repair of errant programs.