论文标题
要模型检查现实世界软件定义的网络（带有附录的版本）
Towards Model Checking Real-World Software-Defined Networks (version with appendix)
论文作者
论文摘要
在软件定义的网络（SDN）中，控制器程序负责在大量开关中部署多样化的网络功能，但这有很大的风险：部署错误控制器代码可能会导致网络和服务中断和安全漏洞。因此，自动检测错误，甚至更好地验证其缺席的验证是最可取的，但是网络的大小和控制器的复杂性使这是一项艰巨的任务。在本文中，我们提出了MOC，这是一种高度表达，优化的SDN模型，允许在合理的时间内捕获微妙的现实错误。这是通过（1）分析模型的部分减少，（2）静态预计数据包等价类以及（3）模型中存在的索引数据包和规则来实现的。我们通过提供了逼真的错误示例，即在捕获的Uppaal中实现MOC的实现，并且通过在各种网络拓扑的示例中运行示例，从而强调了我们的摘要和优化的重要性，我们通过提供了现实的错误的实例来证明其优势与艺术的状态相比。
In software-defined networks (SDN), a controller program is in charge of deploying diverse network functionality across a large number of switches, but this comes at a great risk: deploying buggy controller code could result in network and service disruption and security loopholes. The automatic detection of bugs or, even better, verification of their absence is thus most desirable, yet the size of the network and the complexity of the controller makes this a challenging undertaking. In this paper we propose MOCS, a highly expressive, optimised SDN model that allows capturing subtle real-world bugs, in a reasonable amount of time. This is achieved by (1) analysing the model for possible partial order reductions, (2) statically pre-computing packet equivalence classes and (3) indexing packets and rules that exist in the model. We demonstrate its superiority compared to the state of the art in terms of expressivity, by providing examples of realistic bugs that a prototype implementation of MOCS in UPPAAL caught, and performance/scalability, by running examples on various sizes of network topologies, highlighting the importance of our abstractions and optimisations.
