论文标题
模型检查软件定义的网络，该网络具有超时的流入条目（带有附录的版本）
Model Checking Software-Defined Networks with Flow Entries that Time Out (version with appendix)
论文作者
论文摘要
软件定义的网络（SDN）可以通过（实际上）集中的，可编程的控制器对网络部署进行高级操作和管理，这些控制器通过在网络交换机的流程表中安装规则来部署网络功能。尽管这是一个强大的抽象，但越野车控制器功能可能会导致严重的服务中断和安全漏洞，从而激发了（半）自动化工具的需求，以查找甚至验证缺乏错误。文献中已经提出了模型检查SDN，但是现有的方法都无法支持动态网络部署，在该网络部署中，由于超时而导致流量输入到期。这对于网络中自动刷新（并消除了陈旧的状态（称为网络协议设计命名中的软状态））是必不可少的，这对于扩展应用程序或从失败中恢复至关重要。在本文中，我们扩展了模型（MOC）来处理流表条目的超时，从而支持网络中的软状态。提出了根据此扩展定制的优化。我们使用负载平衡器和防火墙在不同大小的网络拓扑中评估了Uppaal中提出的模型的性能。
Software-defined networking (SDN) enables advanced operation and management of network deployments through (virtually) centralised, programmable controllers, which deploy network functionality by installing rules in the flow tables of network switches. Although this is a powerful abstraction, buggy controller functionality could lead to severe service disruption and security loopholes, motivating the need for (semi-)automated tools to find, or even verify absence of, bugs. Model checking SDNs has been proposed in the literature, but none of the existing approaches can support dynamic network deployments, where flow entries expire due to timeouts. This is necessary for automatically refreshing (and eliminating stale) state in the network (termed as soft-state in the network protocol design nomenclature), which is important for scaling up applications or recovering from failures. In this paper, we extend our model (MoCS) to deal with timeouts of flow table entries, thus supporting soft state in the network. Optimisations are proposed that are tailored to this extension. We evaluate the performance of the proposed model in UPPAAL using a load balancer and firewall in network topologies of varying size.
