面向真实世界的软件定义网络的模型检验（含附录）
Towards Model Checking Real-World Software-Defined Networks (version with appendix)
摘要：
在软件定义网络（SDN）中，控制器程序负责在大量交换机上部署各种网络功能，但这存在很大的风险：部署错误的控制器代码可能导致网络和服务中断以及安全漏洞。因此，最需要的是自动检测错误，或者甚至更好地验证错误的存在，但是网络的大小和控制器的复杂性使得这是一项具有挑战性的任务。在本文中，我们提出了MOCS，这是一种高度表达的优化SDN模型，可以在合理的时间内捕获细微的现实世界错误。这是通过（1）分析模型以获得可能的偏序约简，（2）静态地预先计算数据包等价类，以及（3）对模型中存在的数据包和规则进行索引来实现的。我们展示了其优越性相比，最先进的表现力方面，通过提供的例子，现实的错误，原型实现的MOCS在UPPAAL捕获，和性能/可扩展性，通过运行各种大小的网络拓扑结构的例子，突出我们的抽象和优化的重要性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
